2
$\begingroup$

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.

$\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 Rute
    Aug 7 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 Rute
    Aug 7 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$
    – user695931
    Aug 8 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 Rute
    Aug 8 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 Rute
    Aug 12 at 21:16

2 Answers 2

4
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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

$\endgroup$
1
  • $\begingroup$ Book recommendations are more than welcome. Thank you. $\endgroup$
    – user695931
    Aug 21 at 20:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.