日々の流転

λ. Agda による選択公理の証明

--#include "Hedberg/Logic/Set.alfa"
open LogicSet use Prop, Forall, Exist
 
AC (|A::Set) (|B::A->Set) (|C::(x::A)->(y::B x)->Prop)
   (z :: Forall A (\(x::A) -> Exist (\(y::B x) -> C x y)))
  :: Exist (\(f::(x::A)->B x) -> Forall A (\(x::A) -> C x (f x)))
  = struct
      fst = \(x::A) -> (z x).fst
      snd = \(x::A) -> (z x).snd

以前に「ITT₀では選択公理も証明できる」と書いたが、その証明と本質的に同じもの。

ところで、Forallは量化される型が明示的な引数なのに、Existは量化される型が暗黙の引数なのは何故?　とても気持ち悪い。

ところで、この形の選択公理は証明できるけど、ZF集合論での場合と違って、選択公理から排中律を証明することは出来ない。何故ならば外延性公理に相当するものが仮定されていないから。

λ. ジョンQ —最後の決断—

を視た。

λ. RHG読書会: 鈴木さんを囲む会

寝坊したので諦めた。しょぼーん（´・ω・｀）