Аннотация:Quantifier-free prepositional linear affine logic (i.e. linear logic with weakening) is decidable. Lafont and Scedrov proved that the multiplicative fragment of second-order linear logic is undecidable. In this paper we show that second order linear affine logic is undecidable as well. At the same time it turns out that even its multiplicative fragment is undecidable. Moreover, we obtain a whide class of undecidabile second order logics which lie between the Lambek calculus (LC) and linear affine logic. The proof is based on an encoding of two-counter Minsky machines in second order linear affine logic. The faithfulness of the encoding is proved by means of the phase semantics.
The research described in this publication was made possible in part by Grant No. NFQ300 from the International Science Foundation and by the Russian Foundation for Basic Researh (grant 96-01-01395).