|| LK (論理計算) の意味は初見じゃ分からない
スポンサーリンク
目次
同一律「それはそれ自身であるという当たり前」
代入規則「記号の入れ替えについての規則」
述語論理「実際的な推論を形式化して整理したもの」
LKの推論規則「シークエントと感覚的な証明」
推件式「推論の構造を整理するための道具」
構造規則「シークエントの定義的に当然やれること」
論理規則「述語論理を推件式で翻訳したもの」
論理結合子規則「命題記号の振る舞い」
量化子規則「推件式での量化子の振る舞い」
カット規則「推移する形の証明は省略できる」
カット除去定理「証明可能とカットは無関係」
メタレベルの材料
「LKの推論規則」をきちんと説明するには
\begin{array}{lclcl} \mathrm{Hilbert} && φ∧(φ\to ψ)&\overset{←から→が導かれる}{\vdash} & ψ \\ \\ \mathrm{Gentzen} && φ,φ\to ψ&\overset{ただの置かれる記号}{\vdash} & ψ \end{array}
（ LK の前の推論規則は Modus Ponens のみ）
\begin{array}{ccc} 材料 & \left\{ \begin{array}{lcl} 同一律 && 証明の出発点 \\ \\ 代入規則 && 記号入れ替え時のルール \\ \\ 述語論理 && 論理記号の細かい話 \end{array} \right. \end{array}
こういった知識が必要になります。
（知らないと理解のための障壁が高いかも）
同一律 Identity
これは「推件式」を使う時『最初に来る形』で
\begin{array}{l} A=A &&\Longleftrightarrow&& \displaystyle\frac{ }{A⊢A} \end{array}
「それはそれである」の形式表現になります。
（ A=A は最も基礎的な公理なので名前がある）
代入規則 Substitution Rules
これは「記号の入れ替え」についてのルール集です。
（感覚的な代入での注意事項と許される操作）
\begin{array}{lcl} φ[x/t] &\Longleftrightarrow& 式φの自由変数xを項tに置き換える \\ \\ φ_x[t] &\Longleftrightarrow& 式φの自由変数xを項tに置き換える \\ \\ φ[x:=t] &\Longleftrightarrow& 式φの自由変数xを項tに置き換える \end{array}
「してはならない」ことに気を付けながら
「して良いこと」についてまとめています。
（「同じ記号を使わないようにして」の形式表現）
述語論理 Predicate Logic
これは「命題の中身」を深堀したやつで
（「命題」の定義は『真偽が分かる』という要請のみ）
\begin{array}{lcl} 命題の具体化 && 命題の中身を考える \\ \\ 具体例の提示 && 主張は「～である」という形 \\ \\ 変数が主語なら && 述語が変数の状態を表現 \\ \\ \\ 調査段階 && 真か偽か分かる述語を求める \\ \\ 発見段階 && 量の表現の中で「全て～である」を発見 \\ \\ \\ 精査段階 && 性質を色々調べる \\ \\ 形式化段階 && 述語論理の概形が得られる \end{array}
「LKの推論規則」という記号操作ルールは
ここから得られた「記号表現」を利用しています。
（命題記号 \lnot , ∧,∨,→,⇔ や量化子 \forall , \exists はこれ由来）
LKの推論規則 Logischer Kalkül
|| ヒルベルトの推論規則をより高精度化したもの
\begin{array}{lcl} 各規則の根拠 &→& 局所モデル的意味 \\ \\ メタ的意味だけ &←& \mathrm{LK}の運用 \end{array}
『LKの説明』には「局所モデルレベルの意味」が必要ですが
『LKの運用』では「メタレベルの意味」しか扱いません。
（見かけ上は記号だけを扱い真偽を考えない）
意味の階層
混乱しやすい部分なので改めて整理しておくと
\begin{array}{lcl} メタ的意味 && 実際にはあるが当然すぎて無視 \\ \\ 局所モデル的意味 && 真偽を判断できる段階にある \end{array}
数学における『意味』にはこのような階層があり
（最初の段階や根本的な根拠はメタ的意味）
\begin{array}{lcl} なんでこうなるの？ &\to& 局所モデル的意味が必要 \\ \\ \mathrm{LK}のルールで記号操作 &\to& 局所モデル的意味は不要 \end{array}
「 LK の推論規則（推件式の定義に依存）」では
「局所モデル的意味」が排除されています。
排除できないメタ的意味
「メタレベルの意味」というのは
要は「当たり前すぎる意味」のことで
\begin{array}{ccc} メタ的意味 & \left\{ \begin{array}{l} 記号である \\ \\ 式である \\ \\ Γ\vdash φの形なので推件式である \\ \\ 記号\vdash の左側である\\ \\ 記号 \vdash の右側である \end{array} \right. \end{array}
具体的にはこういったものがメタレベルに該当します。
（これを剥がすとそもそも「記号を扱う」ことが不可能）
メタ的意味の整理
これは大きくは
『記号』の「認識」「存在」「操作」で分類できます。
\begin{array}{lcl} 推件式の操作を行う &\to& 推件式を認識できる \\ \\ &\to& したいことを認識できる \\ \\ &\to& 適用したい規則を認識できる \\ \\ &\to& 推件式が存在する \\ \\ \\ &\to& 用いるを認識できる \\ \\ &\to& 記号を認識できる \\ \\ &\to& 用いる記号を認識できる \\ \\ &\to& 用いる記号が存在する \\ \\ \\ &\to& 記号を任意の位置に置ける \\ \\ &\to& 置きたい位置を認識できる \\ \\ &\to& 記号を適切な位置に置ける \\ \\ \\ &\to& 規則適用の終了を認識できる\\ \\ &\to& 規則適用後の推件式を認識できる \\ \\ &\to& 規則適用後の推件式が存在する \end{array}
具体的にはこういった操作の概形から
（細かくはもっと細分化できるがあまり意味は無い）
\begin{array}{ccc} 分離不可な基礎的意味 & \left\{ \begin{array}{l} 記号である \\ \\ 操作である \\ \\ 推件式である \end{array} \right. \end{array}
「メタ的意味」は抽出することができます。
（形而上の概念に行き着いた時点でひとまずストップ）
そもそも論
従来の「構文」「形式」においては
『意味を取り除いて形だけを取り出す』
\begin{array}{ccc} \left( \begin{array}{l} 私は人間である \\ \\ 人は生き物である \\ \\ 米は食べ物である \end{array} \right) &\to& AはBである \end{array}
こういうことをやってきたわけですが
（この意味が薄まった感じが誤解の原因）
\begin{array}{ccc} A &\to& Aは記号である \end{array}
「意味」は『常に見出されるもの』です。
（直感的な現実認識をベースにするとこれが事実）
\begin{array}{ccc} 取り出された形 &\to& 型である \end{array}
故に「意味が無い状態」というのはあり得ず
\begin{array}{ccc} かなり意味の薄い型 &\to& 記号である \end{array}
最後には必ず「メタ的な意味」が『生じる』ので
『形式化段階』『構文レベル』という領域の実態は
\begin{array}{lcl} メタ的意味 &\to& 真偽を問う意味があまりない \\ \\ 局所モデル的意味 &\to& 確定で真偽が分かる \end{array}
厳密には「意味が無い」のではなく
（実際にメタレベルの意味は排除されない）
\begin{array}{ccc} 私は人間 &\overset{意味を排除する}{\longrightarrow}& AはB && △ \\ \\ 私は人間 &\overset{真偽判定の材料を排除する}{\longrightarrow}& AはB&& 〇 \end{array}
『真偽判定可能性が無い』になります。
（構文化の方向性は意味の排除ではなく真偽の排除）
構造規則 Structure Rules
以上の「方向性（構文レベルへ）」と
「自然言語の振る舞い」から得られた
\begin{array}{ccc} \left( \begin{array}{lcl} Aである& ∧& Bである \\ \\ Aである&∨&Bである \end{array} \right) &\to& A,B \end{array}
『推件式の定義』を根拠として
（推件式で扱う記号は「真と仮定された論理式」のみ）
\begin{array}{l} \mathrm{Permutation} && \displaystyle \frac{L,A,B,R\vdash φ}{L,B,A,R\vdash φ}(\mathrm{PL}) & \displaystyle \frac{Γ\vdash L,A,B,R}{Γ\vdash L,B,A,R}(\mathrm{PR}) \\ \\ \\ \mathrm{Contraction} && \displaystyle \frac{L,A,A,R\vdash φ}{L,A,R\vdash φ}(\mathrm{CL}) & \displaystyle \frac{Γ\vdash L,A,A,R}{Γ\vdash L,A,R}(\mathrm{CR}) \\ \\ \\ \mathrm{Weakening} && \displaystyle \frac{L,A,R\vdash φ}{L,A,B,R\vdash φ}(\mathrm{WL}) & \displaystyle \frac{Γ\vdash L,A,R}{Γ\vdash L,A,B,R}(\mathrm{WR}) \end{array}
この「構造規則」は定められています。
（これの詳細はシークエントの記事を参照してください）
論理規則 Logical Rules
ここからが「推件式の記事の続き」となる部分で
（シークエントの詳細はこの記事では扱いません）
\begin{array}{ccc} \mathrm{Not} && \displaystyle \frac{Γ\vdash L,A}{Γ,\lnot A \vdash L}(\mathrm{\lnot L}) & \displaystyle \frac{A,R\vdash φ}{R\vdash φ, \lnot A}(\mathrm{\lnot R}) \\ \\ \\ \mathrm{And} && \displaystyle \frac{A,B,R\vdash φ}{A∧B,R\vdash φ}(\mathrm{∧L}) & \displaystyle \frac{Γ\vdash L,A \quad Γ\vdash L,B}{Γ\vdash L,A∧B}(\mathrm{∧R}) \\ \\ \\ \mathrm{Or} && \displaystyle \frac{A,R\vdash φ \quad B,R\vdash φ}{A∨B,R\vdash φ}(\mathrm{∨L}) & \displaystyle \frac{Γ\vdash L,A}{Γ\vdash L,A∨B}(\mathrm{∨R}) \\ \\ \\ \mathrm{If} && \displaystyle \frac{R\vdash L,A \quad B,R\vdash L}{A\to B,R\vdash L}(\mathrm{\to L}) & \displaystyle \frac{A,R\vdash L,B}{R\vdash L,A\to B}(\mathrm{\to R}) \end{array}
それぞれ「論理記号の振る舞い」から
（片側のコンテキストが不要なのは転置規則が由来）
\begin{array}{ccc} \mathrm{All} && \displaystyle \frac{L,P(t)\vdash φ}{L,\forall x\,\, P(x) \vdash φ}(\mathrm{\forall L}) & \displaystyle \frac{Γ\vdash L,P(y)}{Γ\vdash L,\forall x \,\, P(x)}(\mathrm{\forall R}) \\ \\ \\ \mathrm{Exist} && \displaystyle \frac{L,P(y)\vdash φ}{L,\exists x \,\, P(x) \vdash φ}(\mathrm{\exists L}) & \displaystyle \frac{Γ\vdash L,P(t)}{Γ\vdash L,\exists x \,\, P(x)}(\mathrm{\exists R}) \end{array}
これらはこのような形で定められています。
（いずれも真仮定論理式と考えれば自然な形）
論理結合子規則 Propositional Rules
以下の規則で特によく分からないのは
\begin{array}{ccc} \mathrm{Not} && \displaystyle \frac{Γ\vdash L,A}{Γ,\lnot A \vdash L}(\mathrm{\lnot L}) & \displaystyle \frac{A,R\vdash φ}{R\vdash φ, \lnot A}(\mathrm{\lnot R}) \\ \\ \\ \mathrm{And} && \displaystyle \frac{A,B,R\vdash φ}{A∧B,R\vdash φ}(\mathrm{∧L}) & \displaystyle \frac{Γ\vdash L,A \quad Γ\vdash L,B}{Γ\vdash L,A∧B}(\mathrm{∧R}) \\ \\ \\ \mathrm{Or} && \displaystyle \frac{A,R\vdash φ \quad B,R\vdash φ}{A∨B,R\vdash φ}(\mathrm{∨L}) & \displaystyle \frac{Γ\vdash L,A}{Γ\vdash L,A∨B}(\mathrm{∨R}) \\ \\ \\ \mathrm{If} && \displaystyle \frac{R\vdash L,A \quad B,R\vdash L}{A\to B,R\vdash L}(\mathrm{\to L}) & \displaystyle \frac{A,R\vdash L,B}{R\vdash L,A\to B}(\mathrm{\to R}) \end{array}
「含意 \to \mathrm{L} 」の部分だと思います。
（他は記号を具体化していくとなんとなく分かる）
\begin{array}{ccc} && \mathrm{Left} & \mathrm{Right} \\ \\ \\ 否定 && 結論を取り除く & 前提を取り除く \\ \\ かつ && 前提の統合 & 結論の統合 \\ \\ または && 前提の分岐 & 結論の選択 \\ \\ ならば && ？ & Aが前提ならBになる \end{array}
『説明（メタレベルの意味）』の段階における定義で
この辺りの話はすんなり理解できると思いますが
（コンテキスト L,R の長さが 1 だと分かり易い）
\begin{array}{ccc}\displaystyle \frac{R\vdash L,A \quad B,R\vdash L}{A\to B,R\vdash L}(\mathrm{\to L}) \end{array}
「記号操作」としては単純でも
（コンテキスト L,R の統合は転置規則で可能）
\begin{array}{ccc} R\vdash L,A \quad B,R\vdash L \end{array}
この『説明』はちょっと難しいと思います。
（これだけ異質に見えるのは正常な感覚）
含意 L だけ逆算で得られている
他の規則は『 ↑ から ↓ を導く』という形で
「自然な解釈」を持ち込むことができる
\begin{array}{ccc}\displaystyle \frac{R\vdash L,A \quad B,R\vdash L}{A\to B,R\vdash L}(\mathrm{\to L}) \end{array}
しかし「含意 L 」に関しては
\begin{array}{ccc} A\to B,R\vdash L &\Longrightarrow& 都合の良い形 \end{array}
『 ↓ から ↑ を得る』という形で定義されているため
\begin{array}{ccc}\displaystyle \frac{R\vdash L,A \quad B,R\vdash L}{A\to B,R\vdash L}(\mathrm{\to L}) \end{array}
『 ↑ から ↓ を得る』という方向では
自然な解釈を得ることができません。
（左の前提部分にあるが出発点）
\begin{array}{lcl} 動機 && 左側にA\to B の形が欲しい \\ \\ 感覚 && 自然な形が作れない \\ \\ 試行 && 似た形を探して￢A∨Bを得る \\ \\ 結論 && 他の規則から形を拝借する \end{array}
これは『構成的に得られる』もので
\begin{array}{ccc} A &B& \lnot A & \lnot B & & A→B & \lnot A∨B \\ \\ 1&1&0&0 && 1 & 1 \\ \\ 1&0&0&1 && 0 & 0 \\ \\ 0&1&1&0 && 1 & 1 \\ \\ 0&0&1&1 && 1 & 1 \end{array}
『真理値の関係』を根拠に
（「転置規則」による並べ替えとコンテキストの統合も）
\begin{array}{ccc} \displaystyle \frac{ \displaystyle \frac{Γ \vdash L,A}{\lnot A,Γ\vdash L \quad B,R\vdash φ}(\mathrm{\lnot L}) }{\lnot A∨B,R\vdash φ }(\mathrm{∨L}) \end{array}
「否定」と「選言（ \mathrm{or} ）」で構成されます。
（これが「含意L」のメタ的な意味になる）
量化子規則 Quantifier Rules
これはまず『変数で定義される』もので
（初期の発想段階では上の P の引数は自由変数）
\begin{array}{ccc} \mathrm{All} && \displaystyle \frac{L,P(t)\vdash φ}{L,\forall x\,\, P(x) \vdash φ}(\mathrm{\forall L}) & \displaystyle \frac{Γ\vdash L,P(y)}{Γ\vdash L,\forall x \,\, P(x)}(\mathrm{\forall R}) \\ \\ \\ \mathrm{Exist} && \displaystyle \frac{L,P(y)\vdash φ}{L,\exists x \,\, P(x) \vdash φ}(\mathrm{\exists L}) & \displaystyle \frac{Γ\vdash L,P(t)}{Γ\vdash L,\exists x \,\, P(x)}(\mathrm{\exists R}) \end{array}
『定数で問題無い形（特に存在Lとか）』が
「項 \mathrm{Term} 」に拡張されています。
自由変数記号の解釈
「推件式」で唐突に置かれることになる
\begin{array}{ccc} L,P(y) &\vdash & φ \end{array}
「自由変数記号 y 」は
いろんな意味でよく分からないので
（下の結論に来る x は量化されたローカル変数）
\begin{array}{ccc} P(y) は真仮定 &\Longleftarrow& 前提は真と仮定される \end{array}
『LKの説明』段階での定義が必要になります。
（メタレベルでの定義が必要になる）
\begin{array}{lcl} 局所モデル段階 && yのドメインは局所モデル内の全て \\ \\ 構文段階 && yはただの変数記号 \end{array}
具体的には「自由変数 y が取り得る範囲」を含む
「代入規則」などの制限が課せられていて
\begin{array}{lcl} \mathrm{LK}の説明 && yのドメインはモデル内全体 \\ \\ \mathrm{LK}の運用 && yは結論で現れない新記号 \end{array}
これらにより y の振る舞いは厳密に定義されています。
（このメタレベルの意味が量化規則の根拠になる）
新記号であるの拡張
「新記号である」を厳密に定義するには
\begin{array}{ccc} \mathrm{Symbols}(Γ\vdash φ) &=& 記号の集合 \end{array}
「推件式を入力とする」形の
『記号抽出写像』を定義する必要があって
\begin{array}{ccc} \mathrm{Symbols}(Γ\vdash φ) &=& \displaystyle \{\vdash \} ∪ \left( \bigcup_{ψ\in Γ} \mathrm{Symbols}(ψ) \right) ∪ \mathrm{Symbols}(φ) \end{array}
定義されたこれを導入することで
「代入」については厳密に定義されます。
（より細かい話は代入規則の記事で扱っています）
記号の入れ替えと規則
「自由変数 y 」での定義では
\begin{array}{ccc} \mathrm{All} && \displaystyle \frac{L,P(t)\vdash φ}{L,\forall x\,\, P(x) \vdash φ}(\mathrm{\forall L}) & \displaystyle \frac{Γ\vdash L,P(y)}{Γ\vdash L,\forall x \,\, P(x)}(\mathrm{\forall R}) \\ \\ \\ \mathrm{Exist} && \displaystyle \frac{L,P(y)\vdash φ}{L,\exists x \,\, P(x) \vdash φ}(\mathrm{\exists L}) & \displaystyle \frac{Γ\vdash L,P(t)}{Γ\vdash L,\exists x \,\, P(x)}(\mathrm{\exists R}) \end{array}
「 P(y) は無条件で真と仮定されてる」ので
（項 t 変数の他に定数の場合も考える）
\begin{array}{ccc} P(y) &\to& \forall x \,\, P(x) \\ \\ P(y) &\to& \exists x \,\, P(x) \end{array}
これらはただの言い換えでしかありません。
（ドメインはモデル定義後の宇宙全体）
量化子規則の結論部分
『結論』側で「定数 c 」で考えてみれば
\begin{array}{ccc} P(c) &\to& \forall x \,\, P(x) && △ \\ \\ P(c) &\to& \exists x \,\, P(x) && 〇 \end{array}
これらがこうなることは直感的に理解できると思います。
（全称化は１つの具体例で保証できない）
\begin{array}{ccc} \displaystyle \frac{Γ\vdash L,P(y)}{Γ\vdash L,\forall x \,\, P(x)}(\mathrm{\forall R}) \\ \\ \\ \displaystyle \frac{Γ\vdash L,P(t)}{Γ\vdash L,\exists x \,\, P(x)}(\mathrm{\exists R}) \end{array}
なのでこれらに関しては
ただ言い換えただけであることがすぐに分かると思います。
（結論をただ他の表現にしただけで内容に変化は無い）
量化子規則と前提部分
問題となるのは
\begin{array}{ccc} \displaystyle \frac{L,P(t)\vdash φ}{L,\forall x\,\, P(x) \vdash φ}(\mathrm{\forall L}) \\ \\ \\ \displaystyle \frac{L,P(y)\vdash φ}{L,\exists x \,\, P(x) \vdash φ}(\mathrm{\exists L}) \end{array}
「前提部分」の規則だと思うんですが
\begin{array}{lcl} \forall \mathrm{L} &\Longleftrightarrow& 使える前提が増える \\ \\ \exists \mathrm{L} &\Longleftrightarrow& P(c)ではなくP(a)で成立し得る \end{array}
これはこのように解釈すれば直感的だと思います。
（存在は定数 c だと他の定数にすり替わる可能性がある）
カット規則 Cut Rule
|| 証明における推移律のようなもの
「証明の省略」を意味する記号操作
\begin{array}{ccc} \displaystyle\frac{ Γ \vdash A \quad A,R\vdash B }{Γ,R \vdash B}(\mathrm{Cut}) \end{array}
見たまま「省略（間を消去）」を意味します。
（これが無いと証明の記述内容が膨大になる）
カット除去定理 Cut-Elimination
|| カット規則は証明可能性とは無関係
「全ての証明からカット規則を除去できる」という主張
\begin{array}{lcl} 具体例 && 実際にカット規則を除去 \\ \\ 一般化 && 機械的な除去手順を抽出 \\ \\ 停止性 && 手順が有限回で終わるか \end{array}
ざっくりとはこのような手順で証明されます。
（各規則の確認が必要でかなり複雑になるため詳細は別記事で）