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

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.


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