矛盾の証明
矛盾を示すときに使える方法としては主に以下の2つだと思う
- 命題
¬P
にP
をぶつける - 矛盾
⊥
の特徴付けを使う
矛盾の特徴付けというのは, 例えばAgdaだと⊥は空集合の公理を満たすことが示せるから,
空集合の公理がそのまま矛盾の特徴付けになる.
∃ \(A : Set) → (∀ x → ¬ (x ∈ A))
否定命題にPをぶつけるというのは口で言うほど簡単ではなくて, まずどの否定命題を選んでくるかからよく考えないといけない.
一体何の話かというと, Agdaで「ZFC ⇒ 排中律 (P ∨ (¬ P))」を示すときに,
https://myuon.github.io/agda-cate/Sets.Sets.NonDatur.html#660
A = ⟦ x ∈ [0,1] ∣ x ≡ 0 ∨ P ⟧ -- A := {x ∈ {0,1} ∣ x = 0 ∨ P} B = ⟦ x ∈ [0,1] ∣ x ≡ 1 ∨ P ⟧ -- B := {x ∈ {0,1} ∣ x = 1 ∨ P} X = [ A , B ] -- X := {A,B}
みたいにするんだけど, 以下の議論では, ここにさらっとでてくる自然数0と1が異なることが仮定されている.
0と1は上のように非順序対を作って使うので適当なsetでないといけないんだけど, 当然AgdaのData.Natで定義されているNatの元は(inductive data typesで定義されているから)setではない.
そこで 0 = ∅
, 1 = ∅ ∪ {∅}
に戻って0と1が異なることを示さないといけなかったけれど, これには空集合の公理や対の公理や和集合の公理が必要で, しかもそんなに明らかなことでもない.
https://myuon.github.io/agda-cate/Sets.Sets.Natural.html#793
Natの世界でもSetの世界でも0と1が異なることを示すには, 0=1を仮定して矛盾を導かなければいけないので, それがいつも自明なことではないなと実感した.
というかむしろ, Agdaの場合は同値なものがrewriteによって書き換えるだけで証明が済んでしまうことが多いので, 等しさが特別扱いやすいだけなのかもしれないけど.