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

Le Mon, 04 Feb 2013 16:16:43 +0100, Makarius <makarius at> a écrit:

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. This is occasionally interesting to know, although just some tiny foundational bit. From Isabelle/Pure you move on to Isabelle/HOL,

But Isabelle/HOL is entirely derived from Isabelle/Pure, isn't 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.

People seems to care, only when they have to port some proof from one system to another. There seems to be multiple HOL4 to Isabelle papers on the web, and seems all are concerned with foundations.

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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