[FOM] About Paradox Theory
Daniel Mehkeri
dmehkeri at gmail.com
Mon Sep 19 02:41:05 EDT 2011
Andrej Bauer writes:
> -----Coq 8.3------
> Parameter A : Set.
> Parameter F : A -> A -> Prop.
> Lemma pratt: ~ exists y, forall x, F x y <-> ~ F x x.
Except I thought he was asking about the paradox of grounded classes.
Formally, I do believe
[ AyEzAx(F(xz) <--> x=y) ] -->
[ -EwAx(F(xw) <--> -Eu([F(xu) & Ay(F(yu) --> Ez{F(zu) & F(zy)})]) ]
will be intuitionistically provable. ("There is no set of all the sets
that do not belong to any set which intersects all of its members,
assuming singletons exist.")
Informally, however, this constructive paradox of grounded classes is
not Mirimanoff's, since this doesn't capture well-foundation, as I said.
Daniel Mehkeri
More information about the FOM
mailing list