I am reading "Concrete semantics with Isabelle/HOL" and I am getting very intrigued by higher-order logic. I know ordinary first-order logic and some modal logic but I have little if none previous exposure to higher-order logic and its metatheory, so I would like to fill the gap. I read that HOL is essentially Church's Theory of simple types and Pure is an intuitionistic variant of the former. The problem is the "essentially" word: How do the Isabelle/HOL and Isabelle/Pure theories differ from, e.g., Andrews' textbook? Is there a textbook introduction to the kind of higher-order logic used in Isabelle/HOL and Isabelle/Pure, with some discussion of their metatheoretical properties?
1 Answers
1
votes
A lot can be said about HOL and its many variants and dialects. It is a recurrent topic on the mailing lists of Isabelle and the other HOL systems. For example, here is a relevent thread from Jan/Feb 2013 on isabelle-users: Where to learn about HOL vs FOL? with a few more references to relavant literature.
There is also a little bit about the logic of Isabelle/Pure (which is minimal HOL) in the Isabelle/Isar Implementation manual, section 2 Primitive logic.
