incomp - 41semicolon/41semicolon.github.io GitHub Wiki

定理と事実

Th.Ga: 算術的体系は健全なら不完全

上記は以下から導出できる:

Fact.G₁: 算術ではexpressibleな数集合の補集合はexpressible
Fact.G₂: 算術ではexpressibleな数集合のスター集合はexpressible
Fact.G₃: 算術ではPはexpressible.
Lem.G: 算術ではPc*がexpressible.
Lem.D: expressibleな任意の数集合にはゲーデル文が存在する.
Lem.G: Pc*がexpressibleな健全な体系には真だが証明できない文が存在する.
Lem.G: 真だが証明できない文が存在する健全な体系は不完全である.

Th.Gb: 算術的体系はω無矛盾なら不完全

上記は以下から導出できる:

Fact.Σ₀a: 算術はΣ₀完全.
Fact.PΣ₁: P及びP*はΣ₁.
Lem.Σ₀Σ₁: Σ₀完全な体系ではΣ₁集合はenumerable.
Lem.ω: ω無矛盾な体系でenumerableな数集合はrepresentable.
Lem.ps: 無矛盾な体系でP*がrepresentableなら不完全.

Th.Gc: Ω₄,Ω₅を拡大した算術的体系は無矛盾なら不完全

上記は以下から導出できる:

Lem.RP: R*がP*からseparatableな無矛盾な体系は不完全
Lem.S: Ω₄,Ω₅の文が定理な体系はロッサー体系.
(補足)Cor: (Q),(R),PAはロッサー体系.

トピック

言語表現を持たないこと: 言語表現の濃度はℵ₀である一方, 数集合の濃度はℵ₁であるため, 全ての数集合に言語表現を対応付けることはできない. つまり expressibleでない数集合も存在するし, representableでない数集合も存在するし, definable でない数集合も存在する.

メタ言語で集合を言及する: 数集合/数関係をメタ言語を使った内包で言及することがある（e.g. 真なる文のゲーデル数の集合, 定理のゲーデル数の集合...）. その際, 対応する言語表現が存在するかには常に注意が必要. 言語表現が存在すればメタ言語を使った言及（各種数式も補助的に使用）は単なる略記であり, 使用に問題はない. e.g.「Σ₀文のゲーデル数の集合」,「x∈A & Pow(x)」.

ゲーデル符号化の選択: アルファベットが13種類であるなら, 記号列を13進数表記とみなすゲーデル数化が最も自然であるが, 例えば10進数表記と対応させるような(1to1でない)ゲーデル数化も可能. 13種類をそれぞれ 0,1,2,3,4,5,6,7,89,889,8889,88889,888889 に対応付け連結させればよい. この𝑔は全射ではないが単射である. 非全射性: 9や99には逆元が存在しない. 単射性: 上記13の（長さのことなる）部分をトークンと呼ぶと10進表現のトークン長・トークン列は一意に決まる. 記号列とトークン列は単射なので, 単射性が確かめられる.

べき判定とべき関係: 「nは13のべきである」という述語が算術的/Σ₁だからといって, 「nは13のm乗である」という関係が算術的/Σ₁だとは直ちには言えない. 前者は構文的な性質から容易に確かめられるのに対し, 後者はβ関数の存在などを経由して確かめられる.

決定不能な文 (H 𝑔(H)): HがPc*をexpressするならこの文は真だが証明できない。健全な体系ではこれは決定不能な文となる.

決定不能な文 ∀v₂¬A(a̅,v₂): AがP*をenumerateし、体系がω無矛盾性だと仮定するならaを∀v₂¬A(v₁,v₂)のゲーデル数として, この文は決定不能な文となる. さらにこの文はゲーデル文であり, さらにω不完全な文の例をも与える.