Re: [isabelle] Where to learn about HOL vs FOL?
On 2/4/2013 9:16 AM, Makarius wrote:
On Sat, 2 Feb 2013, Gottfried Barrow wrote:
I now ask, "Where is the semi-formal definition of a Isabelle type
See the Isabelle/Isar implementation manual chapter 2, about
Isabelle/Pure as reduced version of Higher-Order Logic to provide the
If you said, "If you understand the HOL4 definitions of a type and
term, then you basically understand Isabelle's".
Thanks for the reference. A little guidance can go a long way. But, it
still gets unwieldy, so I quote from a cycling blog article,
In truth the greatest challenge is from having to deal with
performances unfolding in front of you that are just so astounding
and abnormal that you know precisely what's happening but you just
can't say it straight out. The list is endless; Rasmussen, Armstrong
and the Postals, Sella, Ricco, Mazzoleni... and on. I now confine
myself to saying "that was an unbelievable performance"...
What I know precisely is that the answer is spread out over multiple
documents, which was actually easy to know, just not easy to sort out.
I'm already past my word limit, so I try to implement a form of the
method from the quote.
The augmented question at hand: what is a "more formal" definition of a
Isabelle type, term, and formulae.
We start at the very bottom of page 27 and the first three lines of page
28 of isar-ref.pdf to give us a conceptual view of 3 important
meta-logic types: functions, universal quantification, and implication:
On page 28, there's reference  to Stefan and Tobias' "Proof terms for
simply typed higher order logic", published 2000, where on page 2 of
that, there are semi-formal definitions of types, terms, and formulae,
where two of those important meta-logic types show up again, universal
quantification, and implication.
There are references [33,34] in isar-ref.pdf and [8,9] in "Proof terms"
to Larry's papers, where the one common reference is most applicable,
"The foundation of a generic theorem prover", published 1989.
Page 4 introduces types, terms, and formulae, along with three important
meta-logic constants, and then on page 7, the three meta-logic constants
are printed on 3 lines to emphasize them.
So, you look at the three different documents, read the three different
descriptions, look at the types of the meta-logic constants, read about
"prop" and "trueprop", and it might make more sense.
Interesting is that they all list implication and quantification, but
only Larry lists meta-logic equality.
But then things are more complex now, right? But another reference out
of those listed above is "Isabelle, a Generic Theorem Prover", published
And on page 5 they're already talking about type classes.
This is occasionally interesting to know, although just some tiny
foundational bit. From Isabelle/Pure you move on to Isabelle/HOL,
then you add many add-on tools for 'inductive', 'datatype' etc. and
lots of proof tools like Sledgehammer. Then you are quite high above
the logical foundations and don't care much about them.
In another email, you made the analogy to being a Linux user. I think
the better analogy would be where 90% of the code is in C, but then
there's that occasional call into assembly language. If assembly
language is not a total mystery to you, you make tweak here or there.
Or maybe it's the VHDL analogy. You can read schematics, but that VHDL
that the PGA is programmed in, that really stumps you, and you come to a
grinding halt because that's not something you easily learn, and a lack
of understanding really limits your ability to understand the circuit.
Until the book "The Isabelle/Pure and Isabelle/HOL Logic, From Top to
Bottom, as Implemented in ML and Isar" comes out, every 4-6 months
someone will be asking, "Hey, what's Isabelle/Pure all about?"
But there's quite a bit of documentation to all this, or I wouldn't be
messing around with it.
What is also interesting that the final end-user view tends to
converge to what totally different systems offer here, e.g. Coq with
its quite different foundations, if you take inductive definitions or
recursive functions, for example.
This archive was generated by a fusion of
Pipermail (Mailman edition) and