Gentzen systems and decision procedures for relevant logics

Abstract

This dissertation is primarily a proof theoretic investigation of the positive fragments and boolean extensions of two of the principal relevant logics T and R, with and without contraction, and of the corresponding positive semilattice relevant logics. In addition to motivational and syntactic preliminaries, Chapter 1 contains some new semantic results which are useful in the later chapters. In Chapter 2 we develop subscripted Gentzen systems for four positive semilattice logics. Appropriate Cut Theorems are proved, and one system is shown to be equivalent to uR+ Decision procedures are then given for the two contractionless systems. In Chapter 3 Gentzen systems are given for TW+, T+, RW+ and R+, Cut Theorems and equivalences are proved, and TW+ and RW+ are shown to be decidable. The sequent calculi that are used are multiply structured as required for relevant logics. Chapter 4 begins by collecting decision procedures for fragments of TW+ and RW+. We then discuss and make some progress toward solving some open problems, viz., the decision questions for EW+, TW and RW, and the question of equivalence between RW+ and its semilattice counterpart uRW+.