証明可能性論理GLにおける公理Lの必要性

$ \sf PAの再帰的可算な拡大理論$ T，任意の論理式$ \varphi,\psiについて次が成り立つ．

D1. $ T \vdash \varphi$ \implies$ T \vdash \mathrm{Pr}_T \left(\overline{\ulcorner \varphi \urcorner}\right)

D2. $ T \vdash \mathrm{Pr}_T \left( \overline{\ulcorner \varphi \to \psi \urcorner} \right) \to \left( \mathrm{Pr}_T \left( \overline{\ulcorner \varphi \urcorner} \right) \to \mathrm{Pr}_T \left( \overline{\ulcorner \psi \urcorner} \right) \right)

D3. $ T \vdash \text{Pr}_T\left( \overline{\ulcorner \varphi \urcorner}\right) \to \text{Pr}_T\left(\overline{\ulcorner\mathrm{Pr}_T\left(\overline{\ulcorner\varphi\urcorner}\right)\urcorner}\right)

Def. $ \mathsf{GL}

公理図式

$ \sf Taut: 命題論理のトートロジー

$ \mathsf{K}: $ \Box(\Phi \to \Psi) \to (\Box\Psi \to \Box\Psi)

$ \mathsf{L}: $ \Box(\Box \Phi \to \Phi) \to \Box\Phi

推論規則

$ \rm mp: $ \vdash_\mathsf{GL} \varphi \to \psiかつ$ \vdash_\mathsf{GL} \varphiなら$ \vdash_\mathsf{GL} \psi

$ \rm nec: $ \vdash_\mathsf{GL} \varphiなら$ \vdash_\mathsf{GL} \Box\varphi

Thm.

$ \vdash_\mathsf{GL} \Box\varphi \to \Box\Box\varphi

すなわち$ \sf GLは公理図式$ \mathsf{4}:\Phi \to \Box\Box\Phiを含む．

Obsv

$ \Boxを証明可能性述語と捉えれば

$ \mathrm{nec}は導出可能性条件D1に対応．

$ \sf Kは導出可能性条件D2に対応．

$ \mathsf{4}は導出可能性条件D3に対応．

すなわち$ \sf K4でも良いように思える．ところが，現実には$ \sf Lが要請される．

なぜか？

Def.$ \sf K4のバリエーション

$ \sf K4\mathrm{lr}: $ \sf K4の推論規則にLöb推論規則を追加

$ \mathrm{lr}: $ \vdash_{\mathsf{K4}+\mathrm{lr}} \Box\varphi\to\varphiなら$ \vdash_{\mathsf{K4}+\mathrm{lr}} \varphi

Löbの定理$ T \vdash \mathrm{Pr}_T(\overline{\ulcorner \varphi \urcorner}) \to \varphi \implies T \vdash \varphi

$ \sf K4\mathrm{hr}: $ \sf K4の推論規則にHenkin推論規則を追加

$ \mathrm{hr}: $ \vdash_{\mathsf{K4}+\mathrm{hr}} \Box\varphi\leftrightarrow\varphiなら$ \vdash_{\mathsf{K4}+\mathrm{hr}} \varphi

Henkin文$ H（$ T \vdash H \leftrightarrow \mathrm{Pr}_T(\overline{\ulcorner H \urcorner})なる文$ H）がLöbの定理より$ T \vdash Hであることに対応．

$ \sf K4H: $ \sf K4の公理図式としてHenkin公理図式を追加

$ \sf H: $ \Box(\Box\Phi \leftrightarrow \Phi) \to \Box\Phi

Thm

$ \mathsf{GL} = \mathsf{K4}\mathrm{lr} = \mathsf{K4}\mathrm{hr} = \mathsf{K4H}

Obsv: 算術的解釈

そもそも$ \sf GLの命題記号と，形式的算術における命題とを結びつける写像が必要となる．その写像は変換と言われる．

ある変換$ fは，$ \sf GLの命題記号$ pを，形式的算術における文$ 1+1=2に変換する．

他方変換$ gは$ pを文$ \forall_x.\lbrack x = \overline{0} \to x + x = \overline{0}\rbrackに変換する

この$ f,gを$ \sf GLの論理式に拡張する．ただし，$ \Boxをどの理論$ Tの証明可能性として解釈するか？というところに依存するため，$ f_T,g_Tとして表される．

$ f_T(p) \equiv f(p)

$ f_T(\bot) \equiv 0=1すなわち，形式的算術における矛盾

$ f_T(\varphi \to \psi) \equiv f_T(\varphi) \to f_T(\psi)

$ f_T(\Box\varphi) \equiv \mathrm{Pr}_T(\overline{\ulcorner f_T(\varphi) \urcorner})