[Prev][Next][Index][Thread]
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.