Search

This thesis deals with the algorithmic undecidability (unsolvability) of provability in some non-classical logics. In fact, there are two natural variants of this problem. Fix a logic, we can study its set of theorems or its consequence relation, which is a more general problem. It is well-known that both these problems can be undecidable already for propositional logics and we provide further examples of such logics in this thesis. In particular, we study propositional substructural logics which are obtained from the sequent calculus LJ for intuitionistic logic by dropping structural rules. Our main results are the following. First, (finite) consequence relations in some basic non-associative substructural logics are shown to be undecidable. Second, we prove that a basic associative substructural logic with the contraction rule, which is notorious for being hard to handle, has an undecidable set of theorems. Since the studied logics have natural algebraic semantics, we also obtain corresponding algebraic results which are interesting in their own right.