Intuitionistic Logic: Foundations and Distinctions from Classical Logic

1. The Constructivist Philosophy of Truth

The core of classical logic, which we've been studying, is built on the principle of bivalence: every proposition is either true or false, with no third option. This gives rise to the Law of the Excluded Middle (LEM), which states that for any proposition $A$, the statement $A\vee \neg A$ is always a tautology. It must be that either "the 100-billionth digit of $\pi$ is a 7" or "the 100-billionth digit of $\pi$ is not a 7," regardless of whether we can ever determine which is the case.

Intuitionism rejects this view. It is founded on a constructivist epistemology, which identifies truth with constructive proof or what is sometimes called "warranted assertability." For an intuitionist, a mathematical statement is true only if we possess a proof of it. It is false only if we possess a proof that it leads to a contradiction. If we have neither, the statement is simply not decided.

This has immediate and drastic consequences for the logical connectives.

• To assert the disjunction $A\vee B$, you must be in possession of a proof of $A$ or a proof of $B$.
• To assert the existential statement $\exists xP(x)$, you must be able to construct a specific object $c$ (a "witness") and a proof that $P(c)$ holds.

The following video provides an excellent introduction to this philosophical shift and its initial consequences.

The intuitionist's rejection of non-constructive proofs is not merely an abstract preference. Consider the following famous proof that there exist two irrational numbers, $a$ and $b$, such that $a^b$ is rational.

1. Consider the number ${\sqrt{2}}^{\sqrt{2}}$. This number is either rational or irrational (this is an appeal to LEM).
2. Case 1: If ${\sqrt{2}}^{\sqrt{2}}$ is rational, then we are done. We can set $a=\sqrt{2}$ and $b=\sqrt{2}$. We have found a pair of irrationals whose power is rational.
3. Case 2: If ${\sqrt{2}}^{\sqrt{2}}$ is irrational, then we can set $a={\sqrt{2}}^{\sqrt{2}}$ and $b=\sqrt{2}$. Then $a^b=({\sqrt{2}}^{\sqrt{2}}{)}^{\sqrt{2}}={\sqrt{2}}^{(\sqrt{2}\cdot \sqrt{2})}={\sqrt{2}}^2=2$. Since 2 is rational, we are again done.
4. Conclusion: In either case, such a pair of numbers exists.

A classical mathematician finds this proof perfectly valid. An intuitionist rejects it. Why? Because the proof does not construct the required pair. It tells us that one of two pairs must work, but it does not tell us which one. We haven't provided a specific witness. (As it happens, the Gelfond-Schneider theorem later proved that ${\sqrt{2}}^{\sqrt{2}}$ is indeed irrational, so the pair in Case 2 is the correct one, but this requires a much more complex, separate proof).

The following reading provides a more formal discussion of this constructivist viewpoint, often called the Brouwer-Heyting-Kolmogorov (BHK) interpretation.

2. Formal Divergence from Classical Logic

As the Attic Philosophy video noted, rejecting the Law of the Excluded Middle is not a simple tweak. It causes a cascade of failures for other classical principles that depend on it. Two of the most important are:

• The Law of Double Negation Elimination (DNE): In classical logic, $\neg \neg A\to A$ is a tautology. If a statement is not not-true, it must be true. For an intuitionist, this inference is invalid. $\neg \neg A$ means "there is a proof that assuming $\neg A$ leads to a contradiction," or "it is impossible for $A$ to be false." This is considered weaker than a direct, constructive proof of $A$. You can't derive positive information (a proof of $A$) from negative information (the impossibility of $\neg A$). However, note that the other direction, $A\to \neg \neg A$, remains valid in intuitionistic logic.

• Proof by Contradiction (Reductio ad Absurdum): The classical rule that allows you to prove $A$ by assuming $\neg A$ and deriving a contradiction is also rejected. This rule is equivalent to DNE. If you assume $\neg A$ and derive $\perp$ (absurdity), you have successfully proven $\neg \neg A$. But as we just saw, you cannot take the final step to conclude $A$.

The following resource provides a clear, itemized list of some key classical tautologies, showing which ones remain valid in intuitionistic logic and which ones do not.

3. Kripke Semantics: A Model for Growing Knowledge

How can we build a formal semantics for a logic that rejects bivalence? In the 1960s, Saul Kripke developed an elegant solution using model structures very similar to those we saw for modal logic.

Instead of "possible worlds," a Kripke model for intuitionistic logic consists of a set of states of knowledge. These states are related by an accessibility relation, $k_1\le k_2$, which can be interpreted as epistemic or temporal progression: $k_2$ is a future state of knowledge that can be reached from $k_1$. The key constraint is monotonicity: once a proposition is proven true at a state $k$, it remains true in all future states accessible from $k$. You don't un-learn things.

The truth conditions (or "forcing" conditions) for the connectives are defined relative to these states:

• $k\models A\wedge B$ iff $k\models A$ and $k\models B$.
• $k\models A\vee B$ iff $k\models A$ or $k\models B$.
• $k\models A\to B$ iff for all future states $k^{\prime }$ such that $k\le k^{\prime }$, if $k^{\prime }\models A$, then $k^{\prime }\models B$.
• $k\models \neg A$ iff for all future states $k^{\prime }$ such that $k\le k^{\prime }$, $k^{\prime }/\models A$. (This is equivalent to $A\to \perp$, where $\perp$ is never true at any state).

The conditions for implication and negation are the crucial ones. A conditional, $A\to B$, is not just about the current state; it's a guarantee about the future. It says, "From this point on, whenever you gain a proof of $A$, you will also have a proof of $B$." Similarly, a negation, $\neg A$, is a strong claim that $A$ can never be proven from this point forward.

This model beautifully explains the failure of the Law of the Excluded Middle.

The failure of LEM stems directly from this dynamic, forward-looking nature of knowledge. At our current state, we might lack a proof of $P$, so we cannot assert $P$. But we also cannot assert $\neg P$, because that would mean ruling out any possibility of ever finding a proof for $P$ in the future. The system leaves open the possibility for future discovery, thereby invalidating $P\vee \neg P$ as a universal tautology.

4. The Richness of Intuitionistic Logic

It might seem that intuitionistic logic is simply a weaker, impoverished version of classical logic. While it is true that not all classical theorems are intuitionistically valid, the relationship is more complex. Intuitionistic logic is, in some respects, more fine-grained and structurally richer.

One striking example is the failure of interdefinability for connectives. In classical logic, you can define $\vee$ and $\to$ using only $\wedge$ and $\neg$. This is not possible in intuitionistic logic; the connectives are independent.

Perhaps the most dramatic illustration of this increased complexity is in the number of distinct propositions. In classical logic, given a single propositional variable $p$, any formula using only $p$ is equivalent to one of just four forms: $p$, $\neg p$, $p\vee \neg p$ (always true), or $p\wedge \neg p$ (always false). In intuitionistic logic, there are infinitely many non-equivalent propositions that can be constructed from a single variable.

This lattice shows the first few of these infinite propositions. At the bottom, we have $\perp$ (falsum) and then branch up to $p$ and $\neg p$. Above them are familiar combinations like $p\vee \neg p$ and $\neg \neg p$, which are no longer equivalent to each other or to $p$ or $\top$ (tautology). This infinite hierarchy demonstrates that intuitionistic logic makes distinctions that classical logic collapses.

Conclusion

Intuitionistic logic represents a profound philosophical and formal departure from the classical tradition. By tying truth to constructive proof, it challenges some of our most basic logical intuitions.

Key Takeaways:

• Core Principle: Intuitionism is based on a constructivist philosophy where truth is identified with warranted assertability or constructive proof.
• Rejection of LEM: The central divergence from classical logic is the rejection of the Law of the Excluded Middle ($A\vee \neg A$). We cannot assert it unless we have a proof for $A$ or a proof for $\neg A$.
• Formal Consequences: Rejecting LEM leads to the failure of other key classical laws, most notably Double Negation Elimination ($\neg \neg A\to A$) and classical Proof by Contradiction.
• Kripke Semantics: Intuitionistic logic can be given a formal semantics using Kripke models, where "worlds" are interpreted as "states of knowledge" and the accessibility relation represents the monotonic growth of knowledge over time.
• Structural Richness: Far from being merely a "weaker" logic, intuitionism is more fine-grained, distinguishing between propositions (like $p$, $\neg \neg p$, and $p\vee \neg p$) that are equivalent in classical logic.

This journey into intuitionism shows that what we take to be "obvious" laws of logic are in fact deep philosophical commitments. By changing those commitments, we arrive at a completely different, yet internally coherent, way of reasoning.

Preview of the Next Lesson:

The Kripke models we used to understand intuitionistic logic are formally very similar to the possible-worlds semantics we used for modal logic. This raises a pressing metaphysical question: what exactly are these "possible worlds" or "states"? Are they genuine, existing universes as David Lewis's modal realism suggests? Or are they merely useful abstract tools, as a position like actualism would maintain? In our next lesson, we will pivot from formal logic to metaphysics to tackle this very debate.