〜，⇒に関わる inference rules

古典論理での〜の導入（INTRO）と消去（ELIM）の推論には，以下の４通りがあります．

〜Ａ|-　　　　|-〜Ａ
−−−−　　−−−−
　　|-Ａ　　Ａ|-
　　　　　　(UNDISCH o NOT_ELIM)
　　|-Ａ　　Ａ|-
−−−−　　−−−−
〜Ａ|-　　　　|-〜Ａ
　　　　　　NEG_DISCH,(NOT_INTRO o DISCH)

# ARITH_RULE `~(n<0)`;;
val it : thm = |- ~(n < 0)
# NOT_ELIM it;;
val it : thm = |- n < 0 ==> F
# UNDISCH it;;
val it : thm = n < 0 |- F
# DISCH_ALL it;;
val it : thm = |- n < 0 ==> F
# NOT_INTRO it;;
val it : thm = |- ~(n < 0)　　　　　　

古典論理での⇒の導入（INTRO）と消去（ELIM）の推論には，以下の４通りがあります．

Ａ⇒Ｂ|-　　　　　　　|-Ａ⇒Ｂ
−−−−−−−−　　−−−−−
　|-Ａ　　Ｂ|-　　　Ａ|-Ｂ
　　　　　　　　　　UNDISCH

　　　　　　　　　　Ａ|-　または　|-Ｂ
　|-Ａ　Ｂ|-　　　　　　　Ａ|-Ｂ　　　　
−−−−−−−　　　−−−−−−−−−
Ａ⇒Ｂ|-　　　　　　　　　　|-Ａ⇒Ｂ
LII 　　　　　　　　DISCH

...
val th1 : thm = n = 0 |- 2 * n = 0
val th2 : thm = n = 1 |- 2 * n = 2
# LII th1 th2;;
val it : thm = n = 0, 2 * n = 0 ==> n = 1 |- 2 * n = 2

なお，古典論理では（〜Ａ)∨Ｂ，Ａ⇒Ｂは互いに書き換えられますので，〜，⇒の推論は互いに書き換えられます．