# Why are local rings a coherent theory?

It is well known that one way to describe the theory of local rings in first order logic is to add to the algebraic theory of rings two more sequents yielding non triviality and locality: one common form of these axioms is $$1=0\vdash\bot,\ \ \top\vdash\exists y(xy=1)\vee\exists y ((1-x)y=1).$$ Of course these axioms are no longer equational: they belong to coherent logic, since they contain the symbols $\bot$ and finitary $\vee$. This axiomatization is used to talk in general about local ring objects in coherent categories (see https://ncatlab.org/nlab/show/local+ring at section 5).

My question is the following: how can we be sure that the theory of local rings cannot be stated in a weaker fragment of logic? Is there any way to prove that no equivalent axiomatization of local rings in a weaker fragment of logic (say in Horn or cartesian or regular logic) can be given?

• What is regular logic, if not predicate logic? Feb 21, 2018 at 17:44
• @Sudix By regular I mean a theory whose axioms only contain finite $\wedge$, $\top$ and $\exists$ (as defined in ncatlab.org/nlab/show/regular+logic) Feb 21, 2018 at 17:49
• The article says that regular logic is a subset of coherent logic Feb 21, 2018 at 18:48
• @Sudix Yes, that is exactly why I wonder if the axioms above can be written in the smaller fragment of regular logic instead of exploiting coherent logic (i.e. also $\vee$ and $\bot$) Feb 21, 2018 at 18:53

You can immediately rule out Cartesian and Horn theories as the category of models (in $\mathbf{Set}$) of any such theories always includes an object whose carrier is the singleton set. The constantly terminal object functor is always finite limit preserving. Non-triviality means for any local ring $R$, $|R|\geq 2$. This means no formula of cartesian logic can be unsatisfiable if all the free variables are replaced with the same variable.
• In my judgement (which may well be wrong), it would be good enough for the OP's purposes for there to be a Horn (or whatever) theory $T$ for which the category of models of $T$ is equivalent to the category of local rings, and maybe requiring that the local ring corresponding not-very-exotic example of what I mean, if the OP was interested in discretely valued fields, he would be satisfied with a nice formulation of the theory of discrete valuation rings if there were such a thing.