consequently.org/writing/extendingj

Interesting idea, and a beautifully written paper. (It would be nice if mathematicians could learn to write so well!)

Just one small remark, and apologies if this is too obvious. You briefly wonder whether subtraction has a place in topos theory: there is one reasonable sense in which the answer is clearly “no”.

As far as propositional logic goes there is no real need for a subobject classifier, so we can make do with a cartesian closed category that has finite coproducts. For such a category to model negation its opposite would also have to be cartesian closed, i.e. for every object X the functor (X + -) requires a left adjoint. So now the coproduct (taken with a fixed object) is a right adjoint, which means that it preserves limits. In particular it preserves the terminal object, so 1+1 is isomorphic to 1.

Since 1 is terminal it has a unique endomorphism, thus the two injection arrows i1: 1 -> 1+1 and i2: 1 -> 1+1 coincide. Now suppose we have two “different” proofs of some proposition, so we have an object X with two arrows f: 1->X and g: 1 -> X. Take the copairing [f,g]: 1+1 -> X; then of course f=[f,g].i1 and g = [f,g].i2. But i1=i2, so in fact f=g=[f,g].

So such a category must have at most one “proof” of each formula, i.e. at most one arrow in each homset, i.e. be a preorder. So the categorical interpretation is essentially just interpretation in a lattice.

This fact is reflected in the proof theory: cut elimination is non-deterministic in such a way that any two proofs of the same sequent may be identified. The version of sequent calculus you use - with multiple formulae on the right as well as the left - already has this property; but presumably you chose this version so that your new connective could be accommodated. (If one restricts to sequents with a single formula on the right then the extreme nondeterminism disappears; but you can’t define subtraction!)

Posted by: Robin at August 24, 2004 06:11 AM

Thanks for the kind words.

I am aware of these nice collapse results—-at least, I’m aware of them now. I wasn’t when that paper was written. There’s some nice work by Pym and Führmann that shows that we can resist this kind of collapse even in classical logic if we look for models in which proofs are given a preorder by cut-elimination (or normalisation), not an equivalence class. It’s very interesting material, and there’s more to be said about all of this stuff…

Posted by: Greg Restall at August 27, 2004 09:30 AM

I guess you know more than I do about this. It seems (to this non-philosopher) that the real question here is essentially a philosophical one. Is there a meaningful sense in which two classical proofs of the same sequent can be “essentially different”?

On the off-chance that you haven’t seen it, I’d also recommend Hyland’s musings on Proof theory in the abstract (Annals of Pure and Applied Logic Volume 114, Issues 1-3), which discusses the problem.

Posted by: Robin at August 31, 2004 07:52 AM

I agree that the important point is the philosophical one. I think that the different kinds of formal relationships of reduction between proofs are at best raw materials to be considered as options for proof-identity.

I’ve heard about the Hyland paper, but I haven’t got it. Melbourne (alas) doesn’t subscribe to the Annals (even electronically). Does anyone care to send me an offprint if they have one handy?

Posted by: Greg Restall at August 31, 2004 02:09 PM