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?
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.
For a formula in regular logic, you can rewrite it so that it consists of a series of existential quantifiers applied to a formula of cartesian logic. The formula is thus satisfiable by instantiating all the existential quantifiers to the same variable (and replacing all remaining free variables with that variable). So again we get the statement that the singleton set is always a model.