|| 証明の形式的な表現
「証明」のための「計算方法」のこと。
スポンサーリンク
目次
・シークエント「演繹（正しい推測）の形式的な表し方」
・シークエント計算「シークエントを使った計算」
・構造規則「証明の構造から考えて明らかな規則」
シークエント (推件式) Sequent
|| 前提と結論を分けた表し方みたいなもの
これは『証明』の「形式的な表現」のことで、
「演繹」の中身を整理する時に使われたりします。
\begin{array}{llllll} \displaystyle Γ&⊢&\Psi \end{array}
具体的にはこんな感じですね。
意味は「 Γ は \Psi を証明する」です。
記号に関しては、
『 Γ,\Psi 』は「論理式の列（たくさん）」で、
左側に来るやつ Γ を「前件 antecedent 」
右側に来るやつ \Psi 」を「後件 succedent 」
なんて言ったりします。
ちなみに「論理式の列 Γ,\Psi 」の中身は、
\begin{array}{llllll} \displaystyle Γ&=&(ω_1,ω_2,...,ω_n) \end{array}
当然、論理式 ω_i です。
シークエント計算 Sequent Calculus
|| シークエントからシークエントを
そのまま、シークエントを使った計算のこと。
\begin{array}{lllllll} \displaystyle Γ_1&⊢&Δ_1 \\ \\ Γ_2&⊢&Δ_2 \\ \\ &↓& \\ \\ Γ_1 ,Γ_2&⊢&Δ_1, Δ_2 \end{array}
具体的にはこんな感じで、
「定理１,２から別の定理を導く」時とかに使われたりします。
命題論理と推件式 (シークエント)
シークエントの「前件」と「後件」は、
その性質上、以下のように分割することが可能です。
\begin{array}{llllllllll} \displaystyle Γ&=&ω_1∧ω_2∧…∧ω_n \\ \\ \Psi&=&ψ_1∨ψ_2∨...∨ψ_n \end{array}
シークエントは記号だと↓のように解釈できるので。
\begin{array}{llllllll} ω_1∧ω_2∧…∧ω_n&&→&&ψ_1∨ψ_2∨…∨ψ_n \end{array}
これは適当に和訳すると直観的に分かると思います。
（あれで）かつ（あれ）なら （ああなる）もしくは（そうなる）
（あれ）で（これ） なら （ああなる）または（こうなる）
（あー）で（こー） なら （あー）か（そー）
論理式の列
念のため補足しておくと、
「前件」「後件」は、厳密には「論理式の列」ですから、
『使わない論理式』が入っている可能性はあります。
\begin{array}{llllllll} ω_1∧ω_2∧…∧ω_n&&→&&ψ_1∨ψ_2∨…∨ψ_n \end{array}
そのため、この解釈では「全ての論理式が真である」
ということが求められているわけですが、
必ずしもそうとは限らないので、
実際には、使わない論理式は使わなくても良いです。
↑の解釈はあくまで
『必要で正しい論理式だけを集めた場合』の話なので、
それとごっちゃにならないよう気を付けてください。
構造規則 Structure Rules
|| 証明でやって良いこと
「証明の構造上存在する規則」のこと。
\begin{array}{lllll} \displaystyle Γ,ω_A,ω_B,Δ⊢\Psi &&→&& Γ,ω_B,ω_A,Δ⊢ \Psi \\ \\ Γ,ω_A,ω_A,Δ⊢\Psi&&→&&Γ,ω_A,Δ⊢\Psi \\ \\ Γ,ω_A,Δ⊢\Psi&&→&&Γ,ω_A,ω_B,Δ⊢\Psi \end{array}
「論理積・論理和」の性質から
『交換』『追加』『重複を一つに』することができるので、
これらの性質は必然的に導かれることになります。
転置規則 Permutation,Exchange
『 ω_A∧ω_B=ω_B∧ω_A （交換法則）』から
\begin{array}{lllllll} \displaystyle Γ, ω_A,ω_B,Δ⊢\Psi &&→&& Γ,ω_B,ω_A,Δ⊢ \Psi \\ \\ \end{array}
縮約規則 Contraction
『 ω_A∧ω_A=ω_A （冪等性）』から
\begin{array}{llllllll} \displaystyle Γ,ω_A,ω_A,Δ⊢\Psi&&→&&Γ,ω_A,Δ⊢\Psi \end{array}
弱化規則 Weakening
シークエントの「解釈」から、
\begin{array}{llllllll} \displaystyle Γ,ω_A,Δ⊢\Psi&&→&&Γ,ω_A,ω_B,Δ⊢\Psi \end{array}
これは「無関係な文（論理式）」を入れたとしても、
必要な「前提・結論」が欠けてないなら正しい、という感じ。
「 A でありかつ B であるなら～となる」
「 A でありかつ B であり、 C である（無関係）なら～となる」
見ての通り、
いらない文（正しい）が入ったとしても
それで「文の正しさ」は変わりません。
「結論を導くのに必要な条件」は全てそのままなので、
「必要最低限の条件」から「より狭い条件」になっただけ。
なので、この操作は可能となります。
より厳密には『不必要な文は使わない』
ということも許されるので、
不要な文を挟むことで全体に影響が及ぶことはない。
だから許される って感じでしょうか。
そしてこれは「後件」の側でも同様。
「いずれかの結論が導かれる」というのが解釈になるので、
「導かれる結論」が一つでも入ってればOKになります。
シークエント計算と構造規則
シークエント計算の書き方なんですが、
\begin{array}{llllll} \displaystyle \displaystyle \frac{ω_A,ω_B⊢\Psi}{ω_B,ω_A⊢\Psi} \end{array}
これは「 ↑ のから ↓ が導ける」
ということを意味する記号で、
以下で紹介する「構造規則」を含め
『形式的証明』はこのように表現されることがあります。
転置規則 PL, PR （Permutation Left, Right）
\begin{array}{llllll} \displaystyle \frac{Γ,ω_A,ω_B,Δ⊢\Psi}{Γ,ω_B,ω_A,Δ⊢\Psi} && \displaystyle\frac{Γ⊢\Phi,ψ_A,ψ_B,Π}{Γ⊢\Phi,ψ_B,ψ_A,Π} \end{array}
縮約規則 CL, CR （Contraction Left, Right）
\begin{array}{llllll} \displaystyle\frac{Γ,ω_A,ω_A,Δ⊢\Psi}{Γ,ω_A,Δ⊢\Psi}&&\displaystyle\frac{Γ⊢\Phi,ψ_A,ψ_A,Π}{Γ⊢\Phi,ψ_A,Π} \end{array}
弱化規則 WL, WR （Weakening Left, Right）
\begin{array}{llllll} \displaystyle\frac{Γ,ω_A,Δ⊢\Psi}{Γ,ω_A,ω_B,Δ⊢\Psi} && \displaystyle\frac{Γ⊢Φ,ψ_A,Π}{Γ⊢Φ,ψ_A,ψ_B,Π} \end{array}
以上
「シークエント計算」の基本はこんな感じですね。
