Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



Dear Bill,

On Sat, 2012-06-02 at 18:53 -0500, Bill Richter wrote:
> 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!
> 
> But I'm puzzled because almost nobody talks this way in the proof
> assistant world. [...]

I haven't been following this thread in detail, so I am not sure what
you've been told already. Surely you realize that FOL is just one logic
(albeit an important one). There are many other logics, and interactive
proof assistants are usually *not* built on FOL.

There are very good reasons for this design choice, but it also has its
drawbacks. For instance, it tends to puzzle mathematicians with an
interest in foundations who have been taught that everything rests on
FOL and ZFC.

If you are specifically looking for systems that perform (automated)
first-order reasoning, take a look at
http://en.wikipedia.org/wiki/Automated_theorem_proving

Best regards,
Tjark







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