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