LEM and Contraction

Hartry Field’s Saving Truth from Paradox suggests a paracomplete approach to the Liar paradox, that is, we give up LEM. Then we deal with the Curry paradox independently by introducing a conditional for which conditional proof doesn’t hold. That’s the short story.

Viewing logical choices primarily from a proof theoretic perspective, the idea of giving up LEM might strike you as unsatisfactory. LEM is, after all, a principle that is ordinarily proved, say, in natural deduction, by inference rules for negation and disjunction that are themselves interesting (just consider the fact that both proof by cases and reductio in different variants are rejected in other approaches to paradoxes). Sure, you can have LEM as an axiom (i.e. null-premise rule) if you want, but it’s not standard. Field himself admits that one might wonder why rejecting LEM is at all helpful when the Liar is provable with only intuitionistic resources. His reply won’t satisfy the intuitionist: Field holds that the best justification of the intuitionistic reductio rule is precisely LEM.

What’s the idea? If you already accept LEM and proof by disjunction (\veeE), you have the following derivation:

Given that the rightmost subderivation is trivial, we now have a version of intuitionistic reductio from the leftmost subderivation. Analogously, the same story can be told for a classical reductio rule.

Yet, if you – intuitionist or not – think that reductio rules might be justified without LEM, then this won’t do. Instead, you might consider alternative routes to reject LEM. For example, keep some form of classical reductio but reject proof by cases. Are there other options? In standard natural deduction derivations of LEM you also need multiple discharge, the policy that multiple copies of a formula may be discharged simultaneously. In other words, a classical reductio rule may discharge two copies of \neg A with one application of the rule. This global feature of natural deduction is what normally allows you to derive e.g. A \rightarrow (A \rightarrow B) \vdash A\rightarrow B, using multiple discharge in conditional proof. It is also a candidate culprit in the Curry derivation, one well-known but not often pursued.

So, giving up multiple discharge is a possible route for blocking LEM as well. It corresponds roughly to giving up structural contraction in a sequent calculus setting. (Although the details depends on whether one can give a correspondence result where contraction-free proofs are mapped to proofs without multiple discharge and vice versa. See Negri and von Plato for more on this.)

More interestingly, though, LEM itself is a kind of contraction principle. (In particular, you can prove A \rightarrow (A \rightarrow B) \vdash A\rightarrow B, even without multiple discharge.) My supervisor, Stephen Read, used to tell me this, but I never had the details clear in mind. Reading Greg Restall’s On Logics Without Contraction, I now see that this connection can be given more formal characterisation. In particular, in a system with a De Morgan Negation but no contraction, you can add primitive LEM plus \veeE to prove a restricted contraction principle, namely:

That is, contraction is available in the presence of a negated conclusion. Of course, from the above observation about LEM and proof by cases, we already know that we have restricted contraction whenever the conclusion is \neg A (leftmost below). Following Restall let’s call this rule ExMid.

In addition, we need another negation principle (rightmost), which is similar to the rule for simple negation found in Restall (both classically and intuitionistically valid, of course). We can then given the following derivation:

What is the significance of this? First, it shows that, in certain proof theoretic contexts, rejecting LEM is a way of giving up some measure of contraction. (Obviously, it won’t always make a difference since you might have contraction via other – say, explicit – means.) Second, it shows that – as anticipated by Slaney and others – if you give up contraction to avoid paradox, adding LEM to the system is risky. I’m not sure where this leaves the dialectic between Field and the champion of rejecting contraction: The former might say, look, LEM needs to go; the latter, well yes, but LEM is just more contraction in disguise.

What if you like rejecting contraction, but want to keep LEM? One way might be to tinker with disjunction elimination to avoid principles like ExMid. Other suggestions?

Update: I need to mention that Elia Zardini has a paper on contraction-free approaches to paradoxes. Hopefully, I’ll have the chance to comment on his theory when it’s available. Conversations with Elia about contraction and paradox have been crucial in convincing me that this is a tenable and fruitful approach.