証明可能性論理の不動点定理

References

G. Boolos; "The Logic of Provability" Chpt. 8

Def: Modalized / 箱入り

様相論理の論理式$ Aが命題変項$ pに対してModalized(箱入り)であるとは，$ Aの中の$ pが全て$ \Boxの中に入っている状況を指す．

example

$ \Box p \to \bot, \Box\lnot p, \Box\lnot\botは$ pに対してModalized．

$ \Box p \to pは$ pに対してModalizedではない．

Thm 1: 証明可能性論理の不動点定理 (1)

$ pに対してModalizedな論理式$ Aに対し，

次を満たして

$ \mathsf{GL} \vdash \Box(p \leftrightarrow A) \leftrightarrow \Box(p \leftrightarrow H)

かつ，現れる命題が$ \mathrm{Var}(H) \sube \mathrm{Var}(A) \setminus \{p\}で済むような

すなわち$ Aの$ p以外の命題変項だけで構成される

論理式$ Hが存在する．（$ Hを構成するアルゴリズムを構成することが出来る．）

Example 1

そのアルゴリズムによって構成すると以下となる．

$ A \equiv \Box p \implies H \equiv \top

対応: Henkin文

$ A \equiv \lnot\Box p \implies H \equiv \lnot\Box\bot

対応: Gödel文

$ A \equiv \Box\lnot p \implies H \equiv \Box\bot

対応: Jeroslow文

$ A \equiv \lnot \Box \lnot p \implies H \equiv \bot

対応: 否定Jeroslow文

$ A \equiv \Box p \to \Box\lnot p \implies H \equiv \Box\Box \bot \to \Box\bot

対応: 第2不完全性定理の対偶(?)

$ A \equiv \Box p \to q \implies H \equiv \Box q \to q

対応: Kreisel文

Example 2

任意の1階述語論理の文$ \sigmaとし，$ f(p) \mapsto \sigmaとする実現(証明可能性論理)$ fを取り，$ f_\mathsf{PA}に拡張する．

Thm1およびExample1より，

$ \mathsf{GL} \vdash \Box(p \leftrightarrow \lnot\Box p) \leftrightarrow \Box(p \leftrightarrow \lnot\Box\bot)

ここに$ f_\mathsf{PA}を適応することで，GLの健全性より

$ \mathsf{PA} \vdash \mathrm{Pr}_\mathsf{PA}(\ulcorner \sigma \leftrightarrow \lnot\mathrm{Pr}_\mathsf{PA}(\ulcorner \sigma \urcorner ) \urcorner) \leftrightarrow \mathrm{Pr}_\mathsf{PA}(\ulcorner \sigma \leftrightarrow \lnot\mathrm{Pr}_\mathsf{PA}(\ulcorner \bot \urcorner) \urcorner)が得られる．

$ \sf PAの健全性より，

$ \mathsf{PA} \vdash \sigma \leftrightarrow \lnot\mathrm{Pr}_\mathsf{PA}(\ulcorner \sigma \urcorner) \iff \mathsf{PA} \vdash \sigma \leftrightarrow \lnot\mathrm{Pr}_\mathsf{PA}(\ulcorner \bot \urcorner)

前半は$ \sf PAのGödel文の定義そのものである．

すなわちこれは全てのGödel文は自己の無矛盾性を表す文と同値を表している．

Example 3

Example 2と同じ様に各々のExample1を構成すると…

Henkin文$ \mathsf{PA} \vdash \sigma \leftrightarrow \mathrm{Pr}_\mathsf{PA}(\ulcorner \sigma \urcorner) \iff \mathsf{PA} \vdash \sigma \leftrightarrow \top

Jeroslow文$ \mathsf{PA} \vdash \sigma \leftrightarrow \mathrm{Pr}_\mathsf{PA}(\ulcorner \lnot\sigma \urcorner) \iff \mathsf{PA} \vdash \sigma \leftrightarrow \lnot\mathrm{Pr}_\mathsf{PA}(\ulcorner \top \urcorner)

否定Jeroslow文$ \mathsf{PA} \vdash \sigma \leftrightarrow \lnot \mathrm{Pr}_\mathsf{PA}(\ulcorner \lnot \sigma \urcorner) \iff \mathsf{PA} \vdash \sigma \leftrightarrow \bot

第2不完全性定理の対偶$ \mathsf{PA} \vdash \sigma \leftrightarrow (\mathrm{Pr}_\mathsf{PA}(\ulcorner \sigma \urcorner) \to \mathrm{Pr}_\mathsf{PA}(\ulcorner \lnot \sigma \urcorner)) \leftrightarrow \mathsf{PA} \vdash \sigma \leftrightarrow (\mathrm{Pr}_\mathsf{PA}(\ulcorner \mathrm{Pr}_\mathsf{PA}(\ulcorner \bot \urcorner) \urcorner) \to \mathrm{Pr}_\mathsf{PA}(\ulcorner \bot \urcorner))

Kreisel文

$ \mathsf{PA} \vdash \sigma \leftrightarrow (\mathrm{Pr}_\mathsf{PA}(\ulcorner \sigma \urcorner) \to \pi) \iff \mathsf{PA} \vdash \sigma \leftrightarrow (\mathrm{Pr}_\mathsf{PA}(\ulcorner \pi \urcorner) \to \pi)

ただし$ f(q) \mapsto \piとする

$ \pi \equiv \sigmaとすればLöbの定理に対応．

Def: Dot Modal

$ \boxdot A \equiv A \land \Box A

Thm 2: 証明可能性論理の不動点定理 (2)

$ pに対してModalizedな論理式$ Aに対し，

次を満たして

$ \mathsf{GL} \vdash \boxdot(p \leftrightarrow A) \leftrightarrow \boxdot(p \leftrightarrow H)

かつ，現れる命題が$ \mathrm{Var}(H) \sube \mathrm{Var}(A) \setminus \{p\}で済むような

すなわち$ Aの$ p以外の命題変項だけで構成される

論理式$ Hが存在する．（$ Hを構成するアルゴリズムを構成することが出来る．）