選択公理と排中律

集合論シリーズ。いい加減一段落したいんですが...

選択公理と正則公理がうまく分離できなくて、ε-induction という正則公理の別表現が証明できてめでたしだったんですが...

　　なんと、直観主義論理上で集合論を構成すると選択公理から排中律が証明できる

え、え〜という感じなんですが、そもそも、

　　record OD {n : Level}　: Set (suc n) where
　　　field
　　　　def : (x : Ordinal {n} ) → Set n

という順序数定義可能集合で定義しているので、

　　ppp : { n : Level } → { p : Set (suc n) } { a : OD {suc n} } → record { def = λ x → p } ∋ a → p
　　ppp {n} {p} {a} d = d

という感じで要素があれば命題pが成立するODが作れる。というわけで、 p ∨ ( ¬ p )　がp空がでないなら選択公理から要素を取ってきて成立。

そんな感じで証明できました。ってことは、逆の

　　排中律を仮定すると選択公理が出る

ってのを思いつくわけですが。元々、ODの整列性は仮定している(ゲーデル数から出る)ので、整列定理から選択公理を証明すること自体は演習レベル。

なんだが、意外に難い。ε-induction の証明をなぞってとかやっていたんですが、

　　http://tinyurl.com/yy59al29

こんなページを発見。つらつら見てたら、

　　超限帰納法の定義が若干違う

てのを見つけました。いや、要らないとか言って少し条件緩めた記憶がある。osuc x が直後順序数で

　　TransFinite : { ψ : Ordinal → Set }
　　　→ ( ∀ (lx : Nat ) → ψ ordinal lx (Φ lx) )
　　　→ ( ∀ (x : Ordinal )　→ ψ x → ψ ( osuc x )
　　　→　∀ (x : Ordinal)　→ ψ x

だったんですが、Φつまり直前の順序数のない無限順序数が孤立していて変だとは思ってたんだよな。

　　TransFinite : { ψ : Ordinal → Set }
　　　→ ( ∀ (lx : Nat ) → ( (x : Ordinal ) → x o< ordinal lx (Φ lx)　→ ψ x ) → ψ ordinal lx (Φ lx) )
　　　→ ( ∀ (x : Ordinal )　→ ψ x → ψ ( osuc x )
　　　→　∀ (x : Ordinal)　→ ψ x

という感じで、無限順序数より小さい順序数ではψ xが成立ってのを仮定として使えるのが正しい。それがないと無理だとは思っていたんだ。

その治した奴をつかっていて、こんどは、

　　 (∀ x → (A x ∨ B)) →　(∀ x → A x) ∨ B

ってのが欲しくなった。Aが「xより小さいのにψ xは成立しない」で、Bが「見つかりました」なんだけど、量化記号を外に出せないと厳しい。

なんだけど、これって排中律で証明できる、そういえば、排中律を仮定して選択公理を出すのをやっているんだった。というのに気がついて証明できました。

つまり、ODの整列性を持つ直観主義論理上の集合論では、選択公理は排中律と同値というわけですね。

ここ数日、これが頭のたこになっていたので、片付いてうれしいです。