導出可能性条件と可証性論理

Ref:

Remark:

$ \mathbf{D1} \colon T \vdash \varphi \implies T \vdash \mathrm{Pr}_T({\ulcorner \varphi \urcorner})

$ \mathbf{D2} \colon T \vdash \mathrm{Pr}_T({\ulcorner \varphi \to \psi \urcorner}) \to (\mathrm{Pr}_T({\ulcorner \varphi \urcorner}) \to \mathrm{Pr}_T({\ulcorner \phi \urcorner}))

$ \mathbf{D3} \colon T \vdash \mathrm{Pr}_T({\ulcorner \varphi \urcorner}) \to \mathrm{Pr}_T({\ulcorner \mathrm{Pr}_T({\ulcorner \varphi \urcorner}) \urcorner})

$ \mathbf{\Sigma_1C} \colon T \vdash \sigma \implies T \vdash \mathrm{Pr}_T({\ulcorner \sigma \urcorner})．ただし$ \sigmaは$ \Sigma_1文

形式化されたΣ₁完全性定理

$ \mathbf{M}: T \vdash \varphi \to \psi \implies \mathrm{Pr}_T({\ulcorner \varphi \urcorner}) \to \mathrm{Pr}_T({\ulcorner \psi \urcorner})

単調性Monotoneを表す．/ 単調性条件M

Remark:

$ Tの可証性述語$ \mathrm{Pr}_T(x)は全て$ \bf D1を満たす．

Def: 無矛盾性を表す文のとり方について

$ \mathrm{Con}_T \equiv \lnot \mathrm{Pr}_T(\ulcorner 0=1 \urcorner)

$ \mathrm{Con}^\mathrm{S}_T \equiv \lnot (\mathrm{Pr}_T(\ulcorner \varphi \urcorner) \land \lnot \mathrm{Pr}_T(\ulcorner \lnot\varphi \urcorner))

$ \varphiは任意の算術の論理式

Thm: Löbの定理

$ \mathrm{Pr}_T(x)が$ \bf D2,D3を満たすなら，任意の論理式$ \varphiに対し$ T \vdash \mathrm{Pr}_T(\ulcorner \varphi \urcorner) \to \varphi \iff T \vdash \varphi

Cor: Löbの定理から第2不完全性定理を導く

$ \bf D2,D3を満たす$ \mathrm{Pr}_T(x)に対し，$ Tが無矛盾なら$ T \nvdash \lnot\mathrm{Pr}_T(\ulcorner 0=1 \urcorner)．すなわち$ T \nvdash \mathrm{Con}_T．

proof

対偶を示す．

$ T \vdash \mathrm{Con}_Tなら$ Tは矛盾する

$ T \vdash \mathrm{Con}_Tならば$ T \vdash \mathrm{Pr}_T(\overline{\ulcorner 0=1 \urcorner}) \to 0=1．

Löbの定理より$ T \vdash 0=1となる．

よって$ Tは矛盾する．

Thm

1. Rosser証明可能性述語$ \mathrm{Pr}^\mathrm{Ro}_T(x)は$ \bf D2と$ \bf D3を同時に満たすことはない．

2. ただし，$ \bf D2または$ \bf D3の片方だけを満たすようにRosser可証性述語を構成することは出来る．

proof 1.:

Kreiselの注意より$ T \vdash \lnot \mathrm{Pr}^\mathrm{Ro}_T(\ulcorner 0 = 1 \urcorner)．

もし$ \mathrm{Pr}^\mathrm{Ro}_T(x)は$ \bf D2と$ \bf D3を同時に満たしているなら，Löbの定理から第2不完全性定理を導くから$ T \nvdash \lnot \mathrm{Pr}^\mathrm{Ro}_T(\ulcorner 0 = 1 \urcorner)となっておかしい．

proof 2.:

$ \bf D2の場合はC.Bernardi, F. Montagna, "Equivalence relations induced by extensional formulae: classification by means of a new fixed point property"

導出可能性条件D2を満たすRosser証明可能性述語が存在する

$ \bf D3の場合はT. Arai; "Derivability conditions on Rosser's provability predicates"

導出可能性条件D3を満たすRosser証明可能性述語が存在する

Cor

$ \bf D2または$ \bf D3の片方を満たすだけでは$ T \nvdash \lnot\mathrm{Pr}_T(\ulcorner 0=1 \urcorner)を一般には導くことは出来ない．

Remark:

$ \bf D2を満たせば$ \bf Mは満たされる．

導出可能性条件D2から単調性条件Mを導く

$ \bf \Sigma_1Cを満たせば$ \bf D3は満たされる．

形式化されたΣ₁完全性定理から導出可能性条件D3を導く

Thm

$ \bf M, D3を同時に満たすRosser証明可能性述語が存在する．

すなわち，$ \bf Mと$ \bf D3を満たすなら$ T \nvdash \lnot\mathrm{Pr}_T(\ulcorner 0=1 \urcorner)を一般には導くことは出来ない．

ただし，$ \bf Mと$ \bf D3を満たすなら，ある算術の文$ \sigmaが存在して$ T \nvdash \lnot(\mathrm{Pr}_T(\ulcorner \sigma \urcorner \land \mathrm{Pr}_T(\ulcorner \lnot \sigma \urcorner))を導く．

proof

T. Kurahashi; "Rosser Provability and the Second Incompleteness Theorem"

Cor:

$ \bf D2を満たせば，$ \mathrm{Con}_Tと$ \mathrm{Con}^S_Tが同値になる．

remark:

すなわち，無矛盾性を表す文のとり方によって第2不完全性定理は成立したり成立しなかったりする．

Thm

1. $ \mathrm{Pr}_T(x)が$ \bf \Sigma_1Cを満たせば，$ T \nvdash \mathrm{Con}^S_T．

2. $ \bf \Sigma_1Cを満たして$ T \vdash \mathrm{Con}_Tとなる$ \Sigma_1可証性述語$ \mathrm{Pr}_T(x)が存在する．

proof:

1.: R. G. Jeroslow; "Redundancies in the Hilbert–Bernays Derivability Conditions for Gödel's Second Incompleteness Theorem"

2.: A. Mostowski; "Thirty Years of Foundational Studies Lectures on the Development of Mathematical Logic and the Study of the Foundations of Mathematics in 1930–1964"