What are the examples for intuitionistic logic?

Question

I have been curious about intuitionistic logic for some time and I want to know about it and I have a question, the law of the excluded middle and double negation elimination seem completely logical to me and I think they are always correct. But intuitionistic logic does not accept these two laws. What is the cause of this? Are there really propositions in mathematics for which these two principles do not hold? If so, please give examples of propositions that are examined in intuitionistic logic and the law of the excluded middle and double negation elimination does not work in them.

Answer 1

Let's take this in two stages.

(A) It is natural to think of a correct assertion as one that corresponds to some realm of facts (whatever that means exactly). But suppose just for a moment that we instead think of correctness as a matter of being warranted, where we understand this in the following strong sense: $A$ is warranted if and only if there is an informal proof which provides a direct certification for $A$'s correctness. Then here is a reasonably natural story about how to characterize the connectives in this new framework (it's a rough version of what's called the BHK -- Brouwer-Heyting-Kolmorgorov -- interpretation):

1. $(A \land B)$ is warranted iff (if and only if) $A$ and $B$ are both warranted.
2. While there may be other ways of arriving at a disjunction, the direct and ideally informative way of certifying a disjunction's correctness is by establishing one or other disjunct. So we will count $(A \lor B)$ as warranted iff at least one disjunct is certified to be correct, i.e. iff there is a warrant for $A$ or a warrant for $B$.
3. A warranted conditional $(A \to B)$ must be one that, together with the warranted assertion $A$, will enable us to derive another warranted assertion $B$ by using modus ponens. Hence $(A \to B)$ is directly warranted iff there is a way of converting any warrant for $A$ into a warrant for $B$.
4. $\neg A$ is warranted iff we have a warrant for ruling out $A$ because it leads to something absurd (given what else is warranted).
5. $\bot$ is never warranted.

Then, in keeping with this approach, we will think of a reliable inference as one that takes us from warranted premisses to a warranted conclusion.

Now, in this framework, the familiar introduction rules for the connectives will still be acceptable, for they will evidently be warrant-preserving (given our interpretation of the connectives). But the various elimination rules in effect just `undo' the effects of the introduction rules: so they should come for free along with the introduction rules. Finally, we can still endorse EFQ, ex falso quodlibet -- the plausible thought is that if, per impossible, the absurd is warrantedly assertible, then all hell breaks loose, and anything goes.

Hence, regarded now as warrant-preserving rules, all the usual rules of intuitionistic propositional logic can remain in place. And the standard intro/elim quantifier rules can stay in place too. However:

1. DN, double negation elimination will not be acceptable in this framework. We might have a warrant for ruling out being able actually to rule out $A$, so we can warrantedly assert $\neg\neg A$. But that doesn't put us in a position to warrantedly assert $A$. We might just have to remain neutral about $A$
2. Likewise LEM will not be acceptable. On the present understanding of the connectives, $(A \lor \neg A)$ would be correct, i.e. directly warranted, just if there is a warrant for $A$ or a warrant for ruling out $A$. But must there always be a way of justifiably deciding a conjecture $A$ in the relevant area of inquiry one way or the other? Some things may be beyond our ken.

In sum, then, if we want a propositional logic suitable as a framework for regimenting arguments which preserve warranted assertability, we should stick with the core rules of intuitionistic propositional logic -- and shouldn't endorse those further distinctively classical laws.

(B) But of course that leaves it open whether we should think of correctness for mathematical claims as a matter of being warranted by some informal proof. Perhaps you are, for example, a platonist, who thinks that mathematical reality is in some sense "out there" independent of us, and mathematicians are aiming to correctly describe how things stand in this abstract realm. People have been arguing about whether some sort of conception really makes sense ever since the time of ...Plato!

But you can perhaps glimpse why some find that thinking of mathematics as a realm where truth doesn't/can't outstrip informal provability/constructability is not a mad-dog crazy idea (and perhaps platonism is the really problematic position)!

OK: maybe you don't want to tangle with such philosophical conundrums. Fair enough. Let's be ecumenical. There will still be interest in demarcating those bits of mathematics which are constructively respectable, and where intuitionist versions of arithmetic, analysis, set theory etc. can take us, as against those further bits of mathematics where we do essentially depend on using excluded middle. After all, it is always good to know, of a true disjunct, which disjunct is the warranted one, or given a true existential quantification $\exists xFx$ it's good to have a witness $Fa$. Sticking to intuitionistic reasoning gives us that.

So we can sensibly still be very interested in the reach of intuitionistically acceptable mathematics even if we have no particular beef with excluded middle.

With all that by way of more background motivation, try the Wikipedia article that @Karl helpfully links to!

Answer 2

A practical application of intuitionistic logic comes up naturally in the study of modern algebraic geometry.

To be brief, algebraic geometry is the study of the geometry of solution sets to systems of polynomial equations. At some point, it becomes useful to study the sheaf of regular functions on such an object. This means that we are interested in rational functions defined on "open" subsets; here the notion of "open" is given by the Zariski topology, where we just want to impose some conditions that certain other polynomials are nonzero. More generally, we can have functions which look like rational functions only locally.

However, it then turns out that if you generalize to sheaves of sets (as opposed to the sheaves of abelian groups, or sheaves of modules over a sheaf of rings, that are usually studied in algebraic geometry), then that category of sheaves of sets can naturally be given what is known as an "internal logic", which gives a "type theory" which acts very close to usual mathematics. The big difference is that in general, excluded middle and double negation elimination do not hold in this internal logic.

The usefulness then comes in being able to use the internal language of a topos to define interesting objects in the category of sheaves of sets. Also, if you have any statement which is formally provable in the internal logic, then it will always hold on any sheaves of sets. That can sometimes be useful in clarifying what otherwise could be a confusing proof involving passing to refinement covers multiple times.

So, even if you believe that the universe containing the objects of algebraic geometry satisfies the law of excluded middle, you still get interesting models of intuitionistic logic which do not satisfy excluded middle, and for which theorems of this version of intuitionistic logic can give useful information in the original universe.

(Modern algebraic geometry also studies so-called "Grothendieck sites" which generalize the example of Zariski topology: the etale sites, the crystalline site, etc. You can also define sheaves of sets on these sites, and they also have a straightforward generalization of the internal logic.)

Answer 3

There are already some insightful answers; below are some comments, from the perspective of a intuitionism-sympathetic dynamicist.

---

As a non-logician I tend to think of logic as a framework one can use to approach mathematics; so a mathematical statement is true w/r/t this or that logic. Thus instead of asking whether for proposition $P$ the law of excluded middle holds, it seems to me it's more meaningful to ask if proposition $P$ has a proof that never refers to the law of excluded middle. (Whether or not a statement has a proof has also a time dependency, among other dependencies; otherwise one would e.g. need to forgo a distinction between theorem and conjecture (this indeed is done, at least partially); let us suppress this line of thought).

In the case of intuitionism, roughly speaking one simply does not take negation to be an idempotent. Thinking of mathematical statements as nodes and (steps of) proofs as edges, this suggests a caricature: The graph/category/space that is mathematics w/r/t intuitionistic logic is a branched double cover of the graph/category/space that is mathematics w/r/t standard logic.

Another way to think about this "branched double cover" in standard v intuitionistic logic is that any statement in standard logic has a corresponding statement in intuitionistic logic $(\ast)$, but not vice versa. Thus one can translate like this: Statement $P$ w/r/t classical logic means precisely statement $\neg\neg P$ w/r/t intuitionistic logic; there is also the statement $P$ w/r/t intuitionistic logic, but in general this is a strictly stronger statement than $\neg\neg P$. Sometimes it is indeed the case that not only is $P$ true w/r/t classical logic, but $P$ is true w/r/t intuitionistic logic. (My use of the word "branched" above is meant to signify this conditional coincidence.)

As a simple example, the classical statement "$1$ added to itself is $2$" translates to intuitionistic language/framework as "it is not the case that $1$ added to itself is not $2$" (further insinuating that $1$ added to itself perhaps is also not $2$; and that whether $1$ added to itself is $2$ requires further investigation).

There are parallel discussions of the uses and misuses of double negations in literature, rhetoric, and politics (it's a fun exercise to spot them out in the wild).

$(\ast)$ For reference purposes, see p.13, Thm.3.2.1 in Troelstra's book Principles of Intuitionism, where the precise statement of this translation is attributed to Gödel.

---

Continuing, I also don't think it is fruitful to think of intuitionism as a taking away of tools; from this perspective it indeed makes little sense. Instead, it's perhaps better to think of it as a framework facilitating deeper understanding. If memory serves right Manin's book Mathematics as Metaphor includes relevant discussions.

For instance another such restriction would be to formalize memory management needed for an idealized mathematician to read a certain proof (recently Ruelle in the talk "A Natural Limitation for Properly Human Scientific Progress" (available at https://youtu.be/jSul7BRj57k) has made before the (paraphrased) point that mathematical proofs simply keep getting larger and more complicated, with the number of variables one needs to keep in mind to even read a proof growing in an uncontrolled manner). And indeed, in computer science for quite a while there has been attempts (to say the least) to formalize memory management (to prove that a given program does do what it is supposed to do, without messing up the memory structure of the computer it's run on).

It's also good to keep in mind the recent developments in proof checkers (e.g. Lean), which surely also relates to intuitionism/constructivism in subtle ways. (Continuing from Ruelle's point, if things continue this way, we will need computer assistance to read proofs asymptotically; "we" here is meant to be along the lines of "a significant percentage of mathematicians".)

More broadly, intuitionism seems to be pointing a certain unification of mathematics and computer science, with the motto "Proofs are programs. Programs are proofs." (it seems depending on one's background one uses either of these sentences to essentially mean the same thing.)

---

Finally here is a concrete example that at the very least provides an opportunity to appreciate the difference between the classical and intuitionistic approach. Consider the statement

$$ \exists a,b\in\mathbb{R}\setminus\mathbb{Q}: a^b\in\mathbb{Q}. $$

In introductory courses this is given to practice the so-called "proof by case analysis": either $\sqrt{2}^{\sqrt{2}}$ is rational, xor $\left(\sqrt{2}^{\sqrt{2}}\right)^{\sqrt{2}}$ provides an example. Often this discussion follows right after the proof that $\sqrt{2}$ is irrational, hence the educated guess of using $\sqrt{2}$ somehow.

From the classical point of view, this is valid, but from the intuitionistic point of view, the argument still proves something, albeit something much more weaker.

See also Real Numbers to Irrational Powers, Proofs that every mathematician should know., Constructive proof of the irrationality of $\sqrt{2}^{\sqrt{2}}$. for further discussions on this particular example.