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:

http://isabelle.in.tum.de/website-Isabelle2012/dist/Isabelle2012/doc/isar-ref.pdf

On page 28, there's reference [5] 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.

http://www4.in.tum.de/~berghofe/papers/TPHOLs2000.pdf

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.

http://arxiv.org/ftp/cs/papers/9301/9301105.pdf

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 object-logic formulation.

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.

http://www.amazon.com/Isabelle-Generic-Theorem-Lecture-Computer/dp/3540582444

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 beginners, e.g. http://isabelle.in.tum.de/dist/library/HOL/Isar_Examples/Group.html

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.


	Makarius






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