LKの推論規則 Logischer Kalkül


|| LK (論理計算) で戸惑う

最も有名で使われまくってる「推論規則

一階述語論理」で「完全」かつ「健全」

スポンサーリンク

 

 

 


目次

 

記号の意味

   横棒「↑のが↓を導くってことにする」

   論理式「一階述語論理のものに限定する」

   構造規則「左右、名前を省略して書くことにする」


記号と規則

   項「 t とか u を項ってことにする」

   変数「 x とかを変数ってことにする」



規則「シークエントで書かれます」

   同一律「これはこれだっていう当たり前」

   構造規則「シークエントの定義上必ずそうなるやつ」

   命題記号「命題記号を使う上での決まり」

   量化記号「量化記号を使う上でのルール」

   カット規則「証明の省略をして良いっていうやつ」






 

この記事の内容は『シークエント計算

これを理解してないと雰囲気しか分かりません。

ですから、見ていない方は是非とも確認を。

 

 

 

 

 

記号の意味・解釈

 

記号』について 3+3 つ確認します。

 

 

これに加えて、

』に関して 3

変数』に関して 2 つ確認

 

 

11 個はちょっと多いかもしれませんが、

どれも1つ1つはわりと簡単な話なので

覚えるのに難は無いと思います。

 

 

 

 

 

シークエントの記号表現

 

ここが「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の推論規則』はこんな感じですね。