Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



On 04/06/12 19:37, Slawomir Kolodynski wrote:
> 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. 

Tarski's axiom of continuity comes in two versions: a first-order axiom
schema, or a single higher-order axiom.  If you use the higher-order
axiom, his axiom system is categorical.  So, yes, there is a good reason
for using HOL for Tarski's axioms.

Again, sorry for taking so long to make this point.

Tim
<><

Attachment: signature.asc
Description: OpenPGP digital signature



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