Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- 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.firstname.lastname@example.org> (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.email@example.com> <201205020207.q4227VoC013147@poisson.math.northwestern.edu> <4FA0A63C.firstname.lastname@example.org> <201205020409.q42497Ou014411@poisson.math.northwestern.edu> <4FA0BBE7.email@example.com> <201205030338.q433ciL9026861@poisson.math.northwestern.edu> <201205250512.q4P5Cgns004328@poisson.math.northwestern.edu> <alpine.LNX.firstname.lastname@example.org> <201205270818.q4R8IUWm022240@poisson.math.northwestern.edu> <alpine.LNX.email@example.com> <201205310412.q4V4CCrj014777@poisson.math.northwestern.edu> <alpine.LNX.firstname.lastname@example.org>
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and