# Re: [isabelle] rigorous axiomatic geometry proof in Isabelle

On 6/4/2012 9:59 PM, Bill Richter 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.
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.

`Define a system of logic as a language with rules of inference to
``interpret the language.
`

`Define a language as a set of symbols with a set of rules for combining
``the symbols.
`

`Additionally, there is the meta-language which is used to describe and
``define the object-language.
`

`Let the choices of the meta-language be Isabelle/FOL or Isabelle/HOL,
``and let the object-language be Tarski Geometry.
`
http://en.wikipedia.org/wiki/Tarski's_axioms

`The question becomes this: Can either of these be used as a
``meta-language to implement the object-language of Tarski Geometry?
`
To answer that question we can ask these questions:
1) Do these object-languages have the symbols we need for
Tarski Geometry, and let us combine them in the proper way
to create the language of Tarski Geometry.
2) Do these object-languages have rules of inference that allow
us to interpret the language correctly.

`Isabelle/HOL has the standard set of logical connectives and
``quantifiers, and it has natural deduction rules of inference. The syntax
``it forces on you appears to be compatible with Tarski Geometry. It looks
``like Isabelle/HOL can work as a meta-language to describe, define, and
``use Tarski Geometry.
`
But I drop back concerning FOL.

`Slawomir, you say that ZF is built on FOL. But the language of
``first-order logic is a family of languages. Zermelo-Frankael sets isn't
``built on a language of FOL, it is a first-order language, that is, a
``language of first-order logic. Conceptually, Isabelle/FOL + Isabelle/ZF
``is the first-order language of Zermelo-Frankael sets.
`
[pg.19, Language, Proof, and Logic, Barwise & Etchemendy]
...we talked about FOL as though it were a single language.
Actually, it is more like a family of languages, all having a
similar grammar and sharing certain important vocabulary items,
known as the connectives and quantifiers. Languages in this family
can differ, however, in the specific vocabulary used to form their
most basic sentences, the so-called atomic sentences.

`Please refer to Bilaniuk's free book "A Problem Course in Mathematical
``Logic", Def.5.1 Symbols pg.24, Def.5.2 Terms pg. 26, and Def.5.3
``Formulas pg.27, though a friendlier definition of the symbols would give
``us the full set of logical connectives and both the quantifiers.
`
http://euclid.trentu.ca/math/sb/pcml/pcml.html

`Every first-order language must meet the requirements of the logical
``symbols, which are Definition 5.1 items 1 to 5; it's the non-logical
``symbols that allow them to be unique, Definition 5.1 items 6 to 8.
`

`For the non-logical symbols, ZF has no constant or function symbols, and
``it has membership as the one predicate symbol.
`

`Now I switch to Tarski Geometry. I look at the wiki page, and it tells
``me that it can formulated as a first-order language with the predicates
``"betweenness" and "congruence".
`

`Okay, but to elaborate on question 2 above, can Isabelle/FOL provide the
``predicate "betweenness" to the first-order language of Tarski Geometry?
`

`I go out on a limb now, and I say that first-order languages can only be
``given predicates; that is, one language of FOL acting as a meta-language
``can't create new predicates when creating a new language of FOL.
`

`I could be wrong in my last paragraph. Regardless, if you're creating
``predicates for Tarski Geometry, where the logic you're using is
``Isabelle/FOL, aren't you really operating in the realm of "functional
``programming"/"Isabelle's meta-logic"/ML/HOL/etc..
`

`Regardless again, Isabelle/HOL appears to have the necessary ingredients
``to act as a meta-language for any FOL object-language. When different
``logics can be cleanly used as a meta-language to implement a particular
``object-language, can it not be a case of "six of one, or a half dozen of
``the other"?
`

`There is the issue of minimalism. But if you only had to import
``src/HOL/HOL.thy to implement Tarski Geometry, that would be pretty minimal.
`

`I stop here. These have been the comments of a novice speaking from the
``peanut gallery.
`
--GB

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