シーケント計算 ( 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' は三段論法を一般化したものと言えます。
(まとめ)
シーケント計算では、シーケントが推論を、推論図が『正しい推論から、正しい推論を導く』推論を、それぞれ表します。
この視点に立てば、推論図についてもっと考えやすくなるでしょう。
