Re: [isabelle] Where to learn about HOL vs FOL?
On Mon, 4 Feb 2013, Gottfried Barrow wrote:
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
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.
All of the above are important references about Isabelle/Pure.
Generally, you always need to put things into the context of *who* is
writing *when* -- there different ways to explain things, which also tend
to change over time. For example, I always follow the advice by Stefan
Berghofer from 2000 to say "logical framework" and not "meta-logic": Pure
gives you so little to speak about other logics, e.g. no induction on the
The == connective of Pure is hardly relevant for users now, it serves
mainly foundational purposes, so it appears later in my exposition in the
"implementation" manual. And there are more important add-on constants in
Isabelle/Pure, like conjunction or funny prop markers.
For users mainly => !! ==> are relevant, to express the structure of your
abstract syntax and rule statements.
But then things are more complex now, right? But another reference out of
those listed above is "Isabelle, a Generic Theorem Prover", published 1994.
And on page 5 they're already talking about type classes.
That is now really really old. I feel nostalgic about the "3 standard
Isabelle manuals" that were pasted together for the 1994 LNCS volume.
Things have changed a lot since then, both the system and the way it is
explained. Type classes are not as trivial as they were looking in 1992,
so you can't just introduce them in passing right at the start of an
arbitrary Isabelle manual.
What I sometimes do is to show a canonical application of type classes to
This looks simple and obvious, and people learn something they can re-use
later. It is very far removed from the actual logical foundation of type
classes, though. Lots of "layers" around the raw logic at the bottom.
This archive was generated by a fusion of
Pipermail (Mailman edition) and