Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



On Mon, Jun 4, 2012 at 5:44 AM, Bill Richter
<richter at math.northwestern.edu>wrote:

> Thanks, Tjark and Konrad!  I'll read the HOL paper, which looks pretty
> old, and so is maybe something that everyone just assumes nowadays.  I
> don't know about those other first-order reasoning
> Automated_theorem_provers, or why folks don't use them.


Possible reasons include:

   1. FOL isn't expressive enough for their problems. It might technically
   be able to express something, but not nicely.
   2. The automated provers can't solve their problems, at least not
   without a lot of help, and that help is tedious to give.
   3. Some automated provers don't generate complete explicit proofs, and
   so have to be trusted; this is harder than trusting a simple proof checker.

That having been said, I'm under the impression that the world of automated
proving is always getting better. I don't know much about it because I
don't live day-to-day in that world.
Ideally, interactive provers should only benefit from progress in
automation, since automatic tools can be integrated into interactive proof
development environments.


>  My interest
> in proof assistants (HOL Light, Isabelle, Coq) is that Tom Hales is
> using them to formalize his Kepler conjecture proof.
>
>   it tends to puzzle mathematicians with an interest in foundations
>   who have been taught that everything rests on FOL and ZFC.
>
> Tjark, you understand my confusion!  Is something written about this?
> I do contend that it's true what mathematicians are taught, but it may
> not appear to be true at the technical level that proof assistants
> operate on.  That's of course fine, but I need to see the underlying
> FOL and ZFC, even if the proof assistants aren't coded that way.
>

It's not just a matter of how the proof assistant is coded. The underlying
logic of Isabelle/HOL is not FOL. (There is, of course, Isabelle/ZF, which
does use FOL and the ZF axioms.)
The piece of writing I think you might find enlightening is Andy Pitts's
document on the semantics of HOL.
It is the "Logic" manual available here
http://hol.sourceforge.net/documentation.html.
Note it is for the HOL4 system, not Isabelle/HOL, but since it's mainly
about the logic, HOL, itself, that those proof assistants basically share,
this shouldn't matter too much.
It gives a precise description of the syntax and semantics of HOL. The
semantics is given in terms of set-theoretic models, with which you're
probably more familiar.
I'll be happy to answer any questions about it. I was thinking of giving
you syntax and semantics of FOL and then of HOL so you could see them
compared, but that document is better presented than what I would have
written.
(By the way, FOL formulas can be embedded in HOL.)


>
> --
> Best,
> Bill
>
>




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