|
Abstract:
|
In this thesis cut elimination and decidability for several propositional substructural logics are studied. The thesis consists of nine chapters. Chapters 2-6 make the first part of the thesis. In that part sequent systems for substrictural logics are formulated. In Chapters 3 and 4 for each of these systems an algebraic structure is given and completeness and consistency are proved. In Chapters 5 and 6 cut elimination and decidability for these systems are studied. It is well known that sequent system of classical Lambek logic, the system SL is decidable and that cut is not an admissible rule in CL. Another sequent system for classical Lambek logic, the system CL* is formulated, and the elimination of cut in CL* is proved. The system CL* does not posses the subformula property, so decidability for classical Lambek logic is not the direct consequence of the cut-elimination procedure in CL*. However, on the basis of the cut elimination procedure in CL*, a procedure for deciding of whether a sequent is provable in CL* or not is given (i. e., a new (pure syntactic) proof of decidability for classical Lambek logic is given). The same result is shown for classical Lambek logic with weakening. In the second part of the thesis (chapters 7-9), by using that proof, an algorithm (based on the tableau method) is formulated for deciding whether or not a formula is the theorem in any of considered substructural logics. |