8
$\begingroup$

Short version: What is a good shortish introduction to intuitionistic logic, accessible to a relative beginner in logic?

Long version: I'm revising the frequently used Teach Yourself Logic Study Guide which aims to give recommendations for good books and other resources for self-study on different areas of logic. (This, by the way, is aimed at readers with a background in philosophy or maths, not at e.g. computer scientists.)

The Guide needs a better introductory section on intuitionistic logic (aimed at someone who has e.g. done a standard course on classical first order logic, but doesn't yet know much logic). Ideal reading would have something about motivation, the BHK interpretation, leading to Kripke semantics, and something about a proof system (e.g. natural deduction), and some light metatheory. So we are talking about a first pass at the area, not a full book's worth! -- e.g. something along the lines of what van Dalen attempts in Ch. 5 of his Logic and Structure (but perhaps better!). If you are a student, what has worked well for you as a first intro to intuitionistic logic? If you are a logic instructor, what do you recommend to your students?

$\endgroup$
5
  • $\begingroup$ I got into intuitionistic logic (and constructive mathematics as a whole) through automated and interactive theorem proving. Working with a type system like the calculus of inductive constructions in a language like Lean (leanprover.github.io/tutorial) or Coq really makes intuitionism look particularly natural, and is a good way to very quickly get the intuitions (mind the pun) behind how intuitionistic proofs work and feel to write. I learned about the Kripke semantics and other things later. The motivations behind intuitionism are basically the same as constructivism more broadly. $\endgroup$ Dec 8 '19 at 21:43
  • $\begingroup$ Yes, thanks! -- although I don't know it well, I know about the route in via type systems. But (as I've now made a bit clearer) I'm really interested here in something likely to be accessible to those coming from a more conventional logic background. $\endgroup$ Dec 8 '19 at 21:52
  • $\begingroup$ Maybe useful Ch.8 of Harrie de Swart, Philosophical and Mathematical Logic (Springer, 2018). $\endgroup$ Dec 9 '19 at 9:26
  • $\begingroup$ Thanks for the reference, Mauro! I hadn't come across the book before, so I'll take a look. $\endgroup$ Dec 9 '19 at 10:21
  • $\begingroup$ From my point of view, where I got into the subject was through a background of algebraic geometry, leading to sheaves, Grothendieck sites, topos theory and then to the logical interpretations of topos theory. And still, most of my thinking in terms of coming up with counterexamples goes naturally to the point of "well, is it true in the topos $\mathbb{R}$? Is it true over a general topological space? Is it true over general Grothendieck sites? etc." $\endgroup$ Feb 6 '20 at 22:14
2
$\begingroup$

It might be a little late, but perhaps it could help for someone else watching this question. I'm currently studying Intuitionistic Logic from the second chapter in the the book "Lectures on the Curry-Howard Isomorphism" (1998 version): https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf It seems like it fits your description.

$\endgroup$
2
  • $\begingroup$ On a tangent related to C-H: I've thought of writing an introduction for mathematicians (rather than for CS as most of the introductions I've seen do it) which starts out: for each proposition $P$, there exists a set $S_P$ such that $P$ is equivalent to $S_P \ne \emptyset$. The first proof is just either $P$ is true and $S_P = \{ 0 \}$ or $P$ is false or $S_P = \emptyset$. Then, it would go to a more "functorial" proof based on the structure of $P$ and just assuming as an axiom that the statement is satisfied for atomic variables. $\endgroup$ Feb 6 '20 at 22:21
  • $\begingroup$ And then it would observe that based on a natural deduction proof of $\Gamma \vdash P$, and given an element of $S_Q$ for each $Q \in \Gamma$, you can recursively give an explicit element of $S_P$. Then, based on the fact that double negation elimination corresponds to a Hilbert epsilon operator, which is problematic because you don't really know what exactly you're getting out of it, you can wonder which proofs avoid the Hilbert epsilon in the translation and thus give a more explicitly explicit term. $\endgroup$ Feb 6 '20 at 22:24

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.