|| 証明の記号操作の根拠になるもの
「証明」のための「計算方法」のこと
スポンサーリンク
目次
シークエント「証明の記号的な表現方法」
シークエント計算「シークエントを使った計算」
構造規則「証明の構造から考えて明らかな規則」
推件式 Sequent
|| 前提と結論を記号で分けた表現方法
『証明を表現する形』をした「記号表現」のこと
\begin{array}{ccc} 前提 & \overset{←から→が導かれる}{\longrightarrow} & 結論 \\ \\ Γ&⊢&φ \end{array}
これの『記号と意味を分離する』ための概念で
（「記号である」などのメタレベルの意味は残る）
\begin{array}{lcl} 構文段階 && Γ\vdash φ の形をした記号 \\ \\ 記号要請段階 && Γやφや\vdash の具体的な中身 \\ \\ 全体要請段階 && Γ\vdash φ 全体の振る舞いの形式表現 \end{array}
その意味はこのような形で区分されています。
（実際の運用ではメタレベルの意味しか持たない記号を指す）
記号 \vdash の変遷
これは以前ちょっと曖昧に使われていた記号で
（『最終的に証明を表現する』点では一致していた）
\begin{array}{ccc} 証明 &\overset{中身を記号で表現して整理}{\longrightarrow}& 前提\vdash 結論 \\ \\ Γ\vDash φ &\overset{モデル内での表現に形成}{\longrightarrow}& Γ\vdash φ \end{array}
だいたいこのような意味で使われていました。
（本質的には同じだが役割と厳密さに差異がある）
\begin{array}{ccc} Γ\vdash φ &\longrightarrow& この記号表現を推件式と呼ぼう \end{array}
これを整備したのが「推件式」で
\begin{array}{ccc} 直感的な意味での証明 &\to& 推件式の形 \\ \\ 記号的な意味での証明 &←& 推件式の形 \end{array}
これにより「証明である（述語）」を
より厳密な形で定義できるようになりました。
（証明？文の記号表現 → 記号の形チェック）
推件式の意味的な要請的定義
↑ では「推件式の形」は定義されましたが
\begin{array}{ccl} Γ && 前提を表しているはず \\ \\ \vdash && 左側から右側が導かれるを意味するはず \\ \\ φ && 結論を表しているはず \end{array}
これらについての定義はまだされていません。
（チェック対象の範囲がまだ広過ぎる）
\begin{array}{ccl} Γ,\vdash,φ &←& この定義も必要 \\ \\ Γ\vdash φ &←& これがどう振る舞うかも必要 \end{array}
この部分が「意味的に要請される定義」であり
（ここでの『意味』はメタレベルの意味以外の意味）
\begin{array}{ccc} 規則上は大丈夫な記号操作 &\to& 証明計算 \end{array}
この「定義に従う」という形で
『証明の計算』は定義されています。
使われる記号への要請的定義
これについては
\begin{array}{ccc} Γ &\Longleftrightarrow& 前提 \\ \\ φ &\Longleftrightarrow& 結論 \\ \\ Γ\vdash φ &\Longleftrightarrow& Γからφが導かれる \end{array}
この感覚的な定義から
（ ↑ の時点では真偽が重要だが ↓ からは問われない）
\begin{array}{ccc} Γ &\Longleftrightarrow& 論理式の有限列か論理式が要素の有限集合 \\ \\ φ &\Longleftrightarrow& １つの論理式 \\ \\ \vdash &\Longleftrightarrow& チェックの手順で置かれる記号 \end{array}
このような形で厳密に定義されています。
（これでもまだ『証明自体の振る舞い』は曖昧）
推件式かどうかのチェックの流れ
補足しておくと
\begin{array}{ccl} チェック対象 &\to& 導かれるや証明できるなどを記号⊢に変換 \\ \\ &\to& 自然言語表現を論理式に翻訳 \\ \\ &\to& 自然言語が残っているか \\ \\&\to& 無いならチェック対象は加工済み \end{array}
まず「論理式への変換」はこんな感じ。
（これを通過できないものはそもそも数学では扱えない）
\begin{array}{ccc} チェック対象 &\to& 加工済みチェック対象 &\to& 推件式？ \end{array}
その上で定義される
「推件式であるか」のチェック方法は
\begin{array}{lcl} 加工済みチェック対象 &\to& 推件式の概形 Γ\vdash φ を目指す \\ \\ &\to& とりあえず記号 \vdash を置く \\ \\ &\to& φに該当する記号を\vdash の右側に置く \\ \\ &\to& Γに該当する記号を\vdash の左側に置く \\ \\ &\to& Γ \vdash φ に含まれない記号があるか \\ \\ &\to& 無いなら推件式である \end{array}
こんな感じになります。
（これによりチェックの精度が向上した）
それが証明であるのなら
以上でほとんど定義できた気もしますが
実際は「推件式ならできるはずのこと」
推件式全体への意味的な要請的定義
シークエント計算 Sequent Calculus
|| シークエントを元にした計算のこと
「推件式の定義」と「規則」による『記号操作』
\begin{array}{lcl} Γ_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}
以上
「シークエント計算」の基本はこんな感じですね。