LKの推論規則 Logischer Kalkül


|| LKで戸惑う

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

こいつは「一階述語論理」では「完全」で「健全」です。

スポンサーリンク





目次


記号の意味

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

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

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


記号と規則

   項「ある記号を項ってことにする」

   変数「ある記号を変数ってことにする」



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

   同一律「これはこれだって言ってるやつ」

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

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

   量化記号「量化記号を使う上での決まり」

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







シークエント計算』を理解してないと雰囲気しか分かりません。

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

分かってる方は良いです。




これに関してですが、かなり固い感じがします。

といってもまあ、全てを固く覚える必要はありません。

ただ、かなりたくさんの「規則」があります。(まじで多い)




そんなわけなので、いくつかに分けて見てみましょう。

大きく分けて「記号」と「規則」の 2 つを。






意味、解釈


記号の読み方です。そんだけです。

そんだけですが、やっぱり大事なのできちんとやります。




まず『記号』について、 3+3 つ。

次に『』に関して、 3 つ。

そして『変数』に関して、 2 つ。




11 個はちょっと多いんで、

大きくまとめて 3 つとします。






シークエントで書かれた規則


ここが主役ですね。

↑で定めた記号を使って、規則を書いていきます。




まず『公理』である「同一律」を。

これは決まりというより単なる事実です。




次に『構造規則』について、 3 つ。

その後は『命題記号』に関して、 2+1+2+1 個。

ときたら『量化記号』のことを、 1+1 個。



11 個ですが、大きく分けてこの 3 つ。

基本的に単純な事実の集まりですので、多く考えなくて良いです。




んで最後に『カット規則』をやりましょう。

これは無くても良いですが、あった方が良いやつです。






以上、大きくまとめて「 3+3+1 」つの「規則」を、

まとめて『LKの推論規則』と言います。







記号の意味



論理式について「 3


・『横棒 「 」』の意味↓

「上の論理式」から「下の論理式」が導かれる




・『 ω,ψ 』の意味↓

「一階述語論理」の『論理式』のことです。

(用途から「命題論理」に限定されたりします)




・『 Γ,Δ 』の意味↓

「有限」個( 0 を含む)の「論理式の列」のこと



これは脈絡・文脈(コンテキスト)と言ったりします。

「命題(論理式)」を詳しく説明する文と考えて良いです。

とはいえ、一塊で意味を持つと考えてください。(交換で注意)



例えば「定理(結論となる論理式)を証明する証明文」とかだと、

できる場合もありますが、基本、中身を好きに入れ替えられません。

特に「論理包含」なんかだと、交換は基本できませんので。






構造規則を省略して表す「 3


・『収縮規則』を


「Contraction Left/Right」→『 CL 』『 CR




・『弱化規則』を


「Weakening Left/Right」→『 WL 』『 WR




・『転置規則』を


「Permutation Left/Right」→『 PL 』『 PR




単なる省略ですので、難しく考えずに。

単語の意味と英訳から見てすぐわかります。






項の規則「 3


・文字の宣言『 t

この記号は任意(なんでもいい)の『項』を表します。




・量化したい『 ω[t]

項「 t 」に着目した『論理式 ω 』を表します。




・置換を許可『 ω[s/t]

ω[t] 」の、ある「 t 」を「 s 」で『置換した論理式』

(ぜんぶ置換してるとは限りません)






変数(変項)の規則「 2


・文字の宣言『 x,y

x,y 」は『変数(変項)』を表します。




・自由変数と束縛変数『 ∀,∃

量化子「 ∀,∃ 」で束縛されない変数を『自由変数』と呼びます。






以上で『記号の意味』については終わりです。

ようやく本筋に入れます。







推論規則



同一性の公理 Identity


「これはこれ」っていう前提にしないと話が始まらないやつです。

これをシークエントで書くと↓になります。



\displaystyle\frac{ }{ω⊢ω}



上はなんでも良いので、なにも書かれてません。

なにが来ても横線の下に来る「公理」は正しいので。



それと同じ理由で、基本的に公理はこう書かれます。






構造規則


収縮規則∧,∨ の冪等性」



CL\,\,\,\displaystyle\frac{Γ,ω,ω⊢Δ}{Γ,ω⊢Δ}\,\,\,\,\, \,\,\,\,\,CR\,\,\,\displaystyle\frac{Γ⊢ω,ω,Δ}{Γ⊢ω,Δ}






転置規則∧,∨ の交換律」



PL\,\,\,\displaystyle\frac{Γ_p,ω_A,ω_B,Γ_c⊢Δ}{Γ_p,ω_B,ω_A,Γ_c⊢Δ}\,\,\,\,\, \,\,\,\,\,PR\,\,\,\displaystyle\frac{Γ⊢Δ_p,ψ_A,ψ_B,Δ_c}{Γ⊢Δ_p,ψ_B,ψ_A,Δ_c}






弱化規則∧,∨ の文の解釈」



WL\,\,\,\displaystyle\frac{Γ⊢Δ}{Γ,ω⊢Δ}\,\,\,\,\, \,\,\,\,\,WR\,\,\,\displaystyle\frac{Γ⊢Δ}{Γ⊢ω,Δ}






命題記号


『シークエントの解釈』から

見りゃわかるやつです。(記号の解釈と弱化で作れます)

まずは明らかなやつから 2 つ。




記号の意味から


論理積 左「 ∧L



∧L_1\,\,\,\displaystyle\frac{Γ,ω_A⊢Δ}{Γ,ω_A∧ω_B⊢Δ}\,\,\,\,\, \,\,\,\,\,∧L_2\,\,\,\displaystyle\frac{Γ,ω_B⊢Δ}{Γ,ω_A∧ω_B⊢Δ}






論理和 右「 ∨R



∨R_1\,\,\,\displaystyle\frac{Γ⊢ω_A,Δ}{Γ⊢ω_A∨ω_B,Δ}\,\,\,\,\, \,\,\,\,\,∨R_2\,\,\,\displaystyle\frac{Γ⊢ω_B,Δ}{Γ⊢ω_A∨ω_B,Δ}






確認が必要な規則


否定



¬L\,\,\,\displaystyle\frac{Γ⊢ω,Δ}{Γ,¬ω⊢Δ}\,\,\,\,\, \,\,\,\,\,¬R\,\,\,\displaystyle\frac{Γ,ω⊢Δ}{Γ⊢¬ω,Δ}




言ってることは↓

「前提」で「否定」されれば「結論」として導かれない。

「前提」から無くなれば、その「否定」は「結論」として導ける。



これも記号の意味で考えると分かります。

より厳密に確認したいなら、真理値で確認してみましょう。






論理積 右「 ∧R



∧R\,\,\,\displaystyle\frac{Γ_A⊢ω_A,Δ_A\,\,\,\,\,\,\,\,\,\,Γ_B⊢ω_B,Δ_B}{Γ_A,Γ_B⊢ω_A∧ω_B,Δ_A,Δ_B}




Γ_A⊢ω_A,Δ_A であること」と(and)

Γ_B⊢ω_B,Δ_B であること」から、



Γ_A であり、かつ Γ_B である』なら、

A であり、かつ B でもある』が導ける。




こう見ると、まあそうだなって感じしますよね。



要は「成り立たせるための前提」が「両方とも揃っている」なら、

「どちらかではなく」「両方とも正しくなる」と言って良い、

とまあ、そういうことです。






論理和 左「 ∨L



∨L\,\,\,\displaystyle\frac{Γ_A,ω_A⊢Δ_A\,\,\,\,\,\,\,\,\,\,Γ_B,ω_B⊢Δ_B}{Γ_A,Γ_B,ω_A∨ω_B⊢Δ_A,Δ_B}




∧R 」にならうなら、

「どっちか(結論)が正しい」なら、

「前提もまた、どちらかが正しい」って言える感じです。




実際「 ω_A 」だけ正しくても(「 ω_B 」でも)

Δ_A∨Δ_B 」は成立します(やってることは「弱化」)






論理包含



→L\,\,\,\displaystyle\frac{Γ_A⊢ω_A,Δ_A\,\,\,\,\,\,Γ_B,ω_B⊢Δ_B}{Γ_A,Γ_B,ω_A→ω_B⊢Δ_A,Δ_B}\,\,\, \,\,\,→R\,\,\,\displaystyle\frac{Γ,ω_A⊢ω_B,Δ}{Γ⊢ω_A→ω_B,Δ}




左規則は「 A→B≡¬A∨B 」と、

「否定規則 左」と「論理和規則 左」から導かれます。




右規則は単純です。

文脈を取り払ってみてみれば、

上も下も「ただの言い換え」でしかないことが分かります。






量化記号


ここでは「前提条件」と「制約」があります。

主な内容は「記号の意味」と「自由変数の除去」ですね。

証明文なので、きっちりと「真偽を確定」させます。




再三に渡る「記号の確認」を行います。



・『 ω[x/t]

「項 t 」を「変数 x 」に置換した『論理式』です。




・『 ω[x/y]

「変数 y 」を「変数 x 」に置換した『論理式』です。

x への置き換え)




・制約は『 ω[x/y] 』の『 y 』についてです。

∀R 」と「 ∃L 」の規則で「変数 y 」は「自由じゃありません」






というわけで、準備も終わったので「規則」へ



・全称量化「



∀L\,\,\,\displaystyle\frac{Γ,ω[t]⊢Δ}{Γ,∀x\,ω[x/t]⊢Δ}\,\,\,\,\, \,\,\,\,\,∀R\,\,\,\displaystyle\frac{Γ⊢ω[y],Δ}{Γ⊢∀x\,ω[x/y],Δ}






・存在量化「



∃L\,\,\,\displaystyle\frac{Γ,ω[y]⊢Δ}{Γ,∃x\,ω[x/y]⊢Δ}\,\,\,\,\, \,\,\,\,\,∃R\,\,\,\displaystyle\frac{Γ⊢ω[t],Δ}{Γ⊢∃x\,ω[x/t],Δ}




これは本質的に「シークエントの解釈」と同じです。

なので「量化記号」の定義通りになりますし、

定義通りにやれる場所は「項」でOKですから「自由変数」もOK







カット規則


Cut\,\,\,\displaystyle\frac{Γ_A⊢ω,Δ_A\,\,\,\,\,\,Γ_B,ω⊢Δ_B}{Γ_A,Γ_B⊢Δ_A,Δ_B}



これは名前の通りの規則です。

本質的には『公理 ω→ω 』を除去します。




感覚的にも導けますが、次の操作からも導けます。

ω 」を「 ω,ω 」にしてみてください。



∨L,∧R\,\,\,\displaystyle\frac{Γ_A⊢ω,Δ_A\,\,\,\,\,\,Γ_B,ω⊢Δ_B}{Γ_A,ω,Γ_B⊢Δ_A,ω,Δ_B}




↑の導出方法を見てみると分かる通り、

これは当たり前のように思えて、少々込み入っております。




というのも『カット除去定理』というものがあるのです。



これの意味するところは、

この「カット規則」は「完全かつ健全」な推論規則では、

「カット規則」を用いずに証明ができてしまうというものです。




要はこいつ、「健全かつ完全」で成立する法則なんですよ。

規則っていうより、単なる事実って言う方が近いです。






以上が『LKの推論規則』の全てになります。

思えば、単純なことしか書かれてはいません。

多いですが。




これら「演繹」の手法は「演繹」ですから、

「正しいかどうか」を確認することができます。



その確認のやり方は単純です。

「シークエントの解釈」から「真理値」を確認するだけ。(大変)




この事実から、「推論規則」のことを、

「トートロジー(恒真命題)の導出法」と言い換えても良いでしょう。



いや、用語を使うと見事に意味わかんなくなりますね。

意味的にはかなり正確になるんですけど。