[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