*To*: <alfio.martini at acm.org>, <gottfried.barrow at gmx.com>*Subject*: Re: [isabelle] Where to learn about HOL vs FOL?*From*: "Mark" <mark at proof-technologies.com>*Date*: Thu, 31 Jan 2013 23:16:07 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*Reply-to*: "Mark" <mark at proof-technologies.com>

You might find my glossary of HOL terminology useful. It includes various entries about mathematical logic. www.proof-technologies.com/misc/Glossary.txt Mark. on 31/1/13 3:52 PM, Alfio Martini <alfio.martini at acm.org> wrote: > 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-Theor > y/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-isabel > le-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-isabel > le-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/wi > ki/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 > > >

- Previous by Date: Re: [isabelle] Where to learn about HOL vs FOL?
- Previous by Thread: Re: [isabelle] Surprises with transfer method
- 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