Lambek calculus with one division and one primitive type admitting empty antecedents / S. L. Kuznetsov. //Vestnik Moskovskogo Universiteta. Seriya 1. Matematika. Mekhanika. 2009. № 2. P. 62-65 Moscow Univ. Math. Bulletin. Vol. 64, N 2, 2009. P. 76-79].

The following assertion is proved: a deduction rule given by a scheme is admissible in the Lambek calculus with one division \mathrm{L}^*(\backslash) permitting empty antecedents if and only if it is admissible in the fragment of \mathrm{L}^*(\backslash) with one primitive type \mathrm{L}^*(\backslash; p_1). To do that, a type substitution is used which reduces the derivability in \mathrm{L}^*(\backslash) to the derivability in \mathrm{L}^*(\backslash;p_1).

Key words: Lambek calculus, admissible rules, proof nets.

№ 2/2009