数理論理 | 天游ヶ丘数理学院

概要と対象読者

本単元は、命題論理と一階論理について構文、意味論、形式的証明を定義し、完全性、コンパクト性、Löwenheim–Skolem の定理を証明する。Robinson 算術 Q と Peano 算術 PA、構文の算術化、表現可能性、不完全性、Church の定理へ進み、単純型付きラムダ計算と限定した Curry–Howard 対応を扱う。

量化を含む証明を読み書きすることができ、形式言語、意味論、証明体系の関係を定義と証明に基づいて学びたい数学専門課程の読者を対象とする。

到達像

必修の記事を学んだ読者は、次の事柄を実行することができる。

命題論理と一階論理の構文、意味論、証明体系を別々に定義し、代入補題、健全性、完全性を証明することができる。
冠頭標準形と Skolem 化を構成し、論理的同値と充足可能性の同値を区別することができる。
Henkin 拡大と項モデルから完全性を証明し、コンパクト性と Löwenheim–Skolem の定理を導くことができる。
Robinson 算術 Q と Peano 算術 PA を定義し、Gödel 符号化、構文操作の原始再帰性、表現可能性、証明述語、対角線補題を構成することができる。
Gödel–Rosser の第一不完全性定理、第二不完全性定理、Church の定理を、各定理の理論に関する仮定を明示して証明することができる。
直観主義命題論理、単純型付きラムダ計算、含意断片の Curry–Howard 対応を定義し、型保存と局所的な対応を証明することができる。

展望の記事を選んで学んだ読者は、一階論理の意味論的完全性と算術理論の構文的不完全性について、対象となる理論と量化の範囲を比較することができる。また、導出可能性条件から Löb の定理を導き、理論が自分の証明可能性を内部で扱うことの限界を説明することができる。

区分

必修は、命題論理と一階論理の構文・意味論・証明体系から完全性とコンパクト性を導く。Q と PA、算術化、表現可能性、対角線補題、不完全性、Church の定理へ進み、単純型付きラムダ計算と限定した Curry–Howard 対応を扱う。28記事はいずれも必修である。

展望は、一階論理の意味論的完全性と、有効に公理化された算術理論の構文的不完全性について、対象となる理論と量化の範囲を比較する。さらに、導出可能性条件から Löb の定理を導き、証明可能性を理論の内部で扱うことの限界を見る。必修ではなく、関心に応じて選んで読むことができる。

前提知識

必修区分は、集合と論理の発展・応用を前提とする。命題、量化子、意味論的な真偽、形式的な推論を用いる。計算理論の区分全体は前提とせず、次の三つの接続だけを記事単位で用いる。

Gödel 符号化と有限列、構文操作の原始再帰性、算術における表現可能性では、計算可能関数を用いる。
本質的決定不能性と Church の定理では、計算可能帰着を用いる。
単純型付きラムダ計算では、型なしラムダ計算を用いる。

このほか、命題論理の構文と意味論と一階論理の構文では帰納法と再帰的な定義を用いる。一階論理の構文が有限項構文の集合性を証明する箇所では、集合の存在原理が与える対・和・冪・分出・置換の存在原理を前提として用いる。本単元では ZF・ZFC の公理を体系的に扱わない。商構造と項モデルには同値関係と商を用い、Henkin 拡大と Skolem 化には選択公理と Zorn の補題を用いる。Henkin 拡大では、さらに超限帰納法と超限再帰、基数とアレフ、基数算術を用いる。Löwenheim–Skolem の定理では、等濃度と可算性、基数とアレフ、基数算術を用いる。

学習の順序と理由

必修の28記事では、命題論理の構文・意味論・標準形・Boolean 代数・証明体系を整えた後、一階論理の構文、充足関係、代入、理論、標準形、証明体系へ進む。Henkin 拡大と項モデルによって完全性を証明してから、コンパクト性と Löwenheim–Skolem の定理を導く。

続いて Robinson 算術 Q と Peano 算術 PA を定義し、コンパクト性を Peano 算術の非標準モデルの存在へ適用する。不完全性定理の証明鎖では、有限列の符号化、構文操作の原始再帰性、表現可能性、証明述語、対角線補題を順に構成する。この順序により、証明可能性を表す算術式が何を符号化し、どの理論内で何を証明するかを追跡することができる。

第一不完全性定理と第二不完全性定理を証明した後、本質的決定不能性と Church の定理を扱う。最後に直観主義論理、単純型付きラムダ計算、限定した Curry–Howard 対応を扱う。展望の2記事は必修ではなく、完全性と不完全性の比較および Löb の定理を扱うために選んで読むことができる。

各記事の内容

次の一覧は学習順に並んでいる。第1項から第28項までが必修であり、第29項と第30項が任意の展望である。

命題論理の構文と意味論命題変数と結合子から論理式を帰納的に定め、構造帰納法を用いて付値と意味を定義する。充足可能性、恒真性、意味論的帰結を区別する。前提は帰納法と再帰的な定義である。
命題論理の標準形各命題論理式を選言標準形および連言標準形へ変形する。すべての真理関数を論理式で表すことができることを証明し、真理値表による恒真性の決定手続きを導く。前提は命題論理の構文と意味論である。
Boolean 代数 Boolean 代数を定義し、論理式を意味論的同値で割った代数が命題変数上の自由 Boolean 代数になることを証明する。評価を Boolean 代数の準同型として記述する。前提は命題論理の構文と意味論と同値関係と商である。
命題論理の証明体系古典命題論理の Hilbert 型体系を一つ固定し、仮定からの導出と証明可能性を定義する。演繹定理と健全性を証明し、有限個の前提に対する完全性を真理表に対応する導出として構成する。命題変数の集合に濃度の制限を置かず、Zorn の補題によって極大無矛盾集合を取り、任意の前提集合に対する完全性とコンパクト性を証明する。前提は命題論理の標準形と選択公理と Zorn の補題である。
一階論理の構文関数記号、関係記号、定数記号と等号をもつ一ソートの一階言語を定め、項、論理式、文を帰納的に定義する。自由変数と束縛変数を構文的に区別し、束縛変数の名前だけが異なる論理式のアルファ同値を定義する。前提は帰納法と再帰的な定義と集合の存在原理である。
一階構造と充足関係空でない台集合をもつ一階構造と変数割当てを定義し、項の解釈と Tarski の充足関係を帰納的に構成する。真理、充足可能性、妥当性、意味論的帰結を区別し、アルファ同値な論理式の充足が一致することを証明する。前提は一階論理の構文である。
代入補題変数捕獲を避ける項および論理式の代入を定義する。項の解釈と充足関係が代入に関して保存されることを、項と論理式の構造に関する帰納法で証明する。前提は一階論理の構文と一階構造と充足関係である。
理論とモデル文の集合として理論を定義し、モデル、充足可能性、意味論的帰結、完全理論を区別する。同型写像に関する充足関係の不変性を証明し、群、順序、算術の公理化を例として検証する。前提は一階構造と充足関係である。
一階論理の標準形と Skolem 化束縛変数を標準化し、一階論理式を冠頭標準形へ同値変形する。新しい関数記号を加える Skolem 化を定義し、元の式との論理的同値ではなく、拡大と縮約を通じて充足可能性が同値になることを証明する。証人を与える関数を選ぶ際に用いる選択原理を明示する。前提は代入補題、理論とモデル、選択公理と Zorn の補題である。
一階論理の証明体系一階論理の Hilbert 型体系を一つ固定し、仮定からの導出を定義する。等号規則と量化規則の変数条件を明示し、演繹定理と健全性定理を証明する。構文的無矛盾性を定義し、矛盾文を用いる形との同値と、モデルをもつ前提集合が構文的に無矛盾であることを証明する。前提は代入補題と理論とモデルである。
無矛盾性と Henkin 拡大構文的無矛盾性の定義は一階論理の証明体系から引用する。数学の基礎が与える、任意の集合と等濃な基数の存在および無限基数の和・積を用いて、有限記号列、構文対象、Henkin 拡大後の言語の濃度を評価する。同単元の超限再帰と超限帰納法を用いて証人定数を順次加え、無矛盾性を保つ Henkin 理論を構成する。Lindenbaum の補題により、極大無矛盾な Henkin 理論へ拡大する。前提は一階論理の証明体系、選択公理と Zorn の補題、超限帰納法と超限再帰、基数とアレフ、基数算術である。
項モデルと完全性定理 Henkin 理論の閉項を、証明可能な等号が定める合同関係で割って項モデルを構成する。演算と関係の定義が代表元の選び方によらないこと、真理補題、モデル存在定理、完全性定理を証明する。前提は無矛盾性と Henkin 拡大と同値関係と商である。
コンパクト性定理一階論理のコンパクト性定理を完全性定理から導く。無限モデルの存在と、有限構造全体を一階理論のモデル類として公理化することができないことへ応用する。前提は項モデルと完全性定理である。
Löwenheim–Skolem の定理言語の濃度を明示し、充足可能な理論に対する小さいモデルの存在を項モデルの濃度評価から証明する。無限モデルをもつ理論に対する上方のモデル存在形をコンパクト性から導く。初等部分構造としての下方の定理はモデル理論で扱う。前提は項モデルと完全性定理、コンパクト性定理、等濃度と可算性、基数とアレフ、基数算術である。
Robinson 算術 Q と Peano 算術 PA 算術の一階言語を定め、有限公理化された Robinson 算術 Q と、帰納法公理スキーマをもつ Peano 算術 PA を定義する。標準モデルが両理論のモデルであることを確認し、Q が帰納法を含まないことを明示する。固定した標準数詞に関する加法と乗法の計算を Q の有限導出へ移す補題も証明する。前提は理論とモデルである。
Peano 算術の非標準モデル標準モデルの完全理論に、新しい定数が各標準数詞より大きいことを述べる文を加える。有限充足可能性とコンパクト性から、標準モデルと初等同値で、Peano 算術を満たす非標準モデルを構成する。前提はRobinson 算術 Q と Peano 算術 PAとコンパクト性定理である。
Gödel 符号化と有限列自然数の有限列を自然数へ符号化し、成分の取得、連結、長さの計算を自然数上の関数として定義する。符号化と復号に用いる関数および関係が原始再帰的であることを証明する。記号と論理式の符号化は構文操作の原始再帰性で扱う。前提は計算可能関数である。
構文操作の原始再帰性算術の言語について、記号、項、論理式、文、代入、導出を Gödel 符号の集合および関数として定義する。各符号が正しい構文を表すかを判定する関係と、代入や証明検査に用いる構文操作が原始再帰的であることを証明する。前提はGödel 符号化と有限列、計算可能関数、代入補題である。
算術における表現可能性自然数上の関数と関係を算術式で表現することを定義する。初期関数、合成、原始再帰に関する構成を追い、原始再帰関数および原始再帰関係が Robinson 算術 Q で各入力の標準数詞について表現されることを証明する。あわせて、有界量化子と Δ₀ 論理式・Σ₁ 論理式の類を定義し、数詞を代入した Δ₀ 文の真偽を Robinson 算術 Q が決定することを証明する。前提はGödel 符号化と有限列、Robinson 算術 Q と Peano 算術 PA、計算可能関数である。
算術化の PA 内での形式化 Peano 算術 PA の内部で有限列の符号化と原始再帰関数を扱うことができるようにする。中国剰余定理を PA 内で証明して表符号の存在を導き、長さ、成分、連結、末尾追加の法則を証明する。原始再帰関数の全域性と定義方程式が PA の定理であることを示し、数詞と閉項の符号および代入可能性の判定を PA の内部で扱う。前提はRobinson 算術 Q と Peano 算術 PA、Gödel 符号化と有限列、構文操作の原始再帰性、算術における表現可能性である。
証明述語と証明可能性述語公理集合を計算可能に列挙することができ、Robinson 算術 Q を含む一階算術理論 T を固定する。公理の列挙と証明列を同時に符号化して原始再帰的な証明関係を定義し、証明可能性述語と T の無矛盾性を表す算術文を構成する。標準証明述語の Σ₁ 性、証明関係の肯定否定双方の数詞ごとの表現可能性、具体的証明の内部化、および証明符号の合成関数の外的な閉性を証明する。前提は構文操作の原始再帰性、算術における表現可能性、一階論理の証明体系である。
対角線補題と Tarski の定理式へ自己の Gödel 符号を代入する関数の表現可能性から対角線補題を証明する。標準モデルで真である算術文の集合を算術式によって定義することができないという Tarski の定理を導く。前提は算術における表現可能性である。
Gödel–Rosser の第一不完全性定理公理集合を計算可能に列挙することができ、Robinson 算術 Q を含む一階算術理論 T について Gödel 文を構成し、T の無矛盾性から Gödel 文の非証明を、T の1-無矛盾性からその否定の非証明を導く。Rosser 文を構成し、T の無矛盾性だけから、T が Rosser 文とその否定のいずれも証明することができないことを証明する。前提は対角線補題と Tarski の定理、証明述語と証明可能性述語、算術における表現可能性である。
導出可能性条件と第二不完全性定理公理集合を計算可能に列挙することができ、Peano 算術 PA を含む一階算術理論 T の標準的な証明可能性述語について、Hilbert–Bernays–Löb の導出可能性条件を証明する。T の無矛盾性を仮定し、T が自身の無矛盾性を表す文を証明することができないことを導く。Robinson 算術 Q を含むが Peano 算術 PA を含まない理論は扱わない。前提はGödel–Rosser の第一不完全性定理、証明述語と証明可能性述語、一階論理の証明体系、算術化の PA 内での形式化、算術における表現可能性である。
本質的決定不能性と Church の定理 Robinson 算術 Q の本質的決定不能性を証明する。一階論理の完全性と計算可能帰着を用いて、一階論理の妥当性と証明可能性を判定する手続きが存在しないという Church の定理を導く。前提はGödel–Rosser の第一不完全性定理、計算可能帰着、項モデルと完全性定理である。
直観主義論理排中律を採用しない直観主義命題論理の自然演繹体系と Kripke 意味論を定義する。導出がすべての Kripke モデルで妥当であることを証明し、古典命題論理では妥当であるが直観主義命題論理では妥当でない論理式の反例を構成する。前提は命題論理の証明体系である。
単純型付きラムダ計算基本型と関数型、型付きラムダ項、型付け文脈、型付け判断を定義する。変数捕獲を避ける代入に関する補題と型保存定理を証明し、型なしラムダ計算では型付けすることができない項を例示する。正規化は扱わない。前提は型なしラムダ計算である。
Curry–Howard 対応直観主義命題論理の含意断片を単純型付きラムダ計算へ対応させる。含意の導入と除去がラムダ抽象と関数適用に対応すること、およびベータ簡約が含意の局所的な迂回の除去に対応することを証明する。正規化と強正規化は証明論で扱う。前提は単純型付きラムダ計算と直観主義論理である。
完全性と不完全性一階論理の意味論的完全性が任意の理論について意味論的帰結と形式的導出の一致を述べることを確認する。Robinson 算術 Q を含む一階算術理論の構文的不完全性と、Peano 算術 PA を含む理論が自身の無矛盾性を表す文を証明することができないことを、対象となる理論と量化の範囲を比較する。三つの定理が両立する理由を、証明されない文の否定を満たすモデルの存在によって説明する。前提は項モデルと完全性定理、Gödel–Rosser の第一不完全性定理、導出可能性条件と第二不完全性定理である。
Löb の定理 Hilbert–Bernays–Löb の導出可能性条件から Löb の定理と、その仮定と結論を理論の内部で述べた形を証明する。自分自身が証明可能であると述べる文が実際に証明可能であることを導き、第二不完全性定理を系として導き直す。理論が、自分の証明しない文について証明可能性から真理への含意を証明することができないことを示す。前提は導出可能性条件と第二不完全性定理と対角線補題と Tarski の定理である。

証明責務と評価

本単元は、前提知識として掲げた結果を既知として、命題論理の完全性、一階論理の代入補題・健全性・完全性・コンパクト性、Löwenheim–Skolem の定理、Gödel–Rosser の第一不完全性定理、第二不完全性定理、Robinson 算術 Q の本質的決定不能性、Church の定理までの証明鎖を必修の記事で完結させる。各記事は、主張する結果の証明を外部文献へ委ねない。単純型付きラムダ計算では型保存までを証明し、正規化と強正規化は扱わない。Curry–Howard 対応は含意断片と局所的な迂回の除去に限定する。

評価では、定義の再現、構造帰納法、Henkin 拡大と項モデルの構成、有限充足可能性の検証、Gödel 符号による構文操作、理論 T に課す仮定の判定を求める。完全性と不完全性については、意味論と構文、任意の理論と算術理論、外部からの量化と理論内部の表現を区別して説明することを求める。

不完全性の証明鎖では、計算可能関数、符号化関数の原始再帰性、Robinson 算術 Q における各入力の標準数詞についての表現可能性、証明述語、対角線補題を順に扱う。後続の記事は、先行する記事が証明した範囲の結果だけを用いる。

本単元が扱う範囲と扱わない範囲

初等部分構造、Tarski–Vaught 判定法、Skolem 包、非標準モデルの初等埋め込みと初等拡大による比較、量化子消去、型、飽和性、圏別性、安定性理論、有限モデル理論、記述計算量は扱わない。これらはモデル理論が扱う。
複数の演繹体系の証明変換、自然演繹の正規化、シークエント計算のカット除去、単純型付きラムダ計算の強正規化、Gentzen の無矛盾性証明、証明論的順序数は扱わない。これらは証明論が扱う。
オートマトン、形式言語、Turing 機械、型なしラムダ計算、計算可能関数、停止問題、計算可能帰着、計算量理論は扱わない。これらは計算理論が扱う。
一般の束と Boolean 代数、イデアル、フィルター、Stone 双対性、フレーム、locale は扱わない。これらは束論が扱う。
一般の指標と項代数、自由代数、等式論理、Birkhoff の HSP 定理は扱わない。これらは普遍代数が扱う。
順序数、超限帰納法、超限再帰、選択公理とそれに同値な命題、任意の集合と等濃な基数の存在、および基数算術の一般論は扱わない。これらは数学の基礎が扱う。本単元は、これらの結果を一階言語の構文、Henkin 拡大、およびモデルの濃度評価へ適用する。
ZF と ZFC を一階の形式理論として定式化すること、累積階層と正則性、反映原理、初等部分モデル、Mostowski 崩壊、構成可能宇宙、および集合論のモデルと相対無矛盾性は扱わない。これらは公理的集合論が扱う。
多ソート論理、高階論理、様相論理の体系的な理論は扱わない。本単元は、等号を含む一ソートの古典一階論理、直観主義命題論理、単純型付きラムダ計算に限定する。

前後の単元との関係

前段の E15 計算理論は、構文の算術化と表現可能性に必要な計算可能関数、Church の定理に必要な計算可能帰着、単純型付きラムダ計算に必要な型なしラムダ計算を供給する。本単元は、オートマトン、形式言語、Turing 機械、停止問題および計算量理論を扱わず、必要な結果だけを記事ごとの前提として用いる。

後続の F8 証明論は、本単元が扱う証明体系、直観主義命題論理、型保存および含意断片の Curry–Howard 対応を前提として、証明変換、自然演繹の正規化、シークエント計算のカット除去および単純型付きラムダ計算の強正規化へ進む。本単元は、正規化、カット除去および強正規化を扱わない。

後続の F39 モデル理論は、本単元の一階論理、コンパクト性および Peano 算術の非標準モデルを前提として、初等部分構造、初等同値、超積、型および飽和性へ進む。本単元は Löwenheim–Skolem の定理をモデル存在の形で扱い、初等部分構造としての下方 Löwenheim–Skolem の定理を扱わない。

§E16数理論理全30項目

展望