Is there a basic definition of higher order logic, as in HOL, Isabelle, etc.?

Question

I read "Concrete Semantics with Isabelle / HOL" and I am very intrigued by higher order logic. I know the usual first-order logic and some modal logic, but I have little if there was no previous impact of higher-order logic and its metatheory, so I would like to fill in the gap. I read that HOL is essentially a church theory of simple types, and Pure is an intuitionistic version of the former. The problem is the "core" word: how are the theories of Isabelle / HOL and Isabelle / Pure different, for example, Andrews' textbook ? Is there a textbook introduction to the higher order theory used in Isabelle / HOL and Isabelle / Pure, with some discussion of their metatheoretical properties?

Answer 1

Much can be said about HOL and its many variations and dialects. This is a recurring topic on the Isabelle mailing lists , and the other is HOL . For example, here is a relevant thread from January / February 2013 on isabelle-users: Where to find out about HOL vs FOL? with a few more links to relational literature.

There is also a bit about Isabelle / Pure logic (which is the minimum HOL) in the Isabelle / Isar Implementation manual , section 2 Primitive Logic .