Lambek calculus with one division and one primitive type permitting empty antecedents
Vestnik Moskovskogo universiteta. Matematika, mehanika, no. 2 (2009), pp. 62-65
Cet article a éte moissonné depuis la source Math-Net.Ru
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)$.
@article{VMUMM_2009_2_a12,
author = {S. L. Kuznetsov},
title = {Lambek calculus with one division and one primitive type permitting empty antecedents},
journal = {Vestnik Moskovskogo universiteta. Matematika, mehanika},
pages = {62--65},
year = {2009},
number = {2},
language = {ru},
url = {http://geodesic.mathdoc.fr/item/VMUMM_2009_2_a12/}
}
TY - JOUR AU - S. L. Kuznetsov TI - Lambek calculus with one division and one primitive type permitting empty antecedents JO - Vestnik Moskovskogo universiteta. Matematika, mehanika PY - 2009 SP - 62 EP - 65 IS - 2 UR - http://geodesic.mathdoc.fr/item/VMUMM_2009_2_a12/ LA - ru ID - VMUMM_2009_2_a12 ER -
S. L. Kuznetsov. Lambek calculus with one division and one primitive type permitting empty antecedents. Vestnik Moskovskogo universiteta. Matematika, mehanika, no. 2 (2009), pp. 62-65. http://geodesic.mathdoc.fr/item/VMUMM_2009_2_a12/