bool(5.1) ∀，∃に関わる inference rules

∀の導入（INTRO）と消去（ELIM）の推論には，以下の４通りがあります．ただし，全称，特称はメタのものです．

　|-全称　∀|-　　　　|-∀
−−−−−−−−　　−−−−
　　　|-　　　　　　　|-全称
LAE 　　　　　　　　SPEC,SPECL

特称|-　　　　　　　　|-全称
−−−−　　　　　　−−−−
　∀|-　　　　　　　　|-∀
LAI 　　　　　　　　GEN,X_GEN

・古典論理では，対角の推論どうしは，カット（PROVE_HYP）で互いに書き換えられます．
従って，左上のLeft All Elim（LAE）は

# let LAE (a,tha) thx = PROVE_HYP (GEN a tha) thx;;
val ( LAE ) : term * thm -> thm -> thm = <fun>

val th1 : thm = !n. 0 <= n |- b = b
val th2 : thm = b = 1 |- 0 <= a
val th3 : thm = a = 1 |- 0 <= a
# LAE (`a:num`,th2) th1 ;;
val it : thm = b = 1 |- b = b
# LAE (`a:num`,th3) th1 ;;
Exception: Failure "ABS".(* a は仮定にも出現してるので失敗する*)

左下の（LAI）Left All Intro は

# let LAI (px, x) thm = PROVE_HYP (SPEC x (ASSUME px)) thm ;;
val ( LAI ) : term * term -> thm -> thm = <fun>

# UNDISCH_ALL(ARITH_RULE `a>0 ==> a<0 ==> a=0 ==> b=0`);;
val it : thm = a < 0, a = 0, a > 0 |- b = 0
# LAI (`!n. n = 0`, `a:num` ) it;;
val it : thm = !n. n = 0, a < 0, a > 0 |- b = 0

のように実装できます．

∃の導入（INTRO）と消去（ELIM）の推論には，以下の４通りがあります．ただし，全称，特称はメタのものです．

　∃|-　　　　　　　　　　|-∃　全称|-
−−−−　　　　　　　　−−−−−−−−
全称|-　　　　　　　　　　　　　|-
LEE 　　　　　　　　　　CHOOSE

全称|-　　　　　　　　　　|-特称
−−−−　　　　　　　　−−−−
　∃|-　　　　　　　　　　|-∃
CHOOSE,SIMPLE_CHOOSE　　EXISTS,SIMPLE_EXSITS

・古典論理では，対角の推論どうしは，カット（PROVE_HYP）で互いに書き換えられます．従って，左上（LEE）Left Exists Elim は

# let LEE (px, a) thm =
   let pa = rhs(concl(BETA_CONV (mk_comb((rand px),a)))) in
   PROVE_HYP (EXISTS (px, a) (ASSUME pa)) thm ;;
val ( LEE ) : term * term -> thm -> thm = <fun>

# ASSUME `?n. n = 0` ;;
val it : thm = ?n. n = 0 |- ?n. n = 0
# LEE (`?n. n = 0`, `a:num` ) it;;
val it : thm = a = 0 |- ?n. n = 0
# ADD_ASSUM `?n. n = 1` it;;
val it : thm = ?n. n = 1, a = 0 |- ?n. n = 0
# ADD_ASSUM `?n. n = 2` it;;
val it : thm = ?n. n = 2, ?n. n = 1, a = 0 |- ?n. n = 0
# LEE (`?n. n = 2`, `1` ) it;;
val it : thm = ?n. n = 1, a = 0, 1 = 2 |- ?n. n = 0

# ASSUME `?x.(p:A->bool)(x:A)` ;;
val it : thm = ?x. p x |- ?x. p x
# LEE (`?x.(p:A->bool)(x:A)`, `a:A`) it;;
val it : thm = p a |- ?x. p x
# SIMPLE_CHOOSE `a:A` it;;
val it : thm = ?a. p a |- ?x. p x

# ASSUME `?x.(p:A->bool)(x:A)` ;;
val it : thm = ?x. p x |- ?x. p x
# LEE (`?x.(p:A->bool)(x:A)`, `a:A`) it;;
val it : thm = p a |- ?x. p x
# CHOOSE (`a:A`,(ASSUME(`?x.(p:A->bool)(x:A)`))) it;;
val it : thm = ?x. p x |- ?x. p x

# ASSUME `?x.(p:A->bool)(x:A)` ;;
val it : thm = ?x. p x |- ?x. p x
# LEE (`?x.(p:A->bool)(x:A)`, `a:A`) it;;
val it : thm = p a |- ?x. p x
# CHOOSE (`a:A`,(ASSUME(`?y.(p:A->bool)(y:A)`))) it;;
val it : thm = ?y. p y |- ?x. p x

# ASSUME `(p:A->bool)(a:A)` ;;
val it : thm = p a |- p a
# EXISTS (`?x.(p:A->bool)(x:A)`, `a:A`) it;;
val it : thm = p a |- ?x. p x
# CHOOSE (`a:A`,(ASSUME(`?y.(p:A->bool)(y:A)`))) it;;
val it : thm = ?y. p y |- ?x. p x

のように実装できます．

さらに，古典論理では，∀，∃についての推論は一般化されたドモルガン則

# search[name"NOT";name"FORALL"];;
val it : (string * thm) list =
  [("FORALL_NOT_THM", |- !P. (!x. ~P x) <=> ~(?x. P x));
   ("NOT_FORALL_THM", |- !P. ~(!x. P x) <=> (?x. ~P x))]
# search[name"NOT";name"EXISTS"];;
val it : (string * thm) list =
  [("EXISTS_NOT_THM", |- !P. (?x. ~P x) <=> ~(!x. P x));
   ("NOT_EXISTS_THM", |- !P. ~(?x. P x) <=> (!x. ~P x))]

で互いに書き換えられます．