10
$\begingroup$

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.

$\endgroup$

2 Answers 2

14
$\begingroup$

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 ^_^

$\endgroup$
13
  • 1
    $\begingroup$ Re: "Anything you prove intuitionistically has some "computational content" to it," the topic of proof mining (or unwinding, or term extraction) may be of interest. $\endgroup$ Jun 6, 2021 at 3:53
  • 1
    $\begingroup$ @SergeiAkbarov, I'm not entirely sure what you want. There is no intuitionistic proof of the de morgan's law $\lnot(p \land q) \to \lnot p \lor \lnot q$, for instance. Of course, if you allow letcc (and thus classical logic), then there is a program representing this. You can see example programs for the other 3 de morgan's laws, plus a discussion of the failure of this de morgan's law here. $\endgroup$ Jun 6, 2021 at 10:01
  • 1
    $\begingroup$ Halla, of course, I understand that some propositions cannot be proved in intuitionistic logic in contrast to the usual logic. The question is why this turns out to be useful in proggramming. Which kind of tasks do they consider, if intuitionistic logic is better for them than the classical logic? $\endgroup$ Jun 6, 2021 at 10:07
  • 1
    $\begingroup$ I don't know if it's "useful in programming". Rather, intuitionistic logic is a constructive logic, and when writing programs we typically construct things, seeing as that's the raison d'être for code. So the programming languages that arise in practice almost always give us intuitionistic proof systems. I recommend spending some time looking at letcc and callcc to see how to get a classical logic. At least for me, programs involving these functions are much harder to understand than those that don't, and I would argue (philosophically) this is because they're "nonconstructive" $\endgroup$ Jun 6, 2021 at 10:12
  • 1
    $\begingroup$ Halla, these "letcc" and "callcc" seem to be too far from me, I don't understand what they write about all this. If anyone could explain this to non-programmers like me, I would be grateful. Excuse me for my ignorance, and thank you for your answer. $\endgroup$ Jun 6, 2021 at 12:02
10
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .