Decision Problems For Second Order Linear Logic

Decision Problems For Second Order Linear Logic
Yves Lafont

Recently, Lincoln, Scedrov, and Shankar proved that IMLL2 and MLL12 are  
undecidable by simulating the rules of contraction and weakening using second  
order propositional quantifiers and the multiplicatives (see the last message  
of the linear list).

Here is a new result:

Theorem: MALL2 is undecidable.

This is proved by a direct encoding of Minsky machines. We do not use the  
contraction axiom C = forall X. X -o X*X, but a "soft" version:

                    C' = forall X. X&1 -o X*X.

Our encoding is essentially Kanovich's one with A&1 in place of !A. Of course,  
the main difficulty is to show that C' does not produce fake computations. For  
this, we introduce a specific phase model.

Two remarks:

- The main novelty in the proof is the use of phase semantics.

- Additives are used in an essential way: The decidability of MLL2 is still an  
open question.