*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Thu, 31 May 2012 23:26:35 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1205312302520.27828@macbroy21.informatik.tu-muenchen.de> (message from Makarius on Thu, 31 May 2012 23:34:17 +0200 (CEST))*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAFP4q14YwNi6RksUOkGNGWYYzkNi3ca92FH4kYW19kJeOBcT2Q@mail.gmail.com> <alpine.LNX.2.00.1204301125350.6594@macbroy21.informatik.tu-muenchen.de> <201205020207.q4227VoC013147@poisson.math.northwestern.edu> <4FA0A63C.7030904@jaist.ac.jp> <201205020409.q42497Ou014411@poisson.math.northwestern.edu> <4FA0BBE7.4060302@jaist.ac.jp> <201205030338.q433ciL9026861@poisson.math.northwestern.edu> <201205250512.q4P5Cgns004328@poisson.math.northwestern.edu> <alpine.LNX.2.00.1205251146380.8953@macbroy22.informatik.tu-muenchen.de> <201205270818.q4R8IUWm022240@poisson.math.northwestern.edu> <alpine.LNX.2.00.1205292251410.19391@macbroy22.informatik.tu-muenchen.de> <201205310412.q4V4CCrj014777@poisson.math.northwestern.edu> <alpine.LNX.2.00.1205312302520.27828@macbroy21.informatik.tu-muenchen.de>

Thank you very much Makarius, for a long interesting lecture. I didn't know any of that stuff. This in particular: If you take HOL as a simplified version of set-theory with explicit syntactic types it is OK as a start. But I think we'd communicate a lot better if you understood math logic, from say Enderton's book Mathematical Logic. Until then you won't know why I'm floundering. I apologize if I misunderstand you. I can only guess what you mean by "strict axiomatic FOL proof". I mean what Enderton means (same for `models'), and I'd like you to know too. Look, you're really good at what you do, and you communicate really well, and you go to the trouble to speak intelligibly to newbies like me... but don't you want to know the proof of the Goedel incompleteness theorem? Anyway, eventually I'll take all of your suggestions. I'll go through the Isar manuals and learn Pure + Isar and see how close that is to Enderton's FOL. I want to learn! Isabelle is the only proof assistant with nice fonts and serious documentation. -- Best, Bill

- Next by Date: Re: [isabelle] Automation is awesome; one bibliography leads to another
- Next by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Cl-isabelle-users June 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