*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle (Bill Richter)*From*: "Luke Serafin" <lserafin at andrew.cmu.edu>*Date*: Thu, 14 Jun 2012 20:24:34 -0400*Importance*: Normal*In-reply-to*: <mailman.49963.1339656957.29855.cl-isabelle-users@lists.cam.ac.uk>*References*: <mailman.49963.1339656957.29855.cl-isabelle-users@lists.cam.ac.uk>*User-agent*: SquirrelMail/1.4.22

Mr. Richter, It might be helpful to look at a mathematical logic book which develops HOL rather than set theory as the foundation of mathematics, such as Peter Andrews' _An Introduction to Mathematical Logic and Type Theory: To Truth Trough Proof_ (let us abbreviate this TTTP; note that type theory is essentially another term for HOL). There we find (remark after the proof of theorem 5402) that the primitive version of HOL which the author calls Q0 is a conservative extension of FOL. The basic logic used in Isabelle and HOL Light is also a conservative extension of FOL (Coq uses constructive logic which is more restrictive than classical logic; I don't know whether its basic logic is a conservative extension of constructive predicate logic). Any stronger HOL system (e.g. Q0^\infty from the book mentioned above; this system is adequate for the formalization of a very significant portion of mathematics), can be viewed as this basic HOL together with a set of axiom schemata. Choose such a stronger HOL system, and denote its set of axioms by H. Then a sentence A is a theorem of this stronger system iff there exists a finite subset H0 of H such that H0 |- A (because proofs are finite, at least in this context). Note that the turnstile means provable from basic HOL, e.g. Q0. This is equivalent to |- B --> A, where B is the conjunction of all elements of H0. Hence any theorem of any (recursively axiomatized) version of HOL can be viewed as a theorem of a conservative extension of FOL. Furthermore, we could introduce type predicates and axioms about them into FOL and thereby fully import Q0 into FOL (this construction is elementary but tedious), which by the above argument means that we can effectively translate any HOL system into FOL. In this sense, you are right that HOL does not go beyond FOL. However, the notion of proof is completely different between FOL and HOL. In the second paragraph of the remark referred to above (TTTP p. 243), we find quoted a result of Statman that "the minimal length of a proof in first-order logic of a wff of first-order logic may be extraordinarily longer than the minimal length of a proof of the same (as in, translated canonically) wff in second-order logic." The paper referred to may be found here: <http://deepblue.lib.umich.edu/handle/2027.42/22467>, I have not studied it carefully but do know that the function from n to the maximal m such that m is a minimal-length FOL proof of a HOL wff which has a proof of length n asymptotically grows at least as fast as a hyper-exponential function. Thus, using HOL wffs and rules of inference is of great practical advantage when doing proofs with a computer. If we insist on everything being done in FOL, we could change our definition of proof to allow derived rules of inference to be used directly, and then derive translated versions of HOL rules of inference for some translation of HOL into FOL. However, it is practically much simpler to just think in terms of using HOL directly. Regarding set theory, ZF is strictly stronger than Q0^\infty, but its lack of intrinsic types makes proof searches in ZF much more difficult than those in Q0^\infty. Thus it is often advantageous to work with a typed HOL theory than directly with ZF. Isabelle allows the dynamic addition of new axioms, so if we ever need to go beyond Q0^\infty (say), we can just add whatever new facts we need as axioms, and perhaps prove the validity of these axioms in ZF if we believe that is necessary. Also, though ZF is normally considered to be based on FOL, there is no danger of introducing a contradiction if we conservatively extend its background logic, and so we can just as easily consider ZF in the context of HOL (e.g. Isabelle/ZF). This brings with it the possibility of gaining the advantages of types and HOL's much shorter proofs for ZF (e.g. we can define type-parameterized isomorphism predicates between types with associated operations and sets with associated operations, and use these to port theorems between HOL and ZF within this unified system). Hopefully this clarifies things somewhat, let me know if you have any questions about what is written above. Sincerely, Luke Serafin > Message: 4 > Date: Wed, 13 Jun 2012 23:40:15 -0500 > From: Bill Richter <richter at math.northwestern.edu> > Subject: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle > To: Ramana Kumar <rk436 at cam.ac.uk> > Cc: cl-isabelle-users at lists.cam.ac.uk > Message-ID: > <201206140440.q5E4eFgL018050 at poisson.math.northwestern.edu> > > 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 >

**Follow-Ups**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle (Bill Richter)***From:*Bill Richter

- Previous by Date: Re: [isabelle] Real reason for interaction
- Next by Date: Re: [isabelle] Looking for the GOOD way to use Isabelle and Latex together when writing a thesis
- Previous by Thread: Re: [isabelle] Real reason for interaction
- Next by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle (Bill Richter)
- 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