形式的体系とは何か：証明を厳密に定義する - 記号論理学

形式的体系（formal system）は、証明を数学的対象として厳密に定義するための枠組みです。何が公理であり、どのような規則で新しい定理を導けるかを、曖昧さなく規定します。ゲーデルの不完全性定理を理解するための前提となる重要な概念です。

形式的体系の構成要素

形式的体系は、以下の要素から構成されます。

言語：使用する記号のアルファベットと、式の文法規則。

公理：証明なしに正しいと認める式の集合。

推論規則：式から新しい式を導く規則。

言語

どのような記号を使い、どう式を構成するか。述語論理の言語など。

公理と推論規則

出発点と、そこから進む道筋。証明の構成要素。

形式的体系における証明は、式の有限列 φ₁, φ₂, …, φₙ です。各 φᵢ は次のいずれかです。

公理である。または、それより前の式に推論規則を適用した結果である。

最後の式 φₙ が証明される定理です。

φ₁：公理

φ₂：公理または推論規則の適用

…

φₙ：定理（証明の結論）

良い形式的体系では、公理の集合は帰納的（recursive）である必要があります。帰納的とは、与えられた式が公理かどうかを機械的に判定できることを意味します。

公理スキーマを使う場合、スキーマへの代入例が公理かどうかは判定可能です。たとえば「φ → (ψ → φ) の形の式はすべて公理」というスキーマでは、与えられた式がこの形かどうかをアルゴリズムで判定できます。

ペアノ算術（PA）は自然数を扱う形式的体系です。

言語は 0, S（後者関数）, +, ×, = を含みます。公理は、0 ≠ S(x)、S(x) = S(y) → x = y、加法・乗法の帰納的定義、そして数学的帰納法の公理スキーマです。

ペアノ算術の公理（一部）

∀x (0 ≠ S(x))、∀x∀y (S(x) = S(y) → x = y)、∀x (x + 0 = x)

帰納法公理スキーマ

(φ(0) ∧ ∀x(φ(x) → φ(S(x)))) → ∀x φ(x)（φ は任意の式）

ZFC（ツェルメロ・フレンケル集合論 + 選択公理）は、現代数学の標準的な基礎となる形式的体系です。

言語は ∈（属する）と = だけを含みます。公理は、外延性、空集合、対、和、冪集合、無限、置換、正則性、そして選択公理です。

ほとんどの数学は ZFC の中で形式化できます。「数学の定理を証明する」とは、原理的には「ZFC で証明を構成する」ことです。

形式的体系について重要な性質がいくつかあります。

無矛盾性：矛盾（φ と ¬φ の両方）が証明できないこと。矛盾した体系は無意味です。

完全性：任意の文 φ について、φ か ¬φ のどちらかが証明できること。

決定可能性：任意の文 φ について、φ が証明可能かどうかを判定するアルゴリズムが存在すること。

無矛盾性（最重要）

矛盾がないこと。これがないと体系として成り立たない。

完全性

すべての文が決定される。ゲーデルの定理はこれに関わる。

ゲーデルは、形式的体系の式や証明を自然数でコード化する方法を考案しました。これをゲーデル数化といいます。

各記号に番号を割り当て、式を記号の列として、その列を素数の冪の積としてコード化します。たとえば ∀x P(x) を 2³ · 3⁵ · 5² · 7⁵ · 11³ のような数で表します。

この技法により、「φ が証明可能である」という性質を、自然数の間の算術的関係として表現できます。これがゲーデルの不完全性定理の証明の鍵となります。

次回は、ゲーデルの第一不完全性定理について学びます。