3
$\begingroup$

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?

$\endgroup$
4
  • $\begingroup$ What is regular logic, if not predicate logic? $\endgroup$
    – Sudix
    Feb 21, 2018 at 17:44
  • 1
    $\begingroup$ @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) $\endgroup$
    – TheMadcapLaughs
    Feb 21, 2018 at 17:49
  • $\begingroup$ The article says that regular logic is a subset of coherent logic $\endgroup$
    – Sudix
    Feb 21, 2018 at 18:48
  • 1
    $\begingroup$ @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$) $\endgroup$
    – TheMadcapLaughs
    Feb 21, 2018 at 18:53

1 Answer 1

Reset to default
1
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ A priori, there is the possibility that the usual underlying set of elements functor isn't the correct forgetful functor. So, the fact that there is no local ring whose underlying set of elements is a singleton doesn't immediately rule things out. $\endgroup$
    – user14972
    Feb 22, 2018 at 1:54
  • $\begingroup$ I don't really understand what you're getting at. I could recast what I'm saying in traditional model theoretic terms. The coherent theory of local rings is, in particular, a first-order theory. The (traditional) models of that theory are all the local rings. I'm saying the domains of all of those models have at least two elements. I'm also saying for any regular theory, that theory is satisfied by a model consisting of a single element. Therefore, if there was a regular theory for local rings, it would have the same class of models as the coherent theory, but also a model over a singleton. $\endgroup$
    – Derek Elkins left SE
    Feb 22, 2018 at 2:52
  • $\begingroup$ In the approach in the answer and in the comment, there's a specific underlying set functor. Picking one other than the "usual" one is not an option. $\endgroup$
    – Derek Elkins left SE
    Feb 22, 2018 at 2:53
  • $\begingroup$ 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. $\endgroup$
    – user14972
    Feb 22, 2018 at 3:15

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .