LK の健全性の証明

各言語の任意の論理式は,証明論においては,証明系で証明できる式,すなわち,定理式か否かに,モデル論においては,任意の構造,任意の変数への個体割り当てに対して真となる式,すなわち,恒真式か否かに,それぞれ分類されますが,その分類が同じ結果となるという性質を,証明系の健全性と完全性と呼びます.

ここでの「健全性(soundness),および,完全性(completeness)」とは,現実の数学に正しさの基準を置くモデル論から見て,証明系が「恒真でない式を証明してしまわない(健全である)こと,および,恒真な式を漏らさず証明できる(完全である)こと」を表したものです.

勿論,pvs が基づく証明系 LK も健全かつ完全であり,例えば,ある式が証明できないことは,カウンターモデル(その式の否定のモデル,いわゆる反例)の存在と等価であり,証明可能な式は,数学のどんな分野に戻しても正しい主張になります.

そのことは,任意の閉論理式の集合Σ,任意の閉論理式φに対して

1.Σ|-φ

2.Σ∪{¬φ}|-⊥

3.Σ∪{¬φ}にモデルはない

4.任意の構造に対して

 Σ∪{¬φ}には偽の式が属する,つまり

 Σに属する任意の式が真ならば,φは真

5.Σ|=φ

が等価であることから判ります.

なお,健全性(1から5)を導くことは容易で,LK の各推論規則から恒真の含意が得られることを確かめれば充分です,つまり,Σの全ての要素と¬⊥の連言を∧Σ,Δの全ての要素と⊥の選言を∨Δとして(一般結合則を見た上で),シーケントΣ⇒Δに含意の全称閉包∀(∧Σ⊃∨Δ)を対応させ,LKの推論規則のうち,Σ⇒ΔからΣ'⇒Δ'という形のものに対しては
 ∀(∧Σ⊃∨Δ)⊃∀(∧Σ'⊃∨Δ')
が,同じく,Σ_1⇒Δ_1とΣ_2⇒Δ_2からΣ'⇒Δ'という形のものに対しては
 ∀(∧Σ_1⊃∨Δ_1)∧∀(∧Σ_2⊃∨Δ_2)⊃∀(∧Σ'⊃∨Δ')
が,それぞれ恒真ならば,始式の恒真性と推論の個数についての帰納法から,証明図の最下式(終式?)も恒真という訳です.

例えば,MESON で確かめると...

  (* !L *)
  MESON[] `!p r:A->bool q:A->A->bool t:A->A. (
  (!y.( (p y /\ q (t y) y) ==> (r y) ))
   ==>
  (!y.( (p y /\ (!x. q x y)) ==> (r y) ))
  )` ;;
0..0..1..2..solved at 6
val it : thm =
  |- !p r q t.
         (!y. p y /\ q (t y) y ==> r y) ==> (!y. p y /\ (!x. q x y) ==> r y)
#
  (* ?L *)
  MESON[] `!p r:A->bool q:A->A->bool. (
  (!x y.( (p y /\ q x y) ==> (r y) ))
   ==>
  (!y.( (p y /\ (?x. q x y)) ==> (r y) ))
  )` ;;
0..0..1..2..solved at 6
val it : thm =
  |- !p r q.
         (!x y. p y /\ q x y ==> r y) ==> (!y. p y /\ (?x. q x y) ==> r y)
#
  (* cut *)
  MESON[] `!p q r:A->bool. (
  (!x.( (p x /\ q x) ==> (r x) )) /\ (!x.( (p x) ==> (q x \/ r x) ))
   ==>
  (!x.( (p x) ==> (r x) ))
  )` ;;
0..0..1..2..7..12..solved at 18
val it : thm =
  |- !p q r.
         (!x. p x /\ q x ==> r x) /\ (!x. p x ==> q x \/ r x)
         ==> (!x. p x ==> r x)

となります.