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 and term?"

If you said, "If you understand the HOL4 definitions of a type and term, then you basically understand Isabelle's".
See the Isabelle/Isar implementation manual chapter 2, about Isabelle/Pure as reduced version of Higher-Order Logic to provide the logical framework.


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

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

And on page 5 they're already talking about type classes.

(Makarius writes)

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