日々の流転

λ. ロッサーの不完全性定理

かがみさんの「ロッサーの不完全性定理」と通りすがりさんのコメントで情報としては十分過ぎるけど、ちょっと考えたこともあるので一応メモ。

ロッサー文

prove´(x,[A]) := prove(x,[A]) ∧ (∀y≦x. ¬prove(y,[¬A])) として、 T ⊢ R≡¬∃x. prove´(x,[R]) を満たす論理式Rをロッサー文という。 T ⊢ R≡(∀x. prove(x,[R]) → ∃y≦x. prove(y,[¬R])) なので、通りすがりさんが書いているように、Rの直観的な意味は「この命題の証明が存在すれば、この命題の否定のより簡単な証明が存在する」となる。

補題1: T ⊢ A ならば ∃x. prove´(x,[A])

T ⊢ A と仮定する。

1. その証明図πが存在し T ⊢ prove([π],[A])。
2. Tの無矛盾性より T ⊬ ¬A であり、任意の x≦[π] について T ⊢ ¬prove(x,[¬A]) 。したがって、 T ⊢ ¬prove(0,[¬A])∧¬prove(1,[¬A])∧…∧¬prove([π],[¬A]) であり T ⊢ ∀x≦[π]. ¬prove(x,[¬A]) 。

したがって、T ⊢ ∃x. prove´(x, [A])

T ⊬ R

T ⊢ R と仮定する。

1. 補題1より T ⊢ ∃x. prove´(x, [R])
2. 一方、T ⊢ R≡¬∃x. prove´(x,[R]) より T ⊢ ¬∃x. prove´(x,[R]) 。

これは矛盾なので、背理法より T ⊬ R 。

補題2: ある定数nについて T ⊢ ∃x≦n. prove(x, [A]) ならば T ⊢ A

T ⊬ A と仮定し、nを任意の定数とする。 任意のx≦nについて T ⊢ ¬prove(x,[A]) であるので T ⊢ ¬prove(0,[A])∧¬prove(1,[A])∧…∧¬prove(n,[A]) で T ⊢ ∀x≦n. ¬prove(x,[A]) 。 すなわち T ⊢ ¬∃x≦n. prove(x,[A]) で、Tの無矛盾性より T ⊬ ∃x≦n. prove(x,[A]) 。

T ⊬ ¬R

T ⊢ ¬R だと仮定する。

1. その証明図πが存在して T ⊢ prove([π], [¬R])
2. 一方、T ⊢ R≡¬∃y. prove´(y,[R]) より T ⊢ ∃y. prove(y,[R]) ∧ ∀z≦y. ¬prove(z,[¬R])

ここから T ⊢ ∃y. prove(y,[R]) ∧ ¬([π]≦y) で、簡単な定理を適用すると T ⊢ ∃y<[π]. prove(y,[R]) が得られ、補題2より T ⊢ R 。 これはTの無矛盾性に矛盾するので、背理法より T ⊬ R 。

考察

巧妙なのは、「T ⊢ ∃x. prove(x,[A]) ならば T ⊢ A」にはω無矛盾性が必要なのに対して、補題2の「ある n について T ⊢ ∃x≦n. prove(x,[A]) ならば T ⊢ A」には無矛盾性で十分なこと。そして、それが利用できるように論理式Rを構成した点か。ゲーデルのアイディアに比較すれば技術的な微調整に過ぎないかもしれないけど、こういうのも好きだし感心。

算術的階層との関連で考えると、 ∃x. prove(x,y) は Σ₁ であって Δ₁ ではないのに対して、 ∃x≦n. prove(x,y) は Δ₁ というのが効いているのだろうと思う。

次は「クライゼルの注意」について考えるか。

λ. 堀江被告に実刑2年6月「一般投資家欺いた」

有罪自体はそこまで意外ではないけど、実刑になったのは意外。 証取法で実刑なんて結構珍しいのでは。

それと、「堀江被告、即金2億円で再保釈　保証金は5億円」を見て思ったのだが、保釈金って法定利息が付いたりするのだろうか?　……どうやら付かないらしい。供託金には利息がつく*1のに保釈金には付かないというのは少し気持ち悪い気がする。