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