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
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.
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
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and