finite phase semantics
About finite phase semantics
Note: I will only discuss the propositional case.
Remember that an infinite phase model is used in the proof of the
completeness of LL for the phase semantics [Gir87]. What about finite phase
models? Clearly, the finite phase semantics cannot be complete for LL,
since it would give a decision algorithm for LL, whereas LL is known to be
undecidable [LMSS92]. Of course, the same argument applies to
Here are the results for smaller fragments:
1. MELL (multiplicatives + exponentials) is not complete for the finite phase
2. MALL (multiplicatives + additives) is complete for the finite phase
3. Noncommutative MALL (cyclic version, see [Abr91]) is complete for the
noncommutative version of the finite phase semantics.
This is not too unexpected, since the exponentials are supposed to express
infinity in the logic!
1. The formula A = !a * !(a * b) * !(a * b -o 1) -o b is not provable, but
it holds in any finite phase model. The point is that, in a finite model M,
there are p < q such that b^p and b^q have the same interpretation, so that
the formula b^p -o b^q (which entails A) holds in M.
2. The proof uses a system MALL(A,k) where k is big enough (more than the
number of occurrences of atoms and units in A). The formulas in MALL(A,k) are
the subformulas of A and their negations. The rules are those of MALL,
including cut, plus an extra structural rule
---------- (Gamma ~ Delta)
where Gamma ~ Delta means that for any formula B, the multiplicity of B in
Gamma is the same as the multiplicity of B in Delta, or both are >= k. Note
that this congruence defines a finite quotient. The point is that if A is
provable in MALL(A,k), then it is provable in MALL. Yet MALL(A,k) does not
satisfy the cut-elimination property!
3. The argument is similar. The congruence is defined by Gamma ~ Delta if
Gamma and Delta have the same subsequences of length =< k. Again, it
defines a finite quotient.
A paper is under preparation.
[Abr91] V. M. Abrusci, Phase semantics and sequent calculus for pure
noncommutative classical linear propositional logic, JSL 56, 1403-1451
[Gir87] J.-Y. Girard, Linear Logic, TCS 50, 1-102
[LMSS92] P. Lincoln, J. Mitchell, A. Scedrov, & N. Shankar, Decision problems
for propositional linear logic, APAL 56, 239-311