Импликативные логики, ламбековские системы и экспоненциальные мультикатегории.

Abstract

In the paper Lambek's type implicative deductive systems and exponential categories for them are considered and some metamathematical theorems are proved (deduction theorem, functional completeness). Then we formulate both sequential implicative deductive systems and exponential multicategories for which the cut elimination theorem is proved. Finally sequential deductive implicative metasystems and dual deductive systems and categories are discussed.