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.

- Full paper (.ps file) / 10 pages