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

```Thanks, Makarius, and I really like your posts on hol info.  I'd be
happy for you to post there about miz3 ocaml dirty code cache issues.

The Isabelle/Pure framework is centered around higher-order natural
deduction, and Isabelle/Isar as a proof language continues these
ideas. To understand these things properly, you should first blot
out "FOL", then get used to Pure + Isar, then add HOL as
object-logic, and then rediscover what predicate logic (including
FOL) will do for you here via some add-on tools.

I'm not opposed to learning Pure + Isar, but it would be a whole lot
easier for me to learn if I knew in advance how it related to FOL,
which as a mathematician I have a rudimentary (but not practical)
understanding of.  Let me make a rudimentary FOL point:

I think writing down strict axiomatic FOL proofs would really be
tedious because e.g. you have manually substitute variables every time
you want to use an axiom.  I don't have a full list of the tedium
strict FOL can cause.  But I'm only willing to write up FOL-type
proofs if the proof assistant will automate that tedium.  Do similar
issues arise with Pure + Isar?

Also, as you may have observed on hol info, I know next to nothing
about HOL.  Basically I understand the 20 pages of set theory John
explains in his reference manual.  Isn't Isabelle HOL much the same as
HOL as in HOL Light HOL?  Where is a good place to learn about HOL?

> Yes, and thus locales are definitely a real advantage of Isabelle
> over HOL Light right now.  Still, I wonder why one can't just
> define all the sets you'd want in HOL Light (only very lightly
> typed) to get something like a locale.

In principle any of the HOL systems could provide their own locale
mechanism, or something similar.  It is not possible to "just" do
it, though.  Isabelle has required 10+ years to get this all done
right. It is also a matter of culture.  John Harrison would
certainly not add such complexity to his system.  You have to use
Isabelle or Coq for such sophisticated module concepts, or maybe
Mizar.

Sure, but I really dislike the Mizar type system, and I want to
lightly typed sets to avoid any hard typing.  More below:

> But instead we could look at all models of Tarski's axioms, a
> model being some sets and functions with some properties.  Can
> you do this in Isabelle too?

If this means you want to study the meta-theory of Tarski axioms,
then any of the HOL systems -- Isabelle/HOL included -- can do this
for you, if you define the syntax and inference system more
concretely (via datatypes and inductive relations).

Great, but I don't know what meta-theory means.  A model of Tarski's
geometry axioms is be a set S (of points), a 3-ary relation Between on
S and a 4-ary relation Equiv on S satisfying Tarski's axioms (so far I
only use his first 7 axioms, and you coded them up in Isabelle).  So
there might be a predicate TarskiModel(S, Between, Equiv), and
theorems in a Tarski model would begin

assume TarskiModel(S, Between, Equiv)...

I don't understand HOL well enough to actually pull this off, but John
explained how to get started.  My point is that I don't think any
typing is involved here, beyond maybe something rudimentary like

new_type("point",0);;
new_type_abbrev("TarskiPlane",`:point->bool`);;

--
Best,
Bill

```

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