Re: [isabelle] rigorous axiomatic geometry proof in Isabelle

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 MHonArc.