Monday, 20 June 2011

The Law of Permutation and Paracompleteness

The law of permutation (C) is the following conditional law: $\vdash (A \rightarrow (B \rightarrow C))$ $\rightarrow$ $(B \rightarrow (A \rightarrow C))$. In a sense (C) is characteristic of structural exchange, i.e., the sequent calculus rule that permits commutation of premises:

Hartry Field's paracomplete theory of truth rejects (C). I think this is a pretty remarkable and under-discussed aspect of his proposal. The reason the law has to go is that it is equivalent, under pretty minimal assumptions (see Anderson & Belnap 1975, 79), to the following law (A12):

$A \rightarrow ((A \rightarrow B) \rightarrow B)$

From A12, together with another law that Field's algebraic semantics validates, conjunctive syllogism (CS),

$((A \rightarrow B) \land (B \rightarrow C)) \rightarrow (A \rightarrow C)$

Field shows that we can derive the law of contraction (W):

$(A \rightarrow (A \rightarrow B)) \rightarrow (A \rightarrow B)$

This leads to disaster since most systems, including Field's, cannot have (W) on pain of the Curry Paradox. Field's diagnosis is that we have no other choice than to reject (A12), and thus the law of permutation (C) with it. The cost is high, but Field suggests that it would be worse to give up the sensible looking (CS). After all, (CS) simply looks like a law recording the transitivity of the conditional, a property we definitely want to preserve.

Nevertheless, I think that this line of reasoning is not entirely satisfactory. If we instead give up (CS), we might be able to maintain both (C) and the equivalence with A12. As far as intuitions go, I suppose that (C) is a pretty natural looking fellow too. Indeed, I'm not sure what would constitute a tie breaker between (CS) and (C). But that aside, there is another consideration in the favour of giving up (CS) rather than (C). (C) is the conditional law characteristic of structural constraction, i.e.

If we reject (LW) then it naturally follows that we give up (C) as well. More interestingly, if we give up (LW) then (CS) isn't normally derivable either. Notice that (CS) relies on it being possible to apply conjunction elimination ($\land$L) twice in order to derive the consequent. In sequent calculus this involves applying contraction to duplicate the antecedent, and then applying the conjunction rule twice (alternatively, having a conjunction rule with absorbed contraction, in which case full contraction is typically admissible). In natural deduction, we have to assume two copies of the antecedent, and subsequently use multiple discharge (the ND analogue of contraction) in a conditional proof application.

In other words, there is some proof theoretic reason to think that both (W) and (CS) are symptoms of the underlying presence of structural contraction. In contrast, (C) is attached to the structural rule of exchange. Whatever one may think intuitively about (CS), I think there is some reason to think that if we are already committed to rejecting (W), giving up (CS) as well is the move which is most in tune with the revisionary strategy.

Does that mean that we have a non-transitive conditional? No. It's just that expressing the transitivity with the extensional conjunction is unfortunate if one wants to reject the law of contraction as well. There are other, pure conditional laws that express transitivity in both Field's system and related systems:

Of course, that leaves us with an open question. Is there a logic without (CS) but with (C) in the vicinity of Field's logic, which is consistent? I think the answer to this is yes. This brings us roughly to the area of the contraction free relevant logic RW, and perhaps RW plus K.

(Cross-posted on www.hiddenabacus.com)

Update: Shawn Standefer made some very valuable comments. First, A10 and A11 above only hold in the rule form, not as axioms. Second, although I wasn't aware of this, it looks like (CS) isn't valid in the semantics has in the book Saving Truth From Paradox, although it does hold in semantics the of his earlier JPL paper.

1. wouldn't contraction violate [(A->B)->(~B->A)]?

2. Would C violate the rule of contraposition? Also, if a system can be paraconsistent and complete, wouldn't this be stronger than any system that is consistent and paracomplete?

3. Not sure I get the questions. What do you mean by C violating contraposition? If the question is whether giving up C leads to giving up contraction, the answer is no (for the systems I'm considering).

About the second question: Do you mean deductively stronger?

4. Also: CS plus transparent truth plus fusion (multiplicative/intensional conjunction) will go kaboom. (Proof is in RLR1, which I don't have handy.) I certainly wouldn't mind having fusion around; this gives another reason to avoid CS.

5. Didn't know that, Dave! Yes, definitely nice if multiplicative conjunction can be consistently added.

6. Just a side remark on LEx and reasons you may have to reject it; if you want to introduce a dynamic component in your system, such that the order in which the premises make their appearance matters, then this might count as a good reason to reject LEx. The trouble with the way Field goes around is that he rejects principles whenever they 'lead you to trouble' without independent motivation.

This is a reply to your "As far as intuitions go, I suppose that (C) is a pretty natural looking fellow too. Indeed, I'm not sure what would constitute a tie breaker between (CS) and (C)." Well, it will all depend on what you think you are up to with your logic. I don't think there is an absolute sense in which either (CS) or (C) is more/less plausible, it's going to be relative to what you want your logic to capture. One of the things that I like about linear logic is that it's very clear why they reject contraction, for example; it's just a different ball game, namely keeping track of your resources.

7. Ole,

Contraposition:
[(A->B)->(~B->~A)]
By not negating the new antecedent, how can the two rules co-exist?

And yes, deductively stronger. A system paraconsistent and complete can prove more true propositions true, and all true propositions can be proven with reductio ad absurdum.

8. Following up on what Dave said, there is a demonstration of how CS plus fusion results in triviality on p. 366-367 of Relevant Logics and their Rivals vol. 1.