Intuitionistic Logic and Kripke Semantics

A standard proof that there exist irrational $a$ and $b$ with $a^b$ rational goes as follows. Consider $\sqrt{2}^{\sqrt{2}}$. If it is rational, take $a = b = \sqrt{2}$. If it is irrational, take $a = \sqrt{2}^{\sqrt{2}}$ and $b = \sqrt{2}$, since then $a^b = 2$. Either way the pair exists.

The proof is valid and it does not tell one which pair works. It establishes an existence claim by case analysis on a disjunction neither disjunct of which has been settled, and the disjunction is an instance of excluded middle. The tradition this article describes holds that such a proof does not establish what it claims to establish, and rebuilds logic accordingly.

The interpretation

The rejection is not the claim that some sentence is neither true nor false. Intuitionistic logic proves $\neg \neg (\varphi \lor \neg \varphi)$, so no instance of excluded middle can be refuted. What is denied is the assertion, not the instance, and the difference tracks a change in what assertion requires.

Read this way the failure of excluded middle is immediate. A proof of $\varphi \lor \neg \varphi$ would be a proof of $\varphi$ or a refutation of it, together with an indication of which, and for an arbitrary $\varphi$ there is no such thing. The reading also explains what does survive: double negation introduction holds, since a proof of $\varphi$ yields a transformation of refutations of $\varphi$ into contradictions, while the converse fails, since a demonstration that no refutation exists is not itself a construction.

Exactness comes from two metatheorems about intuitionistic arithmetic. The disjunction property says that if the theory proves $\varphi \lor \psi$ then it proves one of them. The existence property says that if it proves $\exists x\, \varphi$ then it proves $\varphi[\bar{n}/x]$ for some numeral. Classical arithmetic has neither, which is the precise sense in which the opening example is not constructive. The properties are not axioms but theorems about the system, proved by Kleene's realisability interpretation in 1945 and also obtainable from cut elimination.

Kripke semantics

Heyting's system had no semantics for over twenty years. Kripke supplied one in 1965, and it is the relational semantics of the modal articles with a different reading and an extra condition.

A model is a partially ordered set of stages together with, at each stage, a set of atoms treated as established. The order is read as the growth of information over time or the extension of a body of evidence, and the interpretation of the connectives is by what will have been established.

The clauses that matter are the ones where monotonicity forces a departure from the classical case. Conjunction and disjunction are evaluated at the stage. Implication is not: $\varphi \rightarrow \psi$ holds at a stage when at every later stage at which $\varphi$ holds, $\psi$ holds too. Negation follows, since $\neg \varphi$ holds at a stage when $\varphi$ holds at no later stage. Both look ahead, because a conditional asserted now must survive whatever is established later.

Excluded middle now fails visibly. Take two stages, one below the other, with an atom $p$ established only at the later one. At the earlier stage $p$ does not hold, and $\neg p$ does not hold either since $p$ holds later. So $p \lor \neg p$ fails at the earlier stage, and the model refutes the schema. Double negation elimination fails in the same model, since $\neg \neg p$ holds at the earlier stage while $p$ does not.

The relation to modal logic is exact rather than analogical. Gödel observed in 1933 that translating intuitionistic formulas by prefixing boxes at the right places embeds intuitionistic propositional logic faithfully into S4, so that a formula is intuitionistically provable exactly when its translation is an S4 theorem. The Kripke models of the two systems are the same objects, a partial order being a reflexive transitive relation that is also antisymmetric, and the embedding was found before either semantics existed.

Next

The BHK reading treats a proof of a conditional as a construction turning proofs into proofs, which is to say a function. That is not a metaphor, and the next article establishes the correspondence exactly: proofs are programs, formulas are types, and proof normalisation is computation.