Thanks for pointing this out, Noam. Maybe I was over-hasty in using the expression "non-truth-functional". I'll take a look at Girard's paper, I think I have it kicking around somewhere.

PS: "uniquely determined by" here means "is a function of", so that ƒ(A # B) is a function of <ƒ(A), ƒ(B)>. (Which amounts to saying that IF ƒ(A1 # B1) ≠ ƒ(A2 # B2) THEN either ƒ(A1) ≠ ƒ(A2) or ƒ(B1) ≠ ƒ(B2).)

Hi Neel, By "truth-functional", I mean "can be furnished with truth tables". More strictly, logic L is truth-functional iff there exists a truth-value assignment ƒ from the atoms of L into set E, such that (1) ƒ sends A to a privileged value, call it e, iff A is provable, (2) ƒ(A # B) is uniquely determined by the values of ƒ(A) and ƒ(B), for every connective # in L. Does this conform with the usual meaning of "truth-functional"? Thanks, Luke

I was running out of space, and left the last sentence unclear: I mean that the problem is that there always tend to be "too many" separately provable formulae grouped together on a given line in the sequent proof, no matter how you try and break them up using the tensor rule. But that's the multiplicatives for you: they don't let you throw anything away, and so a multiplicative sequent can be unprovable because it's "choked" with separately provable formulae.

Thanks, Todd. This is what several hours tinkering around with attempted sequent proofs led me to expect, but the explanation in terms of proof nets makes it clearer why the existence of such formulae are unlikely. That "any proof of A [par] B cannot make any use of the proofs of A and B" is the key obstacle. The tactic that suggests itself is to have A or B throw some [tensor]s into the mix, so that the formulae in the context can be regrouped when the [tensor] rule is employed. But if A and B are to both be provable, there always seems to be "too many provables" in any rearrangement.