Simulating Computations in Second Order Non-Commutative Linear Logic (Preliminary Report)
Max Kanovich · Electronic Notes in Theoretical Computer Science · 1996
Synopsis Lincoln, Scedrov and Shankar proved undecidability of intuitionistic second order multiplicative commutative linear logic by embedding LJ2 into this logic. Emms did the same for intuitionistic second order non-commutative linear logic. Recently, Lafont and Scedrov demonstrated undecidability of classical second order multiplicative commutative linear logic. As for classical second order non-commutative linear logic, its decidability problem remained open. Here we present a direct and natural encoding of arbitrary machine computations in minimal fragments of the second order non-commutative linear logic (for instance, in the product-free Lambek syntactic calculus enriched by only one second order quantifier ∀), and prove the correctness and faithfulness of this encoding with respect to any second order system up to the full classical second order cyclic linear logic. It is thereby proved that any reasonable versions of the second order non-commutative linear logic are undecidable.