Cut Elimination and Contraction
Working with the consistency of contraction free logics with a naive truth predicate (see earlier post), I've been looking at a paper by Uwe Petersen (2000), 'Logic Without Contraction as Based on Inclusion and Unrestricted Contraction'. The paper proves the consistency of a set theory over BCK (see Ono & Komori 1985 for details of the system) with unrestricted comprehension. (As was already proved earlier in Grishin (1982) and White (1987), set theory with unrestricted comprehension and the axiom of extensionality, however, is inconsistent.) The hope is that such a consistency result using proof theoretic techniques can be carried over to a formal theory of (naive) truth. For a typed truth predicate, we already Volker Halbach (1999) which gives a cut elimination theorem to show consistency for a classical theory over PA (details can also be found in his new book).
The critical aspect of making cut elimination work in a system with naive truth is that there is, unlike in Halbach's system of typed truth, no guarantee that the relevant reduction steps will decrease the complexity of the cut formula. This is simply because with naive truth, the T-right rule can be applied to a formula of any complexity, including, say, the Liar sentence L. (For a discussion of this point, see Kremer 1988.) However, I came across the following promising observation by Petersen:
Petersen's observation is pretty neat, but I'm still not sure how general it is. Contraction is tricky, because even if the system has no explicit contraction rule, it might have an admissible contraction rule (as in the G3c system of Troelstra & Schwichtenberg). I'll have to defer to the experts here: Where should I look for a systematic development of this point? Is this observation common in the substructural literature?
(Cross-posted on The Hidden Abacus.)
The critical aspect of making cut elimination work in a system with naive truth is that there is, unlike in Halbach's system of typed truth, no guarantee that the relevant reduction steps will decrease the complexity of the cut formula. This is simply because with naive truth, the T-right rule can be applied to a formula of any complexity, including, say, the Liar sentence L. (For a discussion of this point, see Kremer 1988.) However, I came across the following promising observation by Petersen:
This is why the strategy employed in cut elimination of shifting cuts 'upwards' cannot rely on a decrease of the length of the cut formula. There is, however, no need for a decrease of the length of the cut formula, if contraction is not available; an induction on the length of the number of logical inferences is sufficient. (Petersen 2000: 370)In Petersen's BCK system, the upshot is that the cut elimination theorem is proved with no reference to the complexity of cut formulae. It is sufficient that pushing cuts upwards will decrease the length of the derivation, even if the cut formula increases in complexity. If contraction is around, this does not work. The reason, I think, is something like this: If the cut formula A on the succedent side is the result of an application of contraction, pushing the cut will involve cutting on two copies of A, and thus increasing the length of derivation by including the corresponding subderivation of A on the antecedent side twice.
[I]n the absence of contraction, normalization and cut elimination can be proved without a recourse to the length of the formula in question (maximum or cut formula). It is this that makes logic without contraction so safe against all antinomies arising from abstraction. (ibid. 374)
Petersen's observation is pretty neat, but I'm still not sure how general it is. Contraction is tricky, because even if the system has no explicit contraction rule, it might have an admissible contraction rule (as in the G3c system of Troelstra & Schwichtenberg). I'll have to defer to the experts here: Where should I look for a systematic development of this point? Is this observation common in the substructural literature?
(Cross-posted on The Hidden Abacus.)
I'm probably missing something, since I don't know the background, but just to get things rolling... If the contraction rule is only admissible (not explicit), then the proof can be rewritten without contraction. So you can forget about all the instances of contraction in proving cut elimination. An example of this approach is Negri & Plato's proof of cut admissibility for G3ip. Indeed, most (all?) of the proofs of cut admissibility in Negri & Plato involve induction on both height of the cut and weight (e.g. complexity) of the cut formula. Is this the kind of thing you have in mind, following Petersen?
ReplyDelete