[Prev][Next][Index][Thread]

finite phase semantics


                  About finite phase semantics

                         Yves Lafont


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
noncommutative LL.

Here are the results for smaller fragments:

1. MELL (multiplicatives + exponentials) is not complete for the finite phase  
semantics.
2. MALL (multiplicatives + additives) is complete for the finite phase  
semantics.
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

    |- Delta
   ---------- (Gamma ~ Delta)
    |- Gamma

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