Abstract

van Benthem [1] introduces a variant of Lambek Syntactic Calculus , proposed by Lambek [6], we call the variant Lambek-van Benthem Calculus . As proved by van Benthem, LBC is complete with respect to a semantics of λ-terms. In this note we indicate other relevant properties of LBC , just supporting some expectations of van Benthem. Given a countable set P r, of primitive types, the set T p, of types, is the smallest one such that: T p contains P r, if x, y are in T p then is in T p. The variables x, y, z will range over types. Expressions X → x are to be called reduction formulas