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



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





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