|
Vestnik Moskovskogo Universiteta. Seriya 1. Matematika. Mekhanika, 2009, Number 2, Pages 62–65
(Mi vmumm863)
|
|
|
|
Short notes
Lambek calculus with one division and one primitive type permitting empty antecedents
S. L. Kuznetsov Lomonosov Moscow State University, Faculty of Mechanics and Mathematics
Abstract:
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.
Received: 28.04.2008
Citation:
S. L. Kuznetsov, “Lambek calculus with one division and one primitive type permitting empty antecedents”, Vestnik Moskov. Univ. Ser. 1. Mat. Mekh., 2009, no. 2, 62–65
Linking options:
https://www.mathnet.ru/eng/vmumm863 https://www.mathnet.ru/eng/vmumm/y2009/i2/p62
|
Statistics & downloads: |
Abstract page: | 83 | Full-text PDF : | 36 |
|