Talk by Martin Emms
Embeddings and Undecidability for the Second Order Lambek Calculus
Embedding results for the 2nd Order Lambek Calculus are
presented. The calculus does not have `tuple of categories' or `unit
category' as primitive notions, nor does it allow the structural rules
of Permutation, Contraction or Weakening. However, other logics which
do these things are proven to be $^*$embeddable$^*$ in it. Of interest in
themselves, these embeddings results also allow us to prove simply the
oft conjectured undecidability of the 2nd Order Lambek Calculus.
Paul Dekker, November 2, 1995