[FOM] About Paradox Theory

[Daniel Mehkeri]

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