Re: [isabelle] rigorous axiomatic geometry proof in Isabelle

On Sun, 27 May 2012, Bill Richter wrote:

Thanks, Makarius, I'll run your code and study it.  Is this explained
somewhere in the Isabelle dox, or could you explain it better:

  We are doing precise single step reasoning here, which means all
  the slots for the rules need to be filled in the correct order.
  This is not Mizar or any of the Mizar modes for HOL, which are
  centered around classic predicate logic with some builtin proof
  automation to bridge larger gaps.

I would have said FOL instead of predicate logic, does that mean the
same?  I'm not an expert in FOL, but I think FOL proofs tend to be
very tedious, and the builtin Mizar proof automation turns these FOL
proofs into something that is a real pleasure to code up.  Is that
right?  And Isabelle (Isar?) is doing something different from that?

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.

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.

That is, I think of your locale as something close to FOL Tarski axiomatic geometry proofs. 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).


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