A. P. Kopylov.
The undecidability of second order linear affine logic.
Mathematical Logic and Foundations Series, ML-1995-10, Institute for Logic, Language and Computation, Amsterdam, November 1995
Abstract.
The quantifier-free propositional linear affine logic (i.e. linear logic with the weakening) is
decidable [Kopylov]. Recently, Lafont and Scedrov proved that multiplicative fragment of
second-order linear logic is undecidable. In this paper we show that the second order
linear affine logic is undecidable too. At the same time it turns out that even its multiplicative fragment is undecidable.
Moreover, we obtain the whole class of undecidability second order logics which lie between Lambek calculus (LC) and linear affine logic.
The proof is based on an encoding two-counter Minsky machines in second order linear affine logic. The faithfulness of the encoding
is proved by means of the phase semantic.