[FOM] Discussion between Thomas Forster & Bob Solovay

[Martin Davis]

Mea Culpa!

Bob Solovay had objected to Thomas Forster's indication that there was 
difficulty about the proof that the set of hereditarily finite sets is 
infinite by saying that the proof in ZFC is trivial.
Forster replied and I held up his posting for clarification. Meanwhile 
messages flew back and forth between the two. So I take it upon myself to 
reproduce their contents below:

On Sat, 7 Sep 2002, Thomas Forster wrote:

 > It does indeed have a trivial proof.  But - at least in the
 > proof system i have in mind, it's not normal.
 >

On the same date, Bob Solovay then asked

 >Can you explicate the word "normal"?

Thomas Forster replied

 >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.  Cantor's theorem for example.
 >But that proof involves ordered pairs and so has philosophically
 >irrelevant complications.  The theorem about hereditarily finite sets 
doesn't.


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