# Re: [isabelle] rigorous axiomatic geometry proof in Isabelle (Bill Richter)

• 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
• 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
>



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