[FOM] Discussion between Thomas Forster & Bob Solovay

[Martin Davis]

Thomas Forster wrote

 >My understanding is that if you set up a weak set theory
 >which is nevertheless strong enough to prove that there are
 >infinitely many hereditarily finite sets as a natural deduction system, then
 >the obvious proof turns out to have a maximal formula.

 > My point is simply the general one that any proof in
 >a consistent set theory that involves sanitizing a paradox
 >is likely to be pathological.

Let HF be the set of hereditarily finite sets. Let V_n be defined as usual: 
V_0 = emptyset; V_{n+1}= Powerset[V_n]. Then HF is the union of the V_n and 
and |V_n|=2^n. Hence there is no natural number n such that |HF|=n.

Does this proof "involve sanitizing a paradox"

Alternative proof (using a different definition of infinite set): Choosing 
one of the obvious coding of hereditarily finite sets by natural numbers, 
we have a one-one correspondence between HF and N, and therefore (using the 
von Neumann coding of natural numbers by sets) with a proper subset of itself.

Same question. Really anything odd about the formalized version of these 
proofs in a natural deduction system (with appropriate set theortic axioms)?

Martin


                           Martin Davis
                    Visiting Scholar UC Berkeley
                      Professor Emeritus, NYU
                          martin at eipye.com
                          (Add 1 and get 0)
                        http://www.eipye.com