シークエント計算の推論図におけるWRなどの意味

閲覧いただきありがとうございます。
いま大学で論理学の授業を受けています。
LKの部分をテキストで勉強していますが、なかなか理解できません。
推論図の例などは手元にあるんですが、そもそもweakening, contraction, exchange, cut などがそれぞれどのような意味を持っているのかが分かりません。
テキストには

Γ1, Γ2　⇒　Δ
----------------- WL
Γ1, A, Γ2 ⇒　Δ

などの推論図は載っているんですが詳しい解説はありません・・・。
右と左の区別もよくわかりません。
どなたか詳しい方教えていただけたら幸いです。
よろしくお願いします。

No.2 回答者： minodaiski 回答日時： 2012/08/07 17:52

シーケント計算 ( LK ともいう ) におけるシーケントとは、仮に A、B、C が各々論理式 (または命題) とすれば、

A, B → C

のような形のものを指し、意味は

「命題 A と 命題 B を前提にすると 命題 C が推論される」

... 程度になります。

一方、次のものが 'LK の推論' として現れたとします。

A, B → C
━━━━━
D, E, F → G

... これは、意味としては、
「『命題 A、B を前提とすると 命題 C が推論される』のだから、『命題 D、E、F から 命題 G を推論できる』」

... 程度になります。これは ' 推論についての推論 ' と言えます。LK のおおきな特徴です。

以上を踏まえて、幾つかの推論図 (構造規則) を見ましょう。但し、日本語で表記します。

Γ → Δ
━━━━ (増左)
A, Γ → Δ

... ここで、Γ や Δ は論理式 (または命題) の列を一般的に表します。空の場合も含まれます。気持ちは、

A1,A2, A3, ..., An → B1, B2, ..., Bm
━━━━━━━━━━━━━━━━━━ (増左)
C, A1,A2, A3, ..., An → B1, B2, ..., Bm

... なのですが、長くて見にくい上、「...」という表現が嫌われている節があり、普通はこのようには書かれませんが、Γ や Δ が ぴんとこなければこのような表現に直せば良いでしょう。

さて、意味ですが、

「ある推論が成り立つならば、その前提に任意の論理式 (または命題) を加えたものもやはり推論として成り立つ」

... となります。一方で、

Γ → Δ
━━━━ (増右)
Γ → Δ, A

は、「ある推論が成り立つならば、その結論の候補に 論理式 (または命題) A を加えても推論として成り立つ」

... という程度の意味になります。

ここで、Δ ( または上の話の B1,... ,Bn ) は『結論の候補』位の意味をもちます。次のシーケント...

A → B, C

は、

「前提 A からは 、B または C が推論される」

を意味します。B と C は結論の候補に過ぎないのです。

しかし、仮に ￢B が成り立てば、C が結論として確定します。これを一般化すると、次の論理規則になるわけです。

Γ → Δ, A
━━━━━ (￢左)
￢A, Γ → Δ

このように推論を模式化したものとしてシーケントを見ると、考えやすくなります。

最後に、cut を調べましょう。

Γ→Δ, A　A, Π→Λ
━━━━━━━━ (cut)
　　Γ, Π→Δ, Λ

簡単のため、論理式の列 Γ、Π、Δ、Λ をそれぞれ単一の論理式 ( または命題 ) からなるとして、各々、P 、Q、R、S として cut を書くと、

P→Q, A　A, R→S
━━━━━━━━ (cut)
　　P,R →Q,S

... となります。これは一種の三段論法であり、Q と R がない形は代表的です。

少し調べましょう。

『P→Q, A』が成り立てば『P,￢Q → A』も成り立ちます。ここで、『A,R →S』が成り立てば、次のような推論が可能です。

(1) P ［前提］
(2) R ［前提］
(3) ￢Q ［前提］
(4) A ［(1)、(3)、P,￢Q → A より］
(5) S ［(2)、(4)、A,R →S より］

... この推論から『P,R,￢Q → S』が推論として成り立つと分かります。
ここで、否定の論理規則から、

P,R,￢Q → S
━━━━━━━ (￢右)
P,R → S,￢￢Q

... となります。この下式から『P,R→Q,S』が成り立つことが (意味から) 分かります。

［補足］
推論 A,B → C,D について、前提部 (A、B) や結論部 (C、D) の並びは推論の正しさには関係ありません。B,A → D,C 、としたところで、意味は一つです。すなわち、

『A と B を前提とすると、結論の候補 C と D が得られる』

... となります。このことは、構造規則

Γ,A,B,Π → Δ
━━━━━━ (換左)
Γ,B,A,Π → Δ

などで表現されています。［補足終り］

このように、'cut' は三段論法を一般化したものと言えます。

(まとめ)
シーケント計算では、シーケントが推論を、推論図が『正しい推論から、正しい推論を導く』推論を、それぞれ表します。
この視点に立てば、推論図についてもっと考えやすくなるでしょう。

No.1 回答者： noname#160411 回答日時： 2012/07/25 19:14

ごめんなさい、解答ではありません。

これ、カテゴリー違いでは？　オイラのような国語の人間は目ぇパチクリです。