How much propositional logic suffices for Rosser’s undecidability theorem?

Abstrakt

Rosser [3] famously established that Peano Arithmetic was essentially undecidable against the background of classical ϐirst-order logic, that no consistent extension of that theory against that logic was decidable, and this result was extended to Robinson Arithmetic in [4]. We extend the result further by considering not only a weaker arithmetic theory, but a weaker propositional logic governing the behaviour of logical connectives. Following Hájek’s paper [2] and his later unpublished work on fuzzy arithmetics, we prove essential undecidability for a version of Robinson arithmetic, with predicates (rather than functions) to interpret the arithmetic operations, against the background of a propositional logic with very few logical assumptions. Our logic is much weaker thank the one used by Hájek; it is a variant of Brady’s BBQ [1] with weakening, in a language including falsum (in terms of which negation is deϐined), and a crisp (i.e., two-valued) identity predicate. The key logical fact is that, in this system, one can regain enough of the logical inferential machinery to establish the necessary arithmetic facts, the key fact being that all the theory-speciϐic predicates can be shown to be crisp when applied to numerals. Therefore, our result suggests that essential undecidability is a property largely dependent on the arithmetic theory, rather than the background propositional logic.