Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
I agree that it would be nice to see Elements-style proofs verified in
Isabelle. I have talked about E with friends in the Isabelle community,
so they know about the work.
I'll respond to the rest of the message off-list, though, since the
details are not related to Isabelle.
On 05/02/2012 11:11 PM, Bill Richter wrote:
Our paper aims to provide a formal system, E, that mirrors the
structure of Euclid's proof. We show how such a system can be
interpreted in terms of more conventional proof systems (like
Jeremy, this is very interesting, and explained on p 69 of your paper:
ADM> Below, however, we will show that with a modicum of tinkering,
ADM> Tarski’s axioms can be expressed in a restricted form, namely, as
ADM> a system of geometric rules. We will then invoke a cut
ADM> elimination theorem, due to Sara Negri, that shows that if a
ADM> sequent of suitably restricted complexity is provable in the
ADM> system, there is a proof in which every intermediate sequent is
ADM> also of restricted complexity. This will allow us to translate
ADM> proofs in Tarski’s system to proofs in E.
I don't see where you went the other way, translating your proofs into
Tarski axiomatic proofs. You are saying that rigorous Hilbert/Tarski
axiomatic proofs are simpler than proofs in your framework, right?
Probably you understand the advantage of Tarski's axioms over
Hilbert's, but I'll say it anyway: Mostly the advantage is that Tarski
in a first order axiom basically said that every line is the real
line, so that the model is R x R. Hilbert got that earlier with a
second order logic axiom, a Dedekind cuts axiom. Tarski actually only
got F x F, for a real closed field F, but that's good enough, as he
showed that the theory of real closed fields is decidable. But do you
need decidability? I see you mention it often. Ziegler's result that
you cite is used by Greenberg (Amer. Math. Monthly 2010) to show that
Hilbert's first order geometry is undecidable.
but getting Isabelle to verify proofs in E as such would require
extending Isabelle with some automation to bridge the gap.
But the Isabelle folks are looking for that kinda work (so I copied
the list)! I think that's why Scott, Fleuriot& Meikle are coding up
Hilbert's book FoG, to give HOL Light and Isabelle a workout.
This archive was generated by a fusion of
Pipermail (Mailman edition) and