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:
- ϕ(A) = ϕ(B) ==> ϕ(~A) = ϕ(~B)
- ϕ(A1) = ϕ(A2) AND ϕ(B1) = ϕ(B2) ==> ϕ(A1 ⊗ B1) = ϕ(A2 ⊗ B2)
- ϕ(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.)