名词
合取：逻辑与
析取：逻辑或
合取式：所有子式都成立的式子
析取式：至少一个子式成立的式子
证明规则
[frac{Hvdash Q}{H, Pvdash Q}, Mononicity
]
上面的条件范围更广，下面的条件范围更窄，广中任意都成立，所以窄中任意也成立。
[frac{Hvdash Q, R, Qvdash P}{R, Hvdash P}, Cut
]
(Q) 为真， (H) 也为真 。
[H, Pvdash P, Hypothesis
]
条件成立，作为结论也自然成立。
[frac{Hvdash P Hvdash
eg P}{Hvdash perp}, False\_Rule
]
反证法。要证结论不成立，只需要假设结论成立，然后证明条件矛盾即可。
[H, perpvdash P, False\_Law
]
存疑。
[frac{H, Pvdash perp}{Hvdash
eg P}, Not\_Rule
]
要证 (HRightarrow eg P) ，即证 (H, P) 均为真时，命题不成立。
[frac{H,
eg Qvdash P}{H,
eg Pvdash Q}, Not\_Law
]
反证。假设结论不成立，推出条件矛盾。
[frac{Hvdash P Hvdash Q}{Hvdash Pigwedge Q}, And\_Rule
]
要证 (HRightarrow Pigwedge Q) ，只需要证 (HRightarrow P) 和 (HRightarrow Q) 都成立。
[frac{H, Pvdash Q}{Higwedge Pvdash Q}, And\_Law
]
要证 (Higwedge PRightarrow Q) ，即证 (H, P) 都为真时， (Q) 为真。
[frac{H,
eg Pvdash Q}{Hvdash Pigvee Q}, Or\_Rule
]
要证 (HRightarrow Pigvee Q) ，即证 (H, eg P) 均为真时， (Q) 也为真。
[frac{Pvdash H Qvdash H}{Pigvee Qvdash H}, Or\_Law
]
要证 (Pigvee QRightarrow H) ，即证 (PRightarrow H) 和 (QRightarrow H) 均为真。
[frac{H, Pvdash Q}{Hvdash P
ightarrow Q}, Implication\_Rule
]
要证 (HRightarrow P ightarrow Q) ，即证 (H, P) 都为真时， (Q) 为真。
[frac{H, P, Qvdash R}{H, PRightarrow Qvdash R}, Implication\_Law
]
要证 (H, PRightarrow QRightarrow R) ，即证 (H, P, Q) 都为真时， (R) 为真。