|| 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の推論規則』の全てになります。
思えば、単純なことしか書かれてはいません。
多いですが。
これら「演繹」の手法は「演繹」ですから、
「正しいかどうか」を確認することができます。
その確認のやり方は単純です。
「シークエントの解釈」から「真理値」を確認するだけ。（大変）
この事実から、「推論規則」のことを、
「トートロジー（恒真命題）の導出法」と言い換えても良いでしょう。
いや、用語を使うと見事に意味わかんなくなりますね。
意味的にはかなり正確になるんですけど。