一般化された体系における cut除去定理の成立条件

記号が制限された古典/直観主義
2階命題論理について
2007年12月4日
-1-
証明論研究集会
テーマ
• 直観主義論理で証明できない論理式の例
• ∧、¬のみの論理記号を持つ体系ならば古典論理と等価。
LK∧¬ ⇒ A
LJ∧¬
⇒
A
• 命題変数に対する量化記号∃を加えたらどうなるか？
(藤田憲悦, 2007)
LK∧¬∃ ⇒
A
?
LJ∧¬∃
-2-
⇒
A
直観主義２階命題論理
• 命題変数に対する量化記号
 A
(, r ) *
  p. A
A[ B / p],   
(, l )
p. A,   
A,   
(, l ) *
p. A,   
  A[ B / p]
(, r )
  p. A
– ただし、A[B/p] はA中の命題自由変数pを全て論理式Bに置き換えたものである。
– また、*のついた規則では、pは結論に自由変数としては現れない。
• 例
p ∧q  r
p  q  r  (, r )
p  q  r  p.( p  r )
p∧¬p∧q  r , s
(, l )
p.( p  p  q)  r , s
-3-
2階命題論理の付値
• 直観主義2階命題論理
– 一般フレーム … 付値の付き方を制限したクリプキフレーム
M (p. A) 
 M [ / p] ( A)
 Q
• 古典2階命題論理
M (p. A)  T　
M ( A[T / p])  T　かつ　M ( A[ / p])  T
M (p. A)  T　
M ( A[T / p])  T　または　M ( A[ / p])  T
– 例
M (p.( p  q))  T　iff　v(q)  T
-4-
古典論理LK
推論規則
A,   
(, l )1
A  B,   
A,   
(, l )
pA,   

( w, l )
A,   
A,   
(nam e, l )
A' ,   
–
–
–
–

A A
始式
Τ
A,   
(, l ) 2
B  A,   
  , A[ B / p]
(, r )
  , pA

( w, r )
  , A
  , A    , B
( , r )
  , A  B
  , A
(, l )
A,   
A, A,   
(c, l )
A,   
  , A
(nam e, r )
  , A'
A,   
(, r )
  , A
  , A, A
( c, r )
  , A
  , A A,   
(cut)
,   , 
論理規則は∧、¬、∃の規則のみ持つ。
構造規則は通常通り持つ。
(, l ) においてpは下式に自由変数としては現れない。
(name, l ), (name, r ) におけるA’はAの束縛変数を変更したものである。
-5-
直観主義論理LJ
推論規則
A,   
(, l )1
A  B,   
A,   
(, l )
pA,   

( w, l )
A,   
A,   
(nam e, l )
A' ,   
–
–
–
–

A A
始式
Τ
A,   
(, l ) 2
B  A,   
  A  B
( , r )
  A B
 A
(, l )
A,  
  A[ B / p]
(, r )
  pA
A,  
(, r )
  A
A, A,   
(c, l )
A,   

( w, r )
 A
 A
( name , r )
  A'
  A A,   
(cut)
,   
論理規則は∧、¬、∃の規則のみ持つ。
構造規則は通常通り持つ。
(, l ) においてpは下式に自由変数としては現れない。
(name, l ), (name, r ) におけるA’はAの束縛変数を変更したものである。
-6-
方針と問題点
A
• LK
ならば LJ
 A を示したい
• 一般化の試み1
–
A  B を (A  B) の略とする。
LK

ならば LJ
  
– 証明は容易
¬ ¬A となってしまう。
– しかし、    ,   A とすると、LJ
• 一般化の試み2
LK

  A, A
(c, r )
 A
 A
ならば LJ


  B,  
A, B
(cut)
,   A
-7-
 A

  A,
B
(, l )
B,   A
LK’の完全性
• 体系LK’… LK から(cut), (c,r) を外した体系
• 補題1
LK

LK’

• 証明
• （
）
– LK’の証明図をそのままLKの証明図とみなせる。
• （
）
– LKの証明図からcut除去、contraction右除去ができればよい。
-8-
cut, contraction右の除去
• cut除去


  , A[ B / p]
A,   
(, r )
(∃,l)
p.A
∃
p.A ,   
  , ∃
(cut)
,   , 
?
• contraction右除去

  , A[ B / p], A[C / p]
(∃,r)
  , A[ B / p], p. A
(, r )
  ,∃
p.A,∃p.A
(c,r)
  , p. A　証明論な手法は(∃,r)の扱いづらさにより困難
-9-
?
LKの健全性
• 付値
– v … 命題変数から{T,F} への写像
– M … 論理式から{T,F}への写像
M ( p)  T　 v( p)  T
M ( A  B)  T　 M ( A)  T　かつ　M ( B)  T
M (A)  T　 M ( A)  F
M (p. A)  T　 M ( A[T / p])  T　または　M ( A[ / p])  T
– M … シークエントから{T,F}への写像
M (  )  T　 M (()  ())  T
• LKの健全性
LK

ならば任意の付値vで
M (  )  T　– 証明 … Γ⇒Δの証明図に関する帰納法による。
- 10 -
論理式Aのツリー
• 任意の付値でM(A)=T となるAから次のようなツリーを構成する。
– ノードがシークエント
– 根のノードはS0（「⇒A」）
– 任意のノードのシークエントSαに対し任意の付値でM(Sα)=T
• 葉に対し以下の操作を繰り返す
,
,
Γ⇒Δ
¬A
A ,Γ⇒Δ
,
Γ⇒Δ ,¬A
A
,
,
[q/p] ,
Γ⇒Δ
Γ⇒Δ, AA∧BB
∃p.AA ,Γ⇒Δ
Γ⇒Δ
- 11 -
,
Γ⇒Δ
AA∧BB ,Γ⇒Δ
, [B/p]
Γ⇒Δ
Γ⇒Δ, ∃p.AA
B の定義
vi ～ vj
任意のp
∈ FV(Sα)
に対し、vi(p) = vj(p)
・
• ツリーの定義の停止性
  q  r,    ,
・ V – {vシークエント中の「∃の数」と「論理記号の数」に関する二重帰納法による。
i | 付値viのもとで M ()  T , M ()  F}
Bi
Bi
 { p | vi ( p)  T　かつ、 p  FV ( S )}
 {p | vi ( p)  F　かつ、 p  FV ( S )}
 v0  {q  T r  T }


V   v1  {q  F r  T }
v  {q  T r  F }
 2

M ( A[T / p])  Tならば、 Bi  Bi  Bi
A[T / p]  (T  q)  (T  r )
M ( A[T / p])  Fならば、 Bi 
B0  q  r　B1  q  r　B2 
q  r  (r  q)  (r  r )
{Bi | vi  V }
・ B
例
(
r
B  ((q
q∧
r)r ∨
) (¬q
(∧
q r)
∨
r )⊥

r
)
(
)
(¬p∨pr)∨r)
q∨qr∨r⇒⇒ ∃p.(p
(p∨q)∧(¬
- 12 -
S
Γ⇒Δ , A [B/p]
S
Γ⇒Δ, ∃p.A
LK’の完全性
• LK’の完全性
任意の付値vで M ( A)  T　ならば LK’
 A
• 証明
– A のツリーを作成する。
– 「全てのシークエントが証明可能」を葉までの長さに関する帰納法で示す
– 任意の付値とシークエントSαでM(Sα)=T （ツリーの性質）
– ノードαが葉の時
• 両辺に共通の命題変数を含む
• 左辺に⊥を含む
• 右辺にTを含む
p,r⇒p,s
p,⊥⇒
p⇒T,q
全て証明可能
⇒A
- 13 -
LK’の完全性
A, Γ⇒Δ
Γ⇒Δ , A
Γ⇒Δ ,¬A
¬A ,Γ⇒Δ
,Γ⇒Δ
(, l )
Γ⇒Δ , B
Γ⇒Δ , A
A∧B ,Γ⇒Δ
( , l )
(, r )
A  B, B,   
( , l )
A  B, A  B,   
(c, l )
A [q/p] , Γ⇒Δ
Γ⇒Δ , A [B/p]
∃pA ,Γ⇒Δ
Γ⇒Δ, A∧B
A, B, Γ⇒Δ
(, l )
q. A[q / p],   
- 14 -
Γ⇒Δ, ∃pA
(, l )
(nam e, l )
(, r )
グリベンコの定理
• グリベンコの定理
LK
–
–
–
–
⇒ A
LJ
⇒ ¬¬ A
これは1階命題論理の定理だが、∃を加えても成り立つ
証明
(
) … 自明
(
) … 「LK Γ⇒Δ ならば LJ Γ, ¬Δ⇒ 」を示し、(¬,r)を用いる。
• 系
LK
⇒¬ A
LJ
⇒¬ A
– 証明
– （） … 自明
– （
） … グリベンコの定理よりLJ ⇒¬¬¬A
一方LJ
¬¬¬A⇒¬A
なのでcut規則より。
- 15 -
主定理
• 定理
– 記号が∧、¬、∃に制限された２階命題論理において
LK
⇒ A
LJ
⇒ A
• 証明
– （
– （
） … 自明
） … 補題1 ( LKとLK’の同値性 ) より次を示せばよい。
LK’ ⇒ A
ならば
LJ
– cut規則, contraction右規則を考えなくてよい。
– Aの証明図に関する帰納法による。
(i) 始式の場合。( ⇒T )のみなので自明。
- 16 -
⇒ A
LK’ ⇒A ならば LJ ⇒A
LK’


A B
( , r )
 A B

 A[ B / p]
(, r )
 p. A
帰納法の仮定を用いる
LJ
( , r )
 A B
LK

A
(, r )
 A
グリベンコの定理の系
(, r )
 p. A
⇒ A
LJ
- 17 -
⇒ A
∀を加えた場合
• LKとLK’の同値性は成り立つ
• グリベンコの定理を示せず
「LK Γ⇒Δ ならば LJ Γ, ¬Δ⇒ 」
- 18 -
ご清聴ありがとうございました。
- 19 -

Download Report