証明可能性述語と無矛盾性の文

定義 4.2（「ゲーデルの不完全性定理」§4）

$T$ を帰納的公理化可能な理論とする。自然数の関係

\mathrm{pf}_T=\{(m,n)\ :\ m\ \text{は、ゲーデル数}\ n\ \text{の論理式の}\ T\ \text{における証明の符号}\}

はアルゴリズムで判定できる。(B1) によりこれを表現する論理式 $\mathrm{Pf}_T(y,x)$ を 1 つ固定し、

\mathrm{Prov}_T(x)\ :\equiv\ \exists y\,\mathrm{Pf}_T(y,x)

を証明可能性述語という。また $\bot$ を閉論理式 $0=S0$ （ $Q$ が (Q1) から否定を証明する偽な文）とし、

\mathrm{Con}_T\ :\equiv\ \neg\mathrm{Prov}_T(\overline{\#\bot})

を $T$ の無矛盾性を表す文という。

閉包の状態

定義

定義は閉包の起点です（証明を要しません）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。