Reverse mathematics, constructivism and justification

May 22, 2012

In a recent talk I argued that the computational reverse mathematics suggested by Richard Shore in his 2010 paper, ‘Reverse mathematics: the playground of logic’, was not suitable for the job of analysing which theorems of ordinary mathematics are assertible by proponents of foundational systems such as predicativism or finitistic reductionism. This is because the relation of computable entailment employed by Shore doesn’t preserve the justificatory structure of those programmes. For example, there are statements that are computably entailed by ${\mathsf{\text{WKL}}}_0$, a finitistically reducible system, which are not themselves finitistically reducible.

There is an obvious way in which this problem is shared by classical reverse mathematics, and that is its relationship to constructivism. Constructivists reject unrestricted use of the law of excluded middle, but reverse mathematics is developed within classical logic and as such proofs relying on the law of the excluded middle are commonplace. Consequently there will be reverse mathematical theorems that cannot be countenanced by a constructivist since they have no constructive proof.

Any attempt to convince a committed constructivist that certain parts of mathematics are beyond the reach of her axioms must employ principles that are themselves constructively acceptable. After all, the point here is to analyse foundational programmes—including varieties of constructivism—and not to rule them out before we even begin. The problem is the entailment relation: it’s plain that we can re-run the argument given in §3 of my talk, swapping out computable entailment for classical entailment, and classical proof for constructive proof.

Preserving justification is a key property for any entailment relation: if we are justified in accepting the antecedent, then we are also justified in accepting the consequent. But classical entailment does not, by constructivist standards, preserve justification. Considering just one case, a proof of $\phi \vee \psi$ does not in all cases constitute a proof of $\phi$ or a proof of $\psi$. The constructivist is therefore entitled, by her own lights, to ignore classical results demonstrating the limits of her axiom system.

This points to a tension within reverse mathematics. On the one hand there is an obvious and understandable desire to prove all of the results one is able to, and explore precisely which theorems of ordinary mathematics (ordinary mathematics itself being strongly rooted in classical logic) can be shown to be equivalent to one of the major subsystems of second order arithmetic. On the other, as one bakes stronger assumptions into one’s analytical framework one becomes unable to faithfully analyse weaker foundational systems such as constructivism.