Geodesic
Lambek calculus with one division and one primitive type permitting empty antecedents
Vestnik Moskovskogo universiteta. Matematika, mehanika, no. 2 (2009), pp. 62-65

Voir la notice de l'article provenant de 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},
     publisher = {mathdoc},
     number = {2},
     year = {2009},
     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
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/VMUMM_2009_2_a12/
LA  - ru
ID  - VMUMM_2009_2_a12
ER  - 
%0 Journal Article
%A S. L. Kuznetsov
%T Lambek calculus with one division and one primitive type permitting empty antecedents
%J Vestnik Moskovskogo universiteta. Matematika, mehanika
%D 2009
%P 62-65
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/VMUMM_2009_2_a12/
%G ru
%F VMUMM_2009_2_a12
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/