*To*: Bill Richter <richter at math.northwestern.edu>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Jeremy Avigad <avigad at cmu.edu>*Date*: Thu, 03 May 2012 09:06:34 -0400*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <201205030311.q433BKCq026778@poisson.math.northwestern.edu>*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAPeE+xWo7_cfF6UE_P9OpD_Ot1iBQ-_OApymFyvXPF458Qw+fQ@mail.gmail.com> <201204292118.q3TLI5TK018411@poisson.math.northwestern.edu> <4F9F1B2B.1020209@gmail.com> <201205010456.q414uPRf032246@poisson.math.northwestern.edu> <4F9FE203.6050907@cmu.edu> <201205020156.q421uPti013054@poisson.math.northwestern.edu> <4FA176C5.40209@cmu.edu> <201205030311.q433BKCq026778@poisson.math.northwestern.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:11.0) Gecko/20120329 Thunderbird/11.0.1

Dear Bill,

Best wishes, Jeremy 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 Hilbert's), 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.

**References**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Tim (McKenzie) Makarios

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Jeremy Avigad

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

- Previous by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Date: Re: [isabelle] Using system jEdit with bundle
- Previous by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Cl-isabelle-users May 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