|| LK (論理計算) で戸惑う
最も有名で使われまくってる「推論規則」
「一階述語論理」で「完全」かつ「健全」
スポンサーリンク
目次
横棒「↑のが↓を導くってことにする」
論理式「一階述語論理のものに限定する」
構造規則「左右、名前を省略して書くことにする」
項「 t とか u を項ってことにする」
変数「 x とかを変数ってことにする」
規則「シークエントで書かれます」
同一律「これはこれだっていう当たり前」
構造規則「シークエントの定義上必ずそうなるやつ」
命題記号「命題記号を使う上での決まり」
量化記号「量化記号を使う上でのルール」
カット規則「証明の省略をして良いっていうやつ」
この記事の内容は『シークエント計算』
これを理解してないと雰囲気しか分かりません。
ですから、見ていない方は是非とも確認を。
記号の意味・解釈
『記号』について 3+3 つ確認します。
これに加えて、
『項』に関して 3 つ
『変数』に関して 2 つ確認
計 11 個はちょっと多いかもしれませんが、
どれも１つ１つはわりと簡単な話なので
覚えるのに難は無いと思います。
シークエントの記号表現
ここが「LKの推論規則」のメインの話になるでしょうか。
↑で定めた記号を使って規則を確認していきます。
まず『公理』である「同一律」から
『構造規則』について 3 つ
『命題記号』に関して 2+1+2+1 個
『量化記号』のことを 1+1 個
こちらも計 11 個確認していきます。
そして最後に『カット規則』をやって
それで終わりですね。
以上、
大きく分けて「 3+3+1 」つの「規則」が
まとめて『LKの推論規則』と呼ばれます。
「記号」「項」「変数」
「命題記号」「量化記号」「構造規則」
「カット規則」
記号の意味
「論理式」と「構造規則」について解説。
構造規則についてはただの省略ですが、
わりと必要なのでちゃんと覚えましょう。
論理式について 3 つ
・『横棒 「 — 」』の意味
\begin{array}{llllllllllll} \displaystyle \frac{}{ω \vdash ω} \end{array}
「上の論理式」から「下の論理式」が導かれる
上になんも無い場合は『公理』
・『 ω,ψ 』の意味
「一階述語論理」の『論理式』のこと。
（用途から「命題論理」のものに限定されたりします）
・『 Γ,Δ,Σ,Π 』の意味
「有限」個（ 0 を含む）の「論理式の列」のこと
\begin{array}{llllllll} \displaystyle Γ\vdash Δ \end{array}
これは『脈絡・文脈（コンテキスト）』
なんて呼ばれたりします。
「命題（論理式）を詳しく説明する文」
みたいなものだと考えて良いです。
\begin{array}{llllll} \displaystyle ω,φ && φ,ω \\ \\ Γ,ω,φ,Δ && Γ,φ,ω,Δ \end{array}
役割は「前後の文」「省略」
「定理を証明する証明文」を表現する時に
『空白を埋める』時なんかでこれが必要になります。
\begin{array}{llllllll} \displaystyle Γ\vdash Δ \end{array}
例えばこういう風に証明の一般形を書く時とか
\begin{array}{llllllll} \displaystyle Γ,ω,φ,Δ\vdash Γ,φ,ω,Δ \end{array}
一般性の担保のために付け加えられたりとか。
構造規則の省略表現 3 つ
・収縮規則
\begin{array}{lllllllllll} \displaystyle \mathrm{Contraction \,\, Left/Right} &&→&& CL/CR \end{array}
・弱化規則
\begin{array}{lllllllllll} \displaystyle \mathrm{Weakening \,\, Left/Right} &&→&&WL/WR \end{array}
・転置規則
\begin{array}{lllllllllll} \displaystyle \mathrm{Permutation \,\, Left/Right} &&→&& PL/PR \end{array}
これは単なる省略。
難しく考えないでください。
項の規則 3 つ
・項を表す記号『 t 』
記号 t は『項』を表すことにします。
『項』は「定数」「変数」「関数」の総称
・変数に注目する表現『 ω[t] 』
記号 ω[t] は
項 t に注目した『論理式 ω 』を表すことにします。
（論理式の中に t があることを確定させる）
・置換を表現するための記号『 ω[s/t] 』
記号 ω[s/t] は
「 ω[t] 」の「自由変項 t 」を「項 s へ」
『置換した論理式』を表すことにします。
また、この置換での束縛は起きないこととします。
\begin{array}{lllllllll} \displaystyle ∀x & A(x,y) \end{array}
具体的にはこのようなものがある場合
「束縛されてない y 」を
\begin{array}{llllll} \displaystyle A[x/y] \end{array}
「束縛子 ∀ 」から『束縛されている変数 x 』へ置換する
こういうのをダメってことにします。
変数（変項）の規則 2 個
・変数を表す文字『 x,y 』
x,y は『変数（変項）』を表すことにします。
自由変数か束縛変数かはこの時点じゃ決めません。
・自由変数と束縛変数の区分け『 ∀,∃ 』
量化子「 ∀,∃ 」で
中身が制限されてない変数を『自由変数』
中身が制限されてるやつを『束縛変数』と呼ぶことにします。
以上で『記号の意味』については終わり。
以下、↑の記号で書かれた推論規則の話をしていきます。
LKの推論規則
|| 必要最低限の妥当な推論規則
「一階述語論理」を採用する場合
これを採用された理論は健全かつ完全になります。
同一性の公理 Identity
「これはこれ」っていう
前提にしないと話が始まらないやつ。
シークエントで書くと↓
\begin{array}{llllllll} \displaystyle\frac{ }{ω⊢ω} \end{array}
基本的に公理はこんな風に書かれます。
なんで正しいのか説明できないので。
構造規則 (3)
・収縮規則「 ∧,∨ の冪等性」
\begin{array}{lllllllllll} \displaystyle \displaystyle\frac{Γ,ω,ω⊢Δ}{Γ,ω⊢Δ}(CL) && \displaystyle\frac{Γ⊢ω,ω,Δ}{Γ⊢ω,Δ}(CR) \end{array}
・転置規則「 ∧,∨ の交換律」
\begin{array}{lllllllllll} \displaystyle \displaystyle\frac{Γ_{\mathrm{first}},ω_A,ω_B,Γ_{\mathrm{last}}⊢Δ}{Γ_{\mathrm{first}},ω_B,ω_A,Γ_{\mathrm{last}}⊢Δ}(PL) && \displaystyle\frac{Γ⊢Δ_{\mathrm{first}},ψ_A,ψ_B,Δ_{\mathrm{last}}}{Γ⊢Δ_{\mathrm{first}},ψ_B,ψ_A,Δ_{\mathrm{last}}}(PR) \end{array}
・弱化規則「 ∧,∨ の文の解釈」
\begin{array}{lllllll} \displaystyle \displaystyle\frac{Γ⊢Δ}{Γ,ω⊢Δ}(WL) && \displaystyle\frac{Γ⊢Δ}{Γ⊢ω,Δ}(WR) \\ \\ \end{array}
命題記号 ￢∧∨→
『シークエントの解釈』から見りゃわかるやつ。
（記号の解釈と弱化で作れます）
説明なくても明らかなやつ (2)
・論理積 左「 ∧L 」
\begin{array}{lllll} \displaystyle\frac{Γ,ω_A⊢Δ}{Γ,ω_A∧ω_B⊢Δ}(∧L_1) &&\displaystyle\frac{Γ,ω_B⊢Δ}{Γ,ω_A∧ω_B⊢Δ}(∧L_2) \end{array}
・論理和 右「 ∨R 」
\begin{array}{llllllll} \displaystyle\frac{Γ⊢ω_A,Δ}{Γ⊢ω_A∨ω_B,Δ}(∨R_1) && \displaystyle\frac{Γ⊢ω_B,Δ}{Γ⊢ω_A∨ω_B,Δ}(∨R_2) \end{array}
確認が必要な規則 (4)
・否定「 ￢ 」
\begin{array}{lllllll} \displaystyle \frac{Γ⊢ω,Δ}{Γ,￢ω⊢Δ}(￢L) && \displaystyle\frac{Γ,ω⊢Δ}{Γ⊢￢ω,Δ}(￢R) \end{array}
「定理」から取り除く →「前件」で『否定』できる。
「定理」で『否定』する →「前件」から取り除く。
記号の意味を考えると分かると思いますが、
ぱっと見ですぐには分からないかもしれません。
・論理積 右「 ∧R 」
\begin{array}{llllllllll} \displaystyle\frac{Γ_A⊢ω_A,Δ_A \,\,\,\,\,\,\,\,\,\, Γ_B⊢ω_B,Δ_B}{Γ_A,Γ_B⊢ω_A∧ω_B,Δ_A,Δ_B}(∧R) \end{array}
「 Γ_A⊢ω_A,Δ_A であること」と
「 Γ_B⊢ω_B,Δ_B であること」から
『 Γ_A と Γ_B が正しい』なら、
『 ω_A も ω_B も正しい』が導ける。
確認してみるとまあそうだなって感じしますが
これもすぐにはよく分からないかもしれません。
・論理和 左「 ∨L 」
\begin{array}{rlc} \displaystyle\frac{Γ_A,ω_A⊢Δ_A \,\,\,\,\,\,\,\,\,\, Γ_B,ω_B⊢Δ_B}{Γ_A,Γ_B,ω_A∨ω_B⊢Δ_A,Δ_B}(∨L) \end{array}
これも「 ∧R 」と同様ですね。
「 Δ_A と Δ_B のどっちかが正しい」なら
「 ω_A か ω_B のどっちかが正しい」
・論理包含「 → 」
\begin{array}{llllll} \displaystyle\frac{Γ_A⊢ω_A,Δ_A \,\,\,\,\,\,\,\,\,\, Γ_B,ω_B⊢Δ_B}{Γ_A,Γ_B,ω_A→ω_B⊢Δ_A,Δ_B}(→L) &&\displaystyle\frac{Γ,ω_A⊢ω_B,Δ}{Γ⊢ω_A→ω_B,Δ}(→R) \end{array}
左規則は操作的ですね。
直感的にはよく分かんないと思います。
\begin{array}{llllllllllllll} \displaystyle \frac{Γ_A⊢ω_A,Δ_A}{Γ_A,￢ω_A⊢Δ_A}(￢L) \end{array}
\begin{array}{llllllllllll} \displaystyle\frac{Γ_A,￢ω_A⊢Δ_A \,\,\,\,\,\,\,\,\,\, Γ_B,ω_B⊢Δ_B}{Γ_A,Γ_B,￢ω_A∨ω_B⊢Δ_A,Δ_B}(∨L) \end{array}
真理値が「 A→B≡￢A∨B 」であることと
「否定規則 左」「論理和規則 左」から導けますが。
\begin{array}{cccccccccccc} \displaystyle A&B&￢A&&￢A∨B&&A→B \\ \\ 1&1&0&&1&&1 \\ \\ 1&0 &0 &&0 &&0 \\ \\ 0&1 &1 &&1&&1 \\ \\ 0&0 &1 &&1 &&1 \end{array}
右規則は単純
文脈を取り払ってみてみれば、
↓ のは ↑ の言い換えでしかないことが分かると思います。
\begin{array}{llllll} \displaystyle\frac{Γ,ω_A⊢ω_B,Δ}{Γ⊢￢ω_A,ω_B,Δ}(￢R) \end{array}
操作的には「 ￢R 」と「シークエントの解釈」です。
量化記号 ∀ \,\, ∃
『量化記号』を使う場合
「自由変数」「束縛変数」
この辺りを意識する必要があります。
というわけで、ここで念のために記号のおさらい。
↓ の記号の意味を再確認しておきます。
『 ω[t/x] 』
「変数 x 」を「項 t 」に置換した『論理式』
『 ω[y/x] 』
「変数 x 」を「変数 y 」に置換した『論理式』
この入れ替え（置換）によって
『束縛子による束縛は新たに発生しない』
\begin{array}{llllll} \displaystyle ∀x & ω(x) \end{array}
つまり「束縛子 ∀ の影響がある変数 x への置換」
これが起きることは無いとします。
・全称量化「 ∀ 」
\begin{array}{lllllll} \displaystyle\frac{Γ,ω[t/x]⊢Δ}{Γ,∀x \,\, ω⊢Δ}(∀L) && \displaystyle\frac{Γ⊢ω[y/x],Δ}{Γ⊢∀x \,\, ω,Δ}(∀R) \end{array}
・存在量化「 ∃ 」
\begin{array}{lllllllll} \displaystyle\frac{Γ,ω[y/x]⊢Δ}{Γ,∃x \,\, ω⊢Δ}(∃L) && \displaystyle\frac{Γ⊢ω[t/x],Δ}{Γ⊢∃x \,\, ω,Δ}(∃R) \end{array}
意味は「量化記号」の定義通りですが、
「代入」のとこがよく分からないかもしれません。
変数を代入する時の制約
「違う変数を代入するパターン」を考える時
つまりは『変数が取り得る範囲』が違う
\begin{array}{llllll} \displaystyle y&=&x \\ \\ y&≠&x \end{array}
だから中身を特定できないかも？って時
\begin{array}{llll} \displaystyle x&∈&X \\ \\ y&∈&Y \end{array}
\begin{array}{lllllll} \displaystyle X&=&Y \\ \\ X&⊂&Y \end{array}
つまりこのパターンではなく
\begin{array}{lllll} \displaystyle X&⊃&Y \\ \\ X&≠&Y \end{array}
この「全く違う」パターンと
「 Y が持たない要素がある」パターンの時
他の場所 Γ,∀x\,\,ω,∃x\,\,ω,Δ に
『 y は自由変数として出てこない』
つまり「全体に影響を与えない」
そういう制約を付けることで、
\begin{array}{llllll} \displaystyle \displaystyle ω[y/x]&\mathrm{is}&\mathrm{True} &&→&&∀y \,\, ω[y/x] \end{array}
y が『 x の代わりだけをする』上に
「 ω を満たす」ような「任意（全部）の値をとる」
\begin{array}{lllllll} \displaystyle X&=&Y \\ \\ X&⊂&Y \end{array}
このパターンに限定されるようにすれば
\begin{array}{llllll} \displaystyle ∀y \,\, ω[y/x] &&→&&∀x \,\, ω(x) \end{array}
自由変数 y の中身は
結果的に『変数 x の中身も含む』
あるいは『変数 x と一致する』ことになるので
\begin{array}{llllllllll} \displaystyle\frac{Γ⊢ω,Δ}{Γ⊢∀x \,\, ω,Δ}(∀R) && \displaystyle\frac{Γ,ω⊢Δ}{Γ,∃x \,\, ω⊢Δ}(∃L) \end{array}
この導出は正しい、となります。
・代入しても束縛子による新たな束縛は無い
・代入された変数は他のとこに無い
これらの制約が無い場合は
↓ のようなことが起こり得ます。
『変数の数が減って論理式の意味が限定される』
『他の論理式が連動してしまう』
これら「他への影響」という問題を解決した上で
『 x に限定して量化する』
このために必要なあれこれが ↑ になります。
カット規則
これは名前の通りの規則です。
\begin{array}{llllll} \displaystyle \displaystyle\frac{Γ_A⊢ω,Δ_A \,\,\,\,\,\,\,\,\,\, Γ_B,ω⊢Δ_B}{Γ_A,Γ_B⊢Δ_A,Δ_B}(\mathrm{Cut}) \end{array}
役割は『公理 ω\vdash ω 』の除去
まあつまり「省略」のための規則で、
それ以上の意味は特にないんですが、
これは必要不可欠な規則になります。
決して軽視していい規則ではありません。
カット除去定理
↑ の感覚から分かる通り、
カット規則はただ『当たり前を省略』してるだけです。
まあつまり「省略しなかった」としても、
その証明全体は『正しいまま』なので
これは使わなかったとしても証明は行えます。
はい。とまあそういうわけですから、
これは「証明」を行う上で必要不可欠ではありません。
当然の話に聞こえるかもしれませんが、
これが「カット除去定理」の感覚になります。
カット規則とセットで話されることがあるので、
まあなんとなく覚えておきましょう。
『使わなくても良い』けど
『使わないと証明がくっそ長くなる』
そういう事例（1ページ → 宇宙の寿命以上）が確認されてるので。
以上
『LKの推論規則』はこんな感じですね。
