矛盾の証明 - Just $ A sandbox

矛盾を示すときに使える方法としては主に以下の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によって書き換えるだけで証明が済んでしまうことが多いので, 等しさが特別扱いやすいだけなのかもしれないけど.