Sequence encoding without induction (Q2888636)

Sequence encoding has become, since Gödel's proof of his incompleteness theorem, an indispensable tool in the study of arithmetical theories and related areas of mathematical logic. P.~Pudlák, during his work on interpretability, isolated a general concept of theories supporting encoding of sequences of their elements and called them sequential theories. In the present paper the sequentiality of the theory PA\(^{-}\) of discretely ordered commutative semirings with a least element (without the subtraction axiom) and therefore of all its simple extensions is proved. The theory PA\(^{-}\) is an induction-free theory and it is often used as an arithmetical base theory (like the theory Q). The main result can be adopted in a straightforward way to the theory of discretely ordered commutative rings.