*To*: Gottfried Barrow <gottfried.barrow at gmx.com>*Subject*: Re: [isabelle] Where to learn about HOL vs FOL?*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Thu, 31 Jan 2013 13:51:59 -0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <510A79F0.9050308@gmx.com>*References*: <op.wrrj47uzule2fv@cardamome> <510A79F0.9050308@gmx.com>*Sender*: alfio.martini at gmail.com

Hi Yannick, Adding to Gottfried´s selected readings, I strongly recommend the highly readable "The Seven Virtues of Simple Type Theory' by William Farmer (Journal of Applied Logic 6, 2008. Best! On Thu, Jan 31, 2013 at 12:04 PM, Gottfried Barrow <gottfried.barrow at gmx.com > wrote: > On 1/31/2013 12:54 AM, Yannick Duchêne (Hibou57) wrote: > >> Hi people, >> >> I hope my question won't look too much stupid to logics gurus. >> > > Yannick, > > I collect books written by the logic gurus, and occasionally read the > introductions, so I am qualified to provide links to books. > > The standard text that keeps getting mentioned by the logic gurus here is > Andrews' text, which starts with propositional logic and FOL, and then > covers type theory, where types would be the beginning of the foundation of > HOL in general: > > http://www.amazon.com/**Introduction-Mathematical-**Logic-Type-Theory/dp/* > *1402007639<http://www.amazon.com/Introduction-Mathematical-Logic-Type-Theory/dp/1402007639> > > FOL begins with the standard logic operators as its primitives, or a few > of them from which the others can be derived, as shown by Definitions 5.1, > 5.2, and 5.3 of Bilaniuk's book: > > http://euclid.trentu.ca/math/**sb/pcml/<http://euclid.trentu.ca/math/sb/pcml/> > > FOL is reasonably fixed in stone and standardized. > > HOL begins with variables, functions, and function application as > primitives, as shown by Paulson's "Foundations of Functional Programming" > Definition 1, page 2: > > http://www.cl.cam.ac.uk/~lp15/**papers/Notes/Founds-FP.pdf<http://www.cl.cam.ac.uk/~lp15/papers/Notes/Founds-FP.pdf> > > From there (or somewhere else) HOL diverges, where the two biggest camps > would be Coq's higher-order logic, and the HOL family, where HOL is not to > be confused with the general phrase "higher-order logic", and where John > Harrison gives a diagram showing the HOL family of products on page 9 of > "HOL Light Tutorial": > > http://www.cl.cam.ac.uk/~**jrh13/hol-light/tutorial_220.**pdf<http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf> > > Alfio recently pointed me to "Introduction to Type Theory" by Geuvers > which makes comparisons between type theory and set theory: > > http://www.cs.ru.nl/~herman/**PUBS/IntroTT-improved.pdf<http://www.cs.ru.nl/~herman/PUBS/IntroTT-improved.pdf> > > Because ZFC sets reigns as King and Queen in the world of mathematics, and > is a FOL language, then HOL vs. FOL is largely "types vs. ZFC sets", at > least for those who even know about the comparison, where education about > types is near non-existence in formal, mathematics education, even though > Church and Curry had their formal degrees in mathematics. > > To compare the two, the problem is understanding what HOL is, not what FOL > is, at least for me, since FOL is much simpler, even though HOL starts with > a simple set of primitives. > > I shared a list of the books I'd collected on trying to get up to speed > with Isabelle/HOL: > > http://lists.cam.ac.uk/**mailman/htdig/cl-isabelle-** > users/2012-June/msg00024.html<http://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-June/msg00024.html> > > http://lists.cam.ac.uk/**mailman/htdig/cl-isabelle-** > users/2012-June/msg00003.html<http://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-June/msg00003.html> > > Fortunately, I've decided I probably will be able to be live more > normally, which is to occasionally ponder questions about foundational > logic, but not have to completely understand it all to work at a higher > level. It's a very healthy place to be. > > Regards, > GB > > > > > >> Reading at Wikipedia's page about HOL, something tackled me a bit: >> >> http://en.wikipedia.org/wiki/**Higher-order_logic<http://en.wikipedia.org/wiki/Higher-order_logic> >> >> “HOL with standard semantics is more expressive than first-order logic. >> For example, HOL admits categorical axiomatizations of the natural >> numbers, and of the real numbers, which are impossible with >> first-order >> logic. However, by a result of Gödel, HOL with standard semantics does >> not admit an effective, sound and complete proof calculus.” >> >> There's also a criticism section on the same page. >> >> Well, I'm not sure to understand what it really means and would like to >> know if there are good pointers to understand how and when difference >> between HOL and FOL matters, and when and how Isabelle has to do with it. >> The quote from Wikipedia looks weird to me, as it seems to say they may be >> soundness issue with HOL? Is that really it? I've never heard about any >> such assertion before… >> > > > -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) Coordenador do Curso de Ciência da Computação Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática 90619-900 -Porto Alegre - RS - Brasil

**Follow-Ups**:**Re: [isabelle] Where to learn about HOL vs FOL?***From:*Yannick Duchêne (Hibou57)

**References**:**[isabelle] Where to learn about HOL vs FOL?***From:*Yannick Duchêne (Hibou57)

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

- Previous by Date: Re: [isabelle] Surprises with transfer method
- 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 January 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