Applications of intuitionistic logic

Question

Can anybody enlighten me about the applications of intuitionistic logic? I am familiar with this system only by G.Takeuti's book, where it is described as one of the examples of axiomatic systems of logic. Is it possible to explain to a non-specialist why this system deserves studying?

I suspect that this is easier to explain on the example of propositional intuitionistic calculus, so if somebody could cast a light on this, this would be especially valuable.

Answer 1

One fun answer is "programming languages". It turns out a good way to study programming languages is by viewing them as proof systems, and the programming languages you get in this way tend to be intuitionistic proof systems. You can build programming languages which correspond to classical logic (using letcc and continuations, for instance. See here), but they're less common.

The correspondence goes both ways, too! Anything you prove intuitionistically has some "computational content" to it. So there's a very real sense in which you can run your proof like a program, and in fact most proof systems work in this way. Much ink has been spilled on this subject, so I won't go into it in this answer (see here, here, and here for instance. Plus here for an example of this being done "in the wild").

If you want a great reference for building programming languages with logic, I heartily recommend Harper's Practical Foundations for Programming Languages (lovingly referred to as $\mathsf{PFPL}$ in at least a few of the things I've linked so far).

---

I hope this helps ^_^

Answer 2

The internal logic of a topos is inherently intuitionistic, not classical. This means that if we want to "prove a fact in all topoi (satisfying some conditions)," we should generally look for constructive arguments.

Even if we don't care about the internal structure of a topos, this is still worth thinking about since we may then be able to "de-toposify" the result we get to arrive at a purely classical fact (usually involving sheaves somehow). For example, see this answer of Ingo Blenschmidt where he shows roughly that a particular constructive argument about rings yields the classical fact that for $X$ a reduced scheme and $\mathcal{F}$ an $\mathcal{O}_X$-module of locally finite type, $\mathcal{F}$ is locally free iff its rank is constant.