Re: [isabelle] rigorous axiomatic geometry proof in Isabelle

   Is there a deep reason to code geometry axioms inside HOL? It seems
   to me it would be more natural to build Tarski geometry logic based
   on FOL, in the similar way like ZF logic is built on FOL.

That make sense, Slawomir, especially for Tarksi's axioms.  On hol
info John Harrison has been helping me to code up my Hilbert axiom
paper using set theory you can do in HOL Light.

Thanks, Ramana, for demonstrating that you understand math logic at
least as well as I do.  So I suppose we can assume that folks here in
general understand math logic.  I feel that you mainly answered my
question (about the mathematicians's belief of FOL/ZFC primacy) by
recommending Konrad's The HOL System LOGIC manual.

   Well, perhaps we can continue after you've read about the syntax and
   semantics of HOL and let's see if you have more specific questions then.

Yes, I'll book up and get back to you!  I need to learn HOL anyway,
and this manual seems like a good place to understand the foundations.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.