Equational fragments of systems for arithmetic

We investigate the equational fragments of formal systems for arithmetic by means of the equational theory of f-rings and of their positive cones, starting from the observation that a model of arithmetic is the positive cone of a discretely ordered ring. A consequence of the discreteness of the order is the presence of a discriminator, which allows us to derive many properties of the models of our equational theories. For example, the spectral topology of discrete f-rings is a Stone topology. We also characterize the equational fragment of lopen, and we obtain an equational version of Godel's First Incompleteness Theorem. Finally, we prove that the lattice of subvarieties of the variety of discrete f-rings is uncountable, and that the lattice of filters of the countably generated distributive free lattice can be embedded into it.