*To*: Gottfried Barrow <gottfried.barrow at gmx.com>*Subject*: Re: [isabelle] Where to learn about HOL vs FOL?*From*: Makarius <makarius at sketis.net>*Date*: Wed, 6 Feb 2013 16:10:33 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <51108E34.5080908@gmx.com>*References*: <1359754874943@names.co.uk> <510D7F55.5000902@gmx.com> <alpine.LNX.2.00.1302041610580.9980@macbroy21.informatik.tu-muenchen.de> <51108E34.5080908@gmx.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Mon, 4 Feb 2013, Gottfried Barrow wrote:

The augmented question at hand: what is a "more formal" definition of aIsabelle type, term, and formulae.We start at the very bottom of page 27 and the first three lines of page 28of 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.pdfOn page 28, there's reference [5] to Stefan and Tobias' "Proof terms forsimply typed higher order logic", published 2000, where on page 2 of that,there are semi-formal definitions of types, terms, and formulae, where two ofthose important meta-logic types show up again, universal quantification, andimplication.http://www4.in.tum.de/~berghofe/papers/TPHOLs2000.pdfThere are references [33,34] in isar-ref.pdf and [8,9] in "Proof terms" toLarry's papers, where the one common reference is most applicable, "Thefoundation of a generic theorem prover", published 1989.http://arxiv.org/ftp/cs/papers/9301/9301105.pdfPage 4 introduces types, terms, and formulae, along with three importantmeta-logic constants, and then on page 7, the three meta-logic constants areprinted on 3 lines to emphasize them.So, you look at the three different documents, read the three differentdescriptions, 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 onlyLarry lists meta-logic equality.

All of the above are important references about Isabelle/Pure.

But then things are more complex now, right? But another reference out ofthose 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.

Makarius

**References**:**Re: [isabelle] Where to learn about HOL vs FOL?***From:*"Mark"

**Re: [isabelle] Where to learn about HOL vs FOL?***From:*Gottfried Barrow

**Re: [isabelle] Where to learn about HOL vs FOL?***From:*Makarius

**Re: [isabelle] Where to learn about HOL vs FOL?***From:*Gottfried Barrow

- Previous by Date: Re: [isabelle] Where to learn about HOL vs FOL?
- Next by Date: Re: [isabelle] Where to learn about HOL vs FOL?
- Previous by Thread: Re: [isabelle] Where to learn about HOL vs FOL?
- Next by Thread: Re: [isabelle] Where to learn about HOL vs FOL?
- Cl-isabelle-users February 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list