|| 証明の形式的な表現
簡単に言うと「証明」のための「計算方法」です。
「演繹」のやり方。「推論」のための「推論」とも言われます。
スポンサーリンク
目次
・シークエント「演繹（正しい推測）の形式的な表し方」
・シークエント計算「シークエントを使った証明の形式」
・構造規則「証明の構造から考えて、明らかな規則」
ともかく、これはやり方です。
なのでさっさとどういうものか見た方が良いでしょう。
シークエント Sequent
|| 前提と結論を分けた表し方
これは、要は「形式的な表現」のことです。
「演繹」をやるときに形式的に表現するための方法になります。
これだけじゃ意味わかんないんで、どういうものか見てみましょう。
とりあえず簡単に、「証明の書き方」みたいに思っておけばOKです。
まず「論理式の列（たくさん）」を用意します。『 Γ,Δ 』で。
んで、前提に来るやつを「 Γ 」とし、（前件とか言われます）
結論側に来るやつを「 Δ 」とします。（こっちは後件）
すると↓みたいに書けます。
書けますってか、書くことにします。
Γ⊢Δ
これの意訳は「 Γ は Δ を証明する」です。
ちなみに「論理式の列」ということにしてる「 Γ 」は、
つまるところ、論理式を「 ω_i 」とすると、
『 Γ=(ω_1,ω_2,...,ω_n) 』ってことです。
シークエント計算 Sequent Calculus
|| 証明を形式的に
この「計算」では、1行を「 Γ⊢Δ 」で表します。
『1行を』です。証明図は何行かになります。
ともあれ、まずは「 Γ⊢Δ 」の意味について。
これは『 Γ=ω_1∧ω_2∧…∧ω_n 』で、（論理積）
『 Δ=ψ_1∨ψ_2∨...∨ψ_n 』となって、（論理和）
(ω_1∧ω_2∧…∧ω_n)→(ψ_1∨ψ_2∨…∨ψ_n)
という感じに解釈されます。（論理包含）
これは適当に和訳すると直観的に分かります。
例えば↓みたいなのはよく見る文です。
（あれで）かつ（あれ）なら、（ああなる）もしくは（そうなる）
（あれ）で（これ）なら、（ああなる）または（こうなる）
（あー）で（こー）なら、（あー）か（そー）
これを形式的に表すと↑のみたいになるわけです。
こう考えると分かり易くないですか？
ではなぜこう（命題論理を使って）しないのかと言うと、
この「シークエント計算」では、
使われている「論理式が正しいか」を問わないからです。
どういうことかというと、
「シークエント」は『証明する』ということを表すので、
「妥当な推論規則」なら「論理式」は確実に「真」です。（重要）
逆に言えば「正しくない論理式」を扱う意味がありません。
扱う論理式は『証明のための論理式』なんですから、
任意に「正しいものだけ」を選ぶことができますし。
なので「命題論理」より、範囲が狭いんです。
こちらで扱う論理式は『すべて正しくしていい』ので。
ともかく、「命題論理」の記号で解釈できるので、
『交換法則が使える』ことを確実に理解しましょう。
これがシークエントの核と言って良いくらいです。
以上から、シークエント計算には「規則」が存在します。
それは↑の解釈から得られることをきちんと押さえておきましょう。
もう一度確認です。
シークエントは、「命題論理」で定義されてます。
次に紹介するものは、この『記号』由来のものになります。
構造規則 Structure Rules
|| 証明でやって良いこと
主に「 3 」つの「規則」が導けます。
その規則の元となったものは、記号の性質です。
一つは「論理積・論理和」の性質から、交換できることが。
一つは「論理積・論理和」の性質から、追加できることが。
一つは「論理積・論理和」の性質から、重複を一つにできることが。
転置規則 Permutation,Exchange
『 ω_A∧ω_B=ω_B∧ω_A 』なので（交換法則）
『 ω_A,ω_B⊢ψ 』から『 ω_B,ω_A⊢ψ 』が導ける。
論理和でも一緒。
縮約規則 Contraction
『 ω_A∧ω_A=ω_A 』なので（冪等性）
『 Γ,ω_A,ω_A,Δ⊢ψ 』から『 Γ,ω_A,Δ⊢ψ 』が導ける。
論理和でも同じ。
弱化規則 Weakening
シークエントの「解釈」から、
『 Γ,ω_A,ω_A,Δ⊢ψ 』から『 Γ,ω_A,ω_B,Δ⊢ψ 』を導く。
これは「無関係な文（論理式）」を入れたとしても、
必要な「前提・結論」が欠けてないなら正しい、という感じ。
意訳すると直観的になります。
「 A でありかつ B であるなら、～となる」
「 A でありかつ B であり、 C である（無関係）なら、～となる」
単にいらない言葉が入っただけで、「文の意味」は正しいままです。
「結論を導くのに必要な条件」は全てそのままなので、
単に「必要最低限の条件」から「より強い条件」になっただけの話。
これは「結論側」でも同じです。
結論側は「いずれかの結論が導かれる」ので、
「導かれる結論」が一つでも入ってればOKです。
というわけで大方の準備は整いました。
というわけで、これらをシークエント計算で表してみましょう。
単なる書き方の決まりとして、
「上から下が導かれる」とすると、
縮約規則 CL
Contraction Left
\displaystyle\frac{Γ,ω_A,ω_A,Δ⊢ψ}{Γ,ω_A,Δ⊢ψ}
弱化規則 WL
Weakening Left
\displaystyle\frac{Γ,ω_A,ω_A,Δ⊢ψ}{Γ,ω_A,ω_B,Δ⊢ψ}
転置規則 PL
Permutation Left
\displaystyle\frac{ω_A,ω_B⊢ψ}{ω_B,ω_A⊢ψ}
右側（Right）に関しては「論理和」ですから、
「冪等性」から「縮約規則」が成立するのは確定です。
「交換法則」も成立するので「転置規則」も成り立ります。
どれか一個合ってれば良いので「弱化規則」もOKです。
というわけで、右側の「構造規則」も見ていきましょうか。
縮約規則 CR
Contraction Right
\displaystyle\frac{Γ,Δ⊢Φ,ψ_A,ψ_A,Π}{Γ,Δ⊢Φ,ψ_A,Π}
弱化規則 WR
Weakening Right
\displaystyle\frac{Γ,Δ⊢Φ,ψ_A,ψ_A,Π}{Γ,Δ⊢Φ,ψ_A,ψ_B,Π}
転置規則 PR
Permutation Right
\displaystyle\frac{Γ,Δ⊢Φ,ψ_A,ψ_B,Π}{Γ,Δ⊢Φ,ψ_B,ψ_A,Π}
以上が「シークエント計算」の基本になります。
記号が意味するところを理解できてれば、それでOKです。
