シークエント計算 Sequent Calculus


|| 証明の形式的な表現

簡単に言うと「証明」のための「計算方法」です。

「演繹」のやり方。「推論」のための「推論」とも言われます。

スポンサーリンク





目次


シークエント「演繹(正しい推測)の形式的な表し方」

シークエント計算「シークエントを使った証明の形式」


構造規則「証明の構造から考えて、明らかな規則」







ともかく、これはやり方です。

なのでさっさとどういうものか見た方が良いでしょう。






シークエント 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です。