[FOM] About Paradox Theory

[Daniel Mehkeri]

Harry Deutsch offers:

 > AyEzAx(F(xz) <--> x=y). Therefore,
 >
 > -EwAx(F(xw) <--> Au([F(xu) --> Ey(F(yu) & -Ez{F(zu) & F(zy)])]).

about which Vaughan Pratt asks:

 > Anyone care to comment on whether it's intuitionistically valid as it 
 > stands?  (I presume one can hedge by inserting a few "surely"'s,
 > formalized as not-not, to make it so, via Goedel's translation.)
 > Nik Weaver?

I don't think it is what you want anyway. The classical foundation axiom 
is not constructively valid. Yes it is true we can make it valid by 
contraposition: no inhabited set intersects all of its members. However 
(and this is the sort of thing Nik Weaver keeps reminding us about) this 
is weaker than set induction over all first-order formulas.

I'd say set induction is the intended meaning of well-foundedness. 
Thomas Forster seems to agree: "The only context in which this 
definition [well-foundedness] makes sense at all is [set] induction, and 
the only way to understand the definition or to reconstruct it is to 
remember that it is cooked up precisely to justify induction." (_Logic, 
Induction and Sets_)

CZF just postulates set induction as a schema. I don't know if there is 
a single first-order formula that is equivalent to it over some basic 
assumptions. I don't know how the "set of all well-founded sets" paradox 
would work.

Daniel Mehkeri