A proof that says which half

Classical logic can prove that one of two things is true without being able to say which. The standard example is short: either $\sqrt2^{\sqrt2}$ is rational, in which case it is a rational number that is an irrational raised to an irrational power, or it is irrational, in which case raising it to the power $\sqrt2$ gives $2$ and that is the example. The proof establishes a disjunction and leaves both halves open. It is a perfectly good classical proof, and it contains no information about which half holds.

The constructive system cannot do that. If it proves $A \vee B$, then it proves $A$ or it proves $B$. That is the disjunction property, and it is the most concrete way to say what dropping the excluded middle buys: a proof of an “or” is a proof of one side together with a label saying which.

It sounds like a statement about proofs, which it is, and it has a proof made entirely of pictures. The pictures are the stages-of-knowledge models from the first essay on the subject, and the proof is one operation on them.

The operation: put a new stage underneath #

A Kripke model is a set of stages ordered by later than, with a record of which atomic statements are known at each stage. Knowledge only grows: an atom known at a stage stays known at every later stage. A compound formula is forced at a stage by the constructive rules — an implication, for instance, is forced when every later stage that forces its antecedent also forces its consequent — and the constructive system proves exactly the formulas forced at every stage of every model.

Given two models, glue them: take both, keep all their stages and all their orderings, and add one new stage below the first stage of each, at which no atom is known. The result is a model again — knowledge still only grows, since the new stage knows nothing — and each of the old models sits inside it unchanged, because what a stage forces depends only on the stages at and after it.

That picture is the entire refutation of excluded middle in the Kripke semantics, and it has been met before as a single figure. What is new is reading it as an instance of a general operation. The two models on the left are each classical — one stage, which is a row of a truth table — and each forces $p \vee \neg p$, because in a single stage every atom is either known or never will be. The glued model is the first model that is not a truth table, and its first stage forces neither half.

Why neither half survives #

The argument that the new stage forces neither disjunct is two lines, and it uses only that forcing is persistent.

Suppose the constructive system proves neither $A$ nor $B$. By completeness each has a countermodel: a model with a first stage at which $A$ is not forced, and another at which $B$ is not forced. By the finite model property these can be taken finite — the same kind of shrinking that cuts a modal model down to what a formula can see — which does not matter for the argument but does matter for drawing it. Glue them. If the new first stage forced $A$, then by persistence every later stage would force $A$ too, including the first stage of the countermodel to $A$, which does not. So the new stage does not force $A$, and by the same reasoning it does not force $B$. A disjunction is forced at a stage exactly when one of its halves is, so $A \vee B$ is not forced at the new stage, and by soundness the constructive system does not prove $A \vee B$.

Read in the other direction: whenever the system proves $A \vee B$, it proves one of them. The glue turns two failures into a failure of the disjunction, and that is the property.

Nothing in the argument looked at what $A$ and $B$ say. The countermodels in this second picture have two stages each rather than one, and in the first of them the later stage is what refutes $\neg p$; the glue does not care about any of that. It places them side by side above a common beginning, and the beginning inherits the ignorance of both.

The disjunction property is sometimes stated as a slogan about constructive proof — that a proof of “$A$ or $B$” must contain a decision between them — and the slogan is justified by the syntax: in a derivation with no detours, the last step of a proof of $A \vee B$ is the rule that introduces the “or”, and its premise is a proof of one side — the same rule natural deduction uses to build a disjunction, read backwards. That is how the property was first proved, from a normal form for derivations. Under the reading of derivations as programs, a proof of $A \vee B$ is a value tagged left or right, and running the proof reads the tag. The gluing argument reaches the same statement from the models’ side, with no derivations at all.

The argument does not stop at two. Given countermodels to $A_1$, $A_2$, …, $A_n$, glue all of them at once, as $n$ branches above a single new stage; the new stage forces none of the $A_i$, so the system proves none of the disjunctions $A_1 \vee \dots \vee A_n$. A proof of a many-way “or” names one of its branches, by the same picture with more branches.

The irrational example, done the other way #

The classical proof about $\sqrt2^{\sqrt2}$ is the textbook case of a disjunction proved without a half, and it is worth seeing that the statement it proves is not the problem. The statement is that some irrational number raised to some irrational power is rational, and that has a constructive proof with a named witness: $\sqrt2^{\,\log_2 9} = 2^{\frac12 \log_2 9} = 2^{\log_2 3} = 3$. Both $\sqrt2$ and $\log_2 9$ are irrational — the second because $2^{a/b} = 9$ would make $2^a = 9^b$, an even number equal to an odd one — so the pair is an explicit example, and the proof says which.

What the classical proof lacks is only the decision it pushed onto the excluded middle. It is now known which half of its disjunction holds — $\sqrt2^{\sqrt2}$ is irrational, and in fact transcendental, by the Gelfond–Schneider theorem — but that fact is a deep result, and the classical proof is correct without it. The constructive system would not accept the proof as written; it accepts the one through $\log_2 9$, which carries its own witness, and it would accept a proof of the Gelfond–Schneider case, which settles the half the classical proof left open.

This is the pattern the disjunction property predicts. A constructive proof is not forbidden from reaching the same conclusions as a classical one; it is forbidden from reaching a disjunction without settling it, and so it is pushed toward the proofs that contain more information.

Why classical logic has no room for it #

Classical logic proves $p \vee \neg p$ and proves neither $p$ nor $\neg p$, so it does not have the property. In the pictures, the reason is that classical logic’s models are one-stage models only, and gluing two one-stage models does not give a one-stage model. The glue produces something outside the class, and a logic whose models are all of one shape cannot use a construction that produces another.

That is the whole mechanism, and it applies to every logic between the constructive system and the classical one. There are uncountably many, each defined by extra axioms, and each extra axiom restricts which models count. If the glued model of two allowed models is still allowed, the argument goes through inside that logic. If it is not, the argument has nowhere to stand, and the logic may well prove a disjunction without proving either half.

The two named logics met earlier are the clean cases, because their axioms are themselves disjunctions with unprovable halves.

Two logics that cannot glue #

Gödel–Dummett logic adds the linearity axiom, $(p \to q) \vee (q \to p)$: any two statements are comparable, in the sense that one implies the other. Its models are the ones whose stages form a single line, and the constructive system proves neither half of the axiom — the one-stage model knowing $p$ and not $q$ refutes the first, the one knowing $q$ and not $p$ the second.

Glue them, and the glued model is exactly the counterexample to linearity: a first stage with two incomparable futures, one where $p$ is learned and one where $q$ is. So the logic proves $(p \to q) \vee (q \to p)$, by fiat, and proves neither half, and its models are closed under every operation except the one the property needed. The fork is the shape the axiom was written to exclude.

The weak law is the same story with a different forbidden shape. $\neg p \vee \neg\neg p$ says that a statement is either refutable or irrefutable, and its models are the ones in which every stage has a single final stage above it — all futures eventually agree. Two one-stage models that disagree about $p$ glue into a model with two final stages that disagree forever, which is precisely what the axiom rules out.

In both cases the logic’s own axiom is the witness that the property fails, and the glue is the reason. The property and the frame class are the same fact seen from two sides: a logic whose models are closed under gluing has the disjunction property, and a logic that forbids the glued shape has an axiom that is a disjunction it cannot resolve.

A census of small frames, glued #

The two examples used one-stage models. A census makes the same point more broadly, and shows where the simple picture stops.

There are four rooted frames with at most three stages: one stage, two in a row, three in a row, and a fork. The census checks the frame conditions rather than assuming them — for instance, that the chains are exactly the small frames validating linearity — and then glues every pair within each logic’s class.

The first three rows say what the examples said. The constructive system keeps every glued frame, since it has no condition to violate. Gödel–Dummett logic loses every one: a glued pair of chains is never a chain, however long the chains. The logic of the weak law loses every one too, for the same reason in another shape.

The fourth row is the interesting one. Kreisel–Putnam logic adds an axiom about how a negated hypothesis distributes over a disjunction, $(\neg p \to q \vee r) \to (\neg p \to q) \vee (\neg p \to r)$. All four small frames validate it, and of the ten glued pairs six still do and four do not. So the naive glue does not stay inside the class. And yet the logic has the disjunction property: Kreisel and Putnam proved it in 1957, and in doing so refuted Łukasiewicz’s conjecture, made a few years earlier, that the constructive system was the only logic strictly between it and classical logic with the property.

The census does not contradict that. Closure under the plain glue is enough for the property, not necessary. A logic can keep the property by showing that, whenever two countermodels exist, some other countermodel to the disjunction exists inside the class — a glue followed by a repair, or a different construction altogether. Kreisel–Putnam logic has such a repair; the census shows only that it needs one.

What the property says, and what it does not #

It is a statement about proof, not truth. Every classical model of $p \vee \neg p$ makes one of the halves true. What classical logic lacks is not a true half but a proved one, and the disjunction property is exactly the demand that the proof carry the choice with it. That is the constructive reading of “or” made into a theorem about a system, and it is why the first essay on the subject described proofs as constructions rather than as certificates of truth.

It is not decidability. The constructive propositional system is decidable, and classical propositional logic is too; one has the property and one does not. The property says a proof of a disjunction yields a proof of a half. It says nothing about how hard it is to find either — though, in this case, finding the half is no harder than checking the proof.

It has a sibling for “there exists”. In predicate logic the same argument, with the glue done over domains of objects, gives the explicit witness property for suitably simple statements: a constructive proof that something exists yields a term naming it. That is the property program extraction relies on, and it fails classically for the same reason: a classical proof of existence can proceed by refuting non-existence, and a refutation names nothing.

It is fragile. One axiom that forbids a glued shape is enough to remove it, and which of the continuum of logics keep it, and how to recognise them, is not settled. Infinitely many logics besides the constructive one have it, Kreisel–Putnam logic being the first found.

What the pictures cannot show #

Each figure is a single model, and the property is about all of them. The drawings show countermodels for particular formulas and one glued model each. The theorem is that the glue works for every pair, which the figures illustrate but cannot establish; the establishment is the two-line persistence argument, and the census checks only the small frames.

The completeness theorem is doing invisible work. The glue turns two countermodels into one. That a formula the system does not prove has a countermodel is completeness, and that the countermodel can be taken finite is the finite model property. Neither appears in any picture, and without them the pictures would be examples rather than a proof.

Kreisel–Putnam logic’s repair is not drawn. The census shows that the plain glue leaves the class, and the text says a repair exists. What the repair is — how to modify the glued frame so it validates the axiom while keeping both countermodels intact — is not on the page.

Still open: telling which logics have it #

The glue explains the property wherever it applies and explains its loss for any logic whose axiom forbids the glued shape. What it does not provide is a test. Given an intermediate logic by its axioms, whether it has the disjunction property is not in general something one can read off the axioms, and a characterisation of the logics that have it is not known. The census shows why: closure under the plain glue is sufficient and not necessary, and a logic without it may still have some other construction that saves the property.

The companion question runs the other way — from the logics that lose the property toward their models. Gödel–Dummett logic loses it because its models are lines. Lines of truth values are also where the oldest result about these logics comes from: that no finite table of truth values, however long the line, has the constructive system as its logic. That is a statement about chains, and it is the natural next thing to draw.

The new stage that knows nothing #

The whole argument turns on one stage placed underneath, at which nothing is known. It is the model-theoretic image of a moment before either of two possible developments has begun — the state of knowledge compatible with both futures. A constructive proof of $A \vee B$ has to be valid at that moment. Since at that moment neither $A$ nor $B$ is established, the proof cannot rest on the disjunction being settled by the facts; it has to carry the decision itself.

Classical logic has no such moment in its models, which is why it can prove disjunctions it cannot resolve. Exhibiting a model settled whether a set of rules is consistent; exhibiting one extra stage settles whether a logic can keep its promises about “or”. Its one-stage models are already complete, and a proof valid in all of them can argue by cases about what the single stage decides. The constructive system’s models include every beginning, and a proof valid in all of those must decide before any of them has.