Kripke, Belnap, Urquhart and relevant decidability & complexity “Das ist nicht Mathematik. Das ist Theologie.”

Abstract

The first philosophically motivated sentential logics to be proved undecidable were relevant logics like R and E. But we deal here with important decidable fragments thereof, like R⟶. Their decidability rests on S. Kripke’s gentzenizations, together with his central combinatorial lemma. Kripke’s lemma has a long history and was reinvented several times. It turns out equivalent to and a consequence of Dickson’s lemma in number theory, with antecedents in Hilbert’s basis theorem. This lemma has been used in several forms and in various fields. For example, Dickson’s lemma guarantees termination of Buchberger’s algorithm that computes the Gröbner bases of polynomial ideals. In logic, Kripke’s lemma is used in decision proofs of some substructural logics with contraction. Our preferred form here of Dickson-Kripke is the Infinite Division Principle (IDP). We present our proof of IDP and its use in proving the finite model property for R⟶.