Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



Ramana, I've been discussing the issue with Freek, who I'm very
impressed with, as miz3 is holding up very well under the torture
testing my 1300 lines of Hilbert axiomatic geometry code
http://www.math.northwestern.edu/~richter/OpenIntervalHilbertAxiom.ml.
The issue is almost entirely a matter of terminology.  I say that the
proof assistant (PA) world ought to explain how to translate the
language of mathematical logic books (e.g. Enderton's) into PA
terminology.  In particular there's the vexing issue of the term FOL.

I'm really happy with your understanding of Goedel Incompleteness:

   The First Incompleteness Theorem says that if we fix a theory whose
   axioms can be generated by a computer,[...] 

Yes!  And in math logic books, this is called FOL, and the infinite
set of axioms in ZFC fit into what they call axiom schemes.  You
understand the infinite axiom biz quite well, as we see again here:

   If the set of axioms can be generated by a computer, then all (and
   only) the provable statements of a theory can also be generated by
   a computer.  This is why first-order logic [FOL] is "semidecidable".

Great!  That's my meaning of FOL, which you used again here:

   Right. I'm not sure this result has any particular name. The "nice set" of
   FOL axioms means a "recursively enumerable set".

But now you mystify me by disagreeing with me at the end:

   > So what do proof assistants (Coq, Isabelle, HOL Light) do?  I
   > would assume they all start with some FOL axioms and then deduce
   > axiomatic FOL proofs as one discusses in math logic.  I contend
   > that the proof assistants must do that, because (by math logic)
   > they can't do anything else!  And the mathematicians can't do
   > anything else either!

   No it's not true, because neither proof assistants nor
   mathematicians are restricted to FOL.

Now I think you switched over to to the (apparently more restrictive)
PA meaning of FOL.  I contend that what I said is true, in the
following sense explained commonly in set theory books: Every theorem
proved today by mainstream mathematicians (let's forget large cardinal
axioms) has an FOL proof in ZFC.  Of course it would be extremely
inconvenient for mathematicians to write up FOL ZFC proofs!  Are we
arguing about what's convenient?  I just want to see the big picture
right now, how PAs relate to the FOL math logic which I only
understand at a big picture level anyway.

-- 
Best,
Bill 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.