## Can the Multiplicative Fragment of Linear Logic be shown to be non-truth-functional?

The short form of my question is: Can we find two formulae (in the multiplicative fragment of linear logic (MLL), that is, without additives or exponentials) A and B such that (1st) A is provable and B is provable, (2nd) A ⅋ B (A par B) is provable?

The context of the question is this: If we can find two such formulae, we can easily show that the multiplicative fragment of linear logic is not truth functional.

By truth-functionality, we should have:

1. ϕ(A) = ϕ(B) ==> ϕ(~A) = ϕ(~B)
2. ϕ(A1) = ϕ(A2) AND ϕ(B1) = ϕ(B2) ==> ϕ(A1 ⊗ B1) = ϕ(A2 ⊗ B2)
3. ϕ(A1) = ϕ(A2) AND ϕ(B1) = ϕ(B2) ==> ϕ(A1 ⅋ B1) = ϕ(A2 ⅋ B2)

Let us assume, for reductio, that there exists a function ϕ, from the set of linear formulae to the elements of an arbitrary set E, that satisfies (1)-(3), and which is such that ϕ(A) = e if and only if A is provable in linear logic.

(Remark: We know that it is possible, in fact, to find a truth-functional value-assignment that gives every provable formula the same value---i.e. that assigns "true" to a formula whenever it is provable. This won't concern us here. What we want to show is that any such function always assigns truth to too many formulae, that "truth", on any assignment, may be construed as a necessary condition for provability, but by no means a sufficient condition for provability.)

What we want to do now is find formulae {A1, A2, B1, B2} which are each, on their own, provable, and so which will be such that:

ϕ(A1) = ϕ(A2) = e ϕ(B1) = ϕ(B2) = e

But which are such that (A1 ⅋ B1) is not provable, while (A2 ⅋ B2) is provable. If we find such formulae, then we will have shown that our assumption leads to a contradiction: by (I), ϕ(A1 ⅋ B1) ≠ ϕ(A2 ⅋ B2), but by (II), ϕ(A1 ⅋ B1) = ϕ(A2 ⅋ B2).

This is where I hit the wall. Finding multiplicative A1, B1 is simple enough: Let them each be the constant 1. 11 is easily shown to be unprovable (which by itself tells us a lot about the peculiarities of linear logic---11 looks like the linear counterpart of True v True). If we allow ourselves to dip into the additives, we can let A2 = 1 and let B2 = (1⊕⊥), and the resulting A2 ⅋ B2 will be provable. This is enough to show that LL, as a whole, is not truth-functional, because it leads to the destructive dilemma:

Either ϕ(11) = ϕ(1 ⅋ (1 ⊕ ⊥)) = e, in which case ϕ(x) = e is not equivalent to “x is provable”; since ϕ and e are arbitrary, this shows that no truth-functional value assignment captures linear provability.

Or else ϕ(11) ≠ ϕ(1 ⅋ (1 ⊕ ⊥)), which contradicts truth-functionality requirement (3). To the extent that it violates (3), ϕ is not truth-functional.

This is all well and good, but can we get a similar result for the multiplicative fragment, that is, can we find two multiplicative, MLL-provable formulae whose multiplicative disjunction is also provable?

(PS: I'm using Girard's notation, not Troelstra's, so 1 and ⊥ should be read as the multiplicative constants, the neutrals for tensor and par, respectively.)

-
I'm not sure what you mean by "truth-functional". Girard's phase semantics gives a sound and complete model-theoretic interpretation of the connectives of classical linear lgoic, but perhaps you want something more stringent than that? – Neel Krishnaswami Oct 8 2010 at 8:27
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 – Z.L. Fraser Oct 8 2010 at 18:09
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).) – Z.L. Fraser Oct 8 2010 at 18:13
then phase semantics satisfies your requirements for being truth-functional, except that not every provable formula is necessarily assigned the same value. See Theorem 2 of Girard's "Linear Logic: Its Syntax and Semantics": an arbitrary linear logic formula is provable iff its interpretation in any phase space $(M,\bot)$ (where $M$ is a commutative monoid, $\bot$ an arbitrary subset of $M$) contains the neutral element. – Noam Zeilberger Oct 9 2010 at 8:30
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. – Z.L. Fraser Oct 9 2010 at 22:40

I don't have a complete proof, but I'm rather skeptical of the existence of such formulas. Certainly in the unit-free fragment of MLL it's hopeless, by applying a proof net criterion. For example, using the Danos-Regnier criterion for validity of proof nets, if you have a sequent $\to A \wp B$ (which is equivalent to $\to A, B$; I'm using $\wp$ to denote par) and if $A$ and $B$ are provable, then for any way of setting the $\wp$-switches on subformulas, the resulting graphs for $A$ and $B$ are acyclic and connected, so the graph for $\to A, B$ would be disconnected, and hence the sequent cannot be provable.
Generally speaking, the presence of units (or neutrals as you call them) make provability of sequents much harder to decide. About all I can say at the moment is that if you have proofs of $A$ and $B$, then any proof of $A \wp B$ cannot make any use of the proofs of $A$ and $B$ whatsoever, for essentially the same reason as given above.