Every tautology survives double negation

Intuitionistic logic began as a refusal. L. E. J. Brouwer objected that a mathematician who proves “$A$ or not $A$” has proved nothing unless the proof says which, and that a proof of “not not $A$” — a demonstration that $A$ cannot be refuted — is not yet a proof of $A$. The middle that is not excluded showed the consequence: the law of excluded middle, $P \vee \neg P$, is not intuitionistically valid, and nor is double-negation elimination, $\neg\neg P \to P$. Much else goes with them. Peirce’s law, one of De Morgan’s laws, the reading of $P \to Q$ as $\neg P \vee Q$: all are classical tautologies that intuitionistic logic does not prove.

How much does it refuse? In 1929 Valery Glivenko gave a startling answer for propositional logic: nothing at all. Every classical tautology is not refuted but merely held back. Put $\neg\neg$ in front of it and intuitionistic logic proves it. The two logics agree on what cannot be false; they disagree only on what has been shown to be true. This essay tests that claim by brute force, on every small model of intuitionistic logic and every small formula, and then shows exactly where it stops.

The open-set picture #

The hero uses the topological reading of intuitionistic logic that the earlier essay developed. A statement’s truth value is an open set of the real line, where it is known to hold. Conjunction and disjunction are intersection and union, and the negation of $U$ is the largest open set disjoint from $U$ — the interior of its complement. Take $p$ to be the positive numbers. Then $\neg p$ is the negative numbers, and $p \vee \neg p$ is everything except the point 0, where neither is known. Excluded middle fails at one point.

Now negate again. $\neg(p \vee \neg p)$ is the largest open set avoiding everything but 0, and an open set cannot be a single point, so it is empty. Its negation, $\neg\neg(p \vee \neg p)$, is the whole line. The law is not true, but it is not false either, in the strongest possible sense: its refutation is nowhere. Glivenko’s theorem says this is not special to excluded middle or to the real line. Every classical tautology, doubly negated, is true everywhere in every model.

Kripke’s states of knowledge #

The finite tool for testing this is Saul Kripke’s semantics of 1965. A Kripke model is a set of states of knowledge, partially ordered by “can develop into”, with each propositional letter established at an upward-closed set of states: once known, always known. A conjunction or disjunction holds at a state if its parts do there. An implication $A \to B$ holds at a state if, at every later state where $A$ is established, so is $B$. And $\neg A$, which is $A \to \bot$, holds at a state if $A$ is never established at any later state.

The smallest countermodel to excluded middle has two states. At the later one $p$ has been established. At the earlier one $p$ is not yet known, but $\neg p$ does not hold either, because $p$ will be established. So at $w_0$ the disjunction fails. But $\neg(p \vee \neg p)$ would need the disjunction never to hold later, and at $w_1$ it holds; so $\neg(p \vee \neg p)$ fails at both states and $\neg\neg(p \vee \neg p)$ holds at both. The same model refutes $\neg\neg p \to p$: at $w_0$, $\neg\neg p$ holds — $p$ cannot be ruled out — and $p$ does not.

Intuitionistic propositional logic has the finite model property, the subject of refutable in something small: a formula that is not valid has a finite countermodel, and its size is bounded in terms of the formula. So searching all small Kripke models is a genuine test, complete for formulas whose countermodels fit in the search.

Eight laws, refuted and rescued #

The search runs through every partial order on up to four labelled states with one state below all others, and every way of choosing upward-closed sets for $p$ and $q$. Excluded middle, double-negation elimination, Peirce’s law $((p \to q) \to p) \to p$, contraposition in the backward direction and the reading of implication as a disjunction each fail in a two-state model. De Morgan’s law $\neg(p \wedge q) \to \neg p \vee \neg q$, the weak excluded middle $\neg p \vee \neg\neg p$ and the linearity law $(p \to q) \vee (q \to p)$ each need three states, arranged as a fork: knowledge that can develop in two incompatible ways. In a model whose states form a single chain these three laws hold; they are the laws that fail only when the future branches.

Then the same search runs on each law with $\neg\neg$ in front, and it finds no countermodel at all. The four-state models tried include every way two letters can be learned along every shape of development up to that size, and in none of them can any of the eight laws be refuted.

The laws that need a fork #

The three laws that need three states mark out logics of their own. Adding linearity to intuitionistic logic gives the logic Michael Dummett studied in 1959, which is exactly the logic of Kripke models that are chains, and which Gödel had met in 1932 as the limit of his finite truth tables. Adding the weak excluded middle gives a logic, sometimes called the logic of De Morgan’s law, whose models are the ones in which any two states have a common later state. These are two of the infinitely many intermediate logics between intuitionistic and classical, the subject of not one step but a continuum, and each is characterised by a shape of development that its models are allowed to have.

Glivenko’s theorem holds for every one of them, for the same reason: each is contained in classical logic and contains intuitionistic logic, and the double negation of a tautology is already provable in the weakest. So the whole continuum of intermediate logics agrees, on double negations, with classical logic. What separates them is only which tautologies they accept without the $\neg\neg$, and with two letters that question already has an infinite and intricate answer, as the universal model for two letters showed.

Every formula, up to a size #

Eight laws are a sample. A census does better: list every formula built from $p$, $q$ and $\bot$ with implication, conjunction and disjunction, up to a given number of symbols, and test each in three ways — by truth table for classical validity, by searching for a countermodel among all Kripke models of up to three states, and by the same search on its double negation.

Up to size 7 there are 11,451 formulas, of which 3,116 are classical tautologies. Of those, 2,850 have no countermodel among the small Kripke models — these are, very nearly, the tautologies intuitionistic logic accepts as they stand. The other 266 are refuted, each by some model of at most three states. And the double negation of a formula has no countermodel for exactly the 3,116 tautologies: the agreement is checked formula by formula, not merely in total. Not one non-tautology has an unrefuted double negation, and not one tautology has a refuted one.

The direction from intuitionistic to classical is automatic: a Kripke model of a single state is a classical truth assignment, so anything true in every Kripke model is a tautology, and $\neg\neg A$ classically means $A$. The content of Glivenko’s theorem is the other direction, and the census shows it holding with no exceptions in its range.

What the double negation records #

In a Kripke model, $\neg\neg A$ holds at a state when every later state can be developed further to a state where $A$ holds: $A$ is not established, but no development can rule it out. On a finite tree that means every branch upward eventually reaches $A$. At state 2 of the figure both branches reach $p$; at state 1 the branch through state 4 never does, so $\neg\neg p$ fails there.

The proof of Glivenko’s theorem uses this reading. In a finite model every state can be developed to a maximal state, one with nothing above it, and at a maximal state intuitionistic truth is classical truth, since there is no future to wait for. So a classical tautology holds at every maximal state, and therefore every state can be developed to one where it holds: its double negation holds everywhere. The finite model property finishes the argument, because a formula with a countermodel has a finite one.

Two truth values, recovered #

There is a cleaner way to say what the theorem achieves. Gödel showed in 1932 that no finite table of truth values captures intuitionistic logic: whatever finite set of values one tries, some non-theorem comes out as always true. The formulas of the form $\neg\neg A$, however, behave exactly like classical formulas. They form a fragment of intuitionistic logic in which the two-valued truth table is correct, and Glivenko’s theorem is the statement that this fragment is a faithful copy of classical propositional logic. Intuitionistic logic contains classical logic, not as a part of its theorems, but as its doubly negated shadow.

The dual phenomenon appears in the logics of paradox, where a contradiction can stay where it is without spreading. There the classical tautologies all survive, and what is lost is some of the classical inferences; in intuitionistic logic the inferences survive and the tautologies are weakened by a double negation. The two departures from classical logic are, in this precise sense, on opposite sides of it.

Where the theorem stops #

For statements about all objects the theorem is false. In the figure’s model the states form an endless chain and a new object appears at each one, acquiring the property $P$ one state later. At the first state, every object that exists or will exist eventually has $P$, so $\forall x\,\neg\neg P(x)$ holds. But at no state is $P$ known of every object present, because the newest object never has it yet; so $\forall x\,P(x)$ is never established, $\neg\forall x\,P(x)$ holds at every state, and $\neg\neg\forall x\,P(x)$ holds at none. The double negation cannot be moved through a universal quantifier, and the classical tautology $\forall x\,P(x) \vee \neg\forall x\,P(x)$ has a double negation that is not intuitionistically valid.

The model needs infinitely many states, which is why the first-order case escapes the finite argument above: there is no maximal state to reach. Sigekatu Kuroda found the repair in 1951. Insert $\neg\neg$ not only in front of the whole formula but also immediately after every universal quantifier; then every classical first-order theorem becomes an intuitionistic one. Kurt Gödel and Gerhard Gentzen had found related negative translations in 1933, which insert double negations at the atoms and turn disjunctions and existentials into negated conjunctions and universals, and these show that classical arithmetic is consistent if intuitionistic arithmetic is — so that classical reasoning about whole numbers can never lead to a contradiction unless intuitionistic reasoning already does.

How little intuitionistic logic gives up #

The surprise is how little intuitionistic logic loses. It was designed to reject a whole style of reasoning — proof by contradiction of a positive statement, case analysis on undecided alternatives — and yet, on propositional formulas, it can still prove that every classical law is irrefutable. The difference between the two logics is not a difference in what is true but in the strength of the claim: classical logic says “$A$”, and intuitionistic logic, from the same premises, says “$A$ cannot be refuted”. A proof that says which half showed the positive side of this: when intuitionistic logic does prove a disjunction, it proves one of the disjuncts. Glivenko shows the negative side: it never denies a classical disjunction either.

For a working mathematician the theorem has a practical reading. Any propositional argument that a classical mathematician makes can be replayed intuitionistically, provided the conclusion is weakened to its double negation; and for many statements — negations themselves, and equations between whole numbers that can be checked — the double negation is as good as the statement, because $\neg\neg\neg A$ is equivalent to $\neg A$ and a decidable statement can be checked directly. The loss is concentrated in statements that claim the existence of something without saying which.

There is a parallel in modal logic. Gödel, McKinsey and Tarski showed that intuitionistic logic can be embedded in the modal logic S4 by reading each statement as “it is provable that”, the same reading behind provability logic, and under that embedding the double negation becomes “it is provable that it is consistent that”. The open sets of the hero are the topological picture of the same S4 necessity, the interior operator.

Models searched only to four states #

The searches are bounded. Every rooted Kripke model of up to four states was tried for the eight laws, and up to three states for the census; a formula whose double negation failed only in a larger model would not be caught. Glivenko’s theorem guarantees there is none, and the finite model property bounds the size of countermodels in terms of the formula, but the bound for size-7 formulas is larger than three states, so the census is evidence consistent with the theorem, not a proof of it. Likewise the count of 2,850 formulas with no small countermodel is an upper bound on the intuitionistically valid ones of that size.

The first-order model is described in a finite drawing of five states; its point depends on the chain going on for ever, which no figure can show.

Kripke models enumerated, Glivenko quoted #

Computed here: every partial order on up to four labelled states with a least state — 1, 3 and 19 of them on two, three and four states — with every upward-closed valuation of two letters; the forcing relation for every formula tested; the smallest countermodels of the eight laws and the absence of countermodels to their double negations; all 11,451 formulas up to size 7 and their classical, intuitionistic and double-negation status, agreeing formula by formula; the tree of seven states; and the open sets of the hero.

Quoted: Glivenko’s theorem of 1929; Kripke’s semantics; the finite model property; Kuroda’s translation of 1951 and the negative translations of Gödel and Gentzen; the Gödel–McKinsey–Tarski embedding into S4.

Still open: how much classical logic hides in other logics #

Glivenko’s theorem has analogues for many logics between intuitionistic and classical, and for some it fails. For which intermediate logics does double negation recover classical logic, and for which first-order theories does Kuroda’s translation preserve provability? For propositional intermediate logics the answer is known: Glivenko’s theorem holds for exactly those whose double negations behave as in intuitionistic logic, a condition that can be checked on their models. For first-order theories it depends on the axioms, and for theories of analysis and set theory with intuitionistic logic, which statements survive translation and which need choice principles or more is studied case by case. The finer question — how short the intuitionistic proof of $\neg\neg A$ can be compared with the classical proof of $A$ — is open in general; translations can multiply proof length, and whether that blow-up is ever unavoidable is a question in proof complexity that has not been settled.

Never refuted, only held back #

A propositional formula is a classical tautology exactly when its double negation is intuitionistically valid, so intuitionistic logic rejects no classical law outright; it only declines to affirm what it cannot construct. Excluded middle fails at one point of the line and at one state of a two-state model, while its double negation holds everywhere. Eight classical laws fall to models of two or three states, and their double negations to none of up to four; among 11,451 formulas the double negation is unrefuted for exactly the 3,116 tautologies. With quantifiers the theorem breaks, in a model whose domain grows for ever, and Kuroda’s extra negations are needed.