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.)

  • 1
    $\begingroup$ 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? $\endgroup$ – Neel Krishnaswami Oct 8 '10 at 8:27
  • $\begingroup$ 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 $\endgroup$ – Z.L. Fraser Oct 8 '10 at 18:09
  • $\begingroup$ 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).) $\endgroup$ – Z.L. Fraser Oct 8 '10 at 18:13
  • $\begingroup$ 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. $\endgroup$ – Noam Zeilberger Oct 9 '10 at 8:30
  • $\begingroup$ 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. $\endgroup$ – Z.L. Fraser Oct 9 '10 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.

  • $\begingroup$ 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. $\endgroup$ – Z.L. Fraser Oct 8 '10 at 18:01
  • $\begingroup$ 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. $\endgroup$ – Z.L. Fraser Oct 8 '10 at 18:04

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.

  • $\begingroup$ That's really nice, Robin; wish I had seen that! $\endgroup$ – Todd Trimble Apr 1 '15 at 16:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.