*To*: Ramana Kumar <rk436 at cam.ac.uk>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Wed, 13 Jun 2012 23:40:15 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAMej=266eUx0Z_Y_88UOf2PA63pfMgEufBSRZCLykHnSU3ep3Q@mail.gmail.com> (message from Ramana Kumar on Mon, 4 Jun 2012 09:46:37 +0100)*References*: <alpine.LNX.2.00.1205312302520.27828@macbroy21.informatik.tu-muenchen.de> <201206022353.q52Nredm012382@poisson.math.northwestern.edu> <CAMej=266eUx0Z_Y_88UOf2PA63pfMgEufBSRZCLykHnSU3ep3Q@mail.gmail.com>

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

**References**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Ramana Kumar

- Previous by Date: Re: [isabelle] Formalisations of infinite streams
- Next by Date: [isabelle] 3 new AFP entries available
- Previous by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Cl-isabelle-users June 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list