トップ «前の日記(2005-05-13) 最新 次の日記(2005-05-16)» 月表示 編集

日々の流転


2005-05-14 [長年日記]

λ. 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

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

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

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

Tags: agda

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

ジョンQ-最後の決断- [DVD](ジェームズ・キアーンズ) を視た。

Tags: 映画

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

寝坊したので諦めた。しょぼーん(´・ω・`)

Tags: ruby