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

Question

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. 1 ⅋ 1 is easily shown to be unprovable (which by itself tells us a lot about the peculiarities of linear logic---1 ⅋ 1 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 ϕ(1 ⅋ 1) = ϕ(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 ϕ(1 ⅋ 1) ≠ ϕ(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.)

Answer 1

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.

Answer 2

I realise I am several years late, but there is a lovely simple principle that answers your question definitively, and I can’t resist explaining it. I’ll assume we’re working in multiplicative linear logic, with units.

Consider a sequent $\Gamma$. Suppose $\Gamma$ has $m$ occurrences of ⅋ – counting commas as occurrences of ⅋ – and that it has $n$ negative occurrences of atoms (e.g. $p^\perp$ or $\perp$).

Lemma. If $\Gamma$ is provable, then $m=n$.

Proof. Suppose $\Gamma$ is provable, thus has a proof net. Ignoring axiom and $\perp$ links, each ⅋-switching of the proof net has $m+1$ connected components. To make it connected and acyclic, there must be $m$ axiom and $\bot$ links. But the number of axiom and $\bot$ links is just $n$, hence $m=n$ as required. ■

So at most two of $\vdash A$, $\vdash B$ and $\vdash A⅋B$ can be provable.

PS. Maybe it’s worth adding that you don’t need proof nets to prove this lemma. It can also be done as an easy induction over proofs.