Logiki podstrukturalne oparte na dystrybutywnych kratach z rezyduacjami

Abstract

Praca traktuje o logikach podstrukturalnych, które są oparte na dystrybutywnych kratach z rezyduacjami. W pierwszej kolejności autor skupia się na podstawowym rachunku logicznym, którego modelem algebraicznym jest klasa dystrybutywnych krat z rezyduacjami, tzn. dystrybutywnym pełnym rachunku Lambeka. Dla rachunku tego, autor dowodzi własności skończonego modelu, a stąd rozstrzygalności tego rachunku. Oba te problemy były problemami długo otwartymi w literaturze. W dowodzie tym autor rozszerzył, szeroko stosowaną w systemach niedystrybutywnych, metodę nuklearnego domknięcia monoidu i quasi-zanurzenia na systemy dystrybutywne. Następnie autor wprowadza system dystrybutywnego pełnego rachunku Lambeka z cykliczną inwolucją i także dowodzi jego rozstrzygalności. Ponadto dla wersji niedystrybutywnej podaje pierwszy rozstrzygalny system z sekwentami intuicjonistycznymi. Na końcu, autor skupia się na infinitystycznych logikach akcji (tzn. logikach których modelami algebraicznymi są *-ciągłe kraty akcji) oraz rozszerza metodę nuklearnego domknięcia monoidu i quasi-zanurzenia zarówno na wersję dystrybutywną jak i niedystrybutywną. Dla wersji niedystrybutywnej ponadto dowodzi własności skończonego modelu.

The dissertation treats about substructural logics which are based on distributed residuated lattices. First, the author focuses on the basic logical calculus that algebraic model is the class of distributed residuated lattices, i.e. distributive full Lambek calculus. For this calculus, the author proves the finite model property, where from the decidability of this calculus follows. Both these problems were long-open problems in the literature. In this proof, the author extended the method of nuclei and quasi-embedding to distributive systems – so far, this method was known and widely used only for nondistributive systems. Next, the author introduces the system of cyclic involutive distributive full Lambek calculus and he proves its decidability as well. Moreover, for the nondistributive version, he gives the first decidable system with intuitionistic sequents. At the end, the author focuses on infinitary action logics (i.e. logics that algebraic models are *-continuous action lattices) and he extends the method of nuclei and quasi-embedding both to the distributive and to the nondistributive versions. In addition, for the nondistributive version, he proves the finite model property.