I'm looking for an introductory text or other materials on higher order logic, with a minimum of assumed background knowledge beyond first order logic.
$\begingroup$
$\endgroup$
12
-
$\begingroup$ It might help to say what you are interested in learning about HOL. There are purely mathematical texts which describe the logic and its type theoretic properties, like normalization. On the other hand, there are plenty of tutorials for the theorem provers, e.g. Isabelle/HOL, which use HOL as a logical base. Those focus more on the axioms of HOL and how to build mathematics in it practically using a computer. And finally there are papers connecting HOL to topos theory since a form of HOL is the internal language of a topos. $\endgroup$– Jason RuteCommented Aug 7, 2022 at 21:34
-
$\begingroup$ Also your background might help to. Do you come from more of a logic/math background (say having taken a logic course in logic in undergraduate), or a CS background (where you learned functional programming)? That might also impact what resources are best for you. $\endgroup$– Jason RuteCommented Aug 7, 2022 at 21:43
-
$\begingroup$ @JasonRute Thank you. My background is a mix of computer science and math. I have studied some first order logic, Haskell and Lean. I'm interested in the syntax and semantics and how it generalizes from first order logic. I would like to implement a simple proof checker for it in Haskell and prove some properties about it in Lean. $\endgroup$– user695931Commented Aug 8, 2022 at 1:25
-
$\begingroup$ I think then for the implementation side that you might be interested in HOL Light. HOL Light's implementation is really light weight and is only a few hundred lines of OCaml code. $\endgroup$– Jason RuteCommented Aug 8, 2022 at 2:54
-
1$\begingroup$ I don’t know the perfect resource but I learned about normalization of simple type theory (which is similar to the type theory used in say HOL Light, except the later adds polymorphism) through Jeremy Avigad’s logic course notes which are now the book Mathematical Logic and Computation. $\endgroup$– Jason RuteCommented Aug 12, 2022 at 21:16
|
Show 7 more comments
2 Answers
$\begingroup$
$\endgroup$
Since you are asking on the proof assistant stack exchange, possibly the best approach would be to read a tutorial for one of the proof assistants using HOL. Any good tutorial would describe the logic and how one can build mathematics in this logic.
I learned HOL via HOL-Light. The HOL-Light tutorial covers the logic, how to construct common mathematical objects like the natural numbers, and how to do proofs in HOL Light. Having said that, I don't know that I would really recommend HOL-Light, as it doesn't have a large base of users and it is not the most user-friendly system to work with (because you have to use an OCaml interpreter to interact with the theorem prover).
Possibly better would be to find a good tutorial for Isabelle/HOL. I think, but am not sure, that Proving and Programming is the recommended starting tutorial now.
answered Aug 7, 2022 at 22:05
$\begingroup$
$\endgroup$
1
I found it useful to also read books on higher-order logic, several I can recommend:
- Stewart Shapiro, Foundations without foundationalism (which argues second-order logic is adequate for doing ordinary mathematics, preferable to first-order logic, and examines higher-order logic)
- Peter B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof.
As preposterous as it sounds, I also found Johnstone's Sketches of an Elephant, vol. II, chapter D particularly good for discussions of categorical aspects of logic (specifically, the functorial behaviour of interpretations, and generalizing ideas to higher-order logic).
-
$\begingroup$ Book recommendations are more than welcome. Thank you. $\endgroup$ Commented Aug 21, 2022 at 20:33