24
$\begingroup$

Consider the first-order theory whose intended/standard model is the natural numbers $\mathbb{N}$, with constant $0\in \mathbb{N}$, with an injective successor operation $s$ such that $0$ is not a successor, and with the binary operation $\max\{n,m\}$, satisfying the axioms that hold in the usual $\mathbb{N}$. For instance: $\max$ is commutative and associative with $\max\{0,n\}=n$, hence $(\mathbb{N},\max,0)$ is a monoid, and then compatibility axioms like $\max\{n,sn\} = sn$, and $\max\{sn,sm\} = s\max\{n,m\}$ and perhaps so on. No induction axiom schema is assumed.

Is there anything known about this theory? I'm guessing it's decidable, because this is apparently one way that type universes are indexed in some proof assistants. My 'and perhaps so on' above should be read as indicated what is needed for that use case, it's just that I'm not 100% sure on what is needed. The two axioms I gave seem to be all that I can think of that is critically needed, but if there is anything obvious, throw that in as well. Since we don't have induction, I'd lean on the side of putting more axioms in that would otherwise need induction to prove.

$\endgroup$
9
  • 9
    $\begingroup$ Since this is a subtheory of (more precisely, interpretable in) Presburger arithmetic it's definitely decidable, but I suspect that more can be said from a complexity theory angle. Also, note that both $0$ and $s$ are definable from $\max$. $\endgroup$ Commented May 28 at 2:24
  • 7
    $\begingroup$ The theory is equivalent to the theory of $\langle\mathbb{N},<\rangle$, since from max we can define the order, and from the order we can define successor. This is the theory of a discrete order with a least element and no largest element. $\endgroup$ Commented May 28 at 2:33
  • 1
    $\begingroup$ That's right. From the work of Büchi and others we know that we can add any automatic function to Presburger arithmetic without affecting decidability nor the complexity of the decision algorithm. I also suspect this theory has a much easier decision algorithm. $\endgroup$ Commented May 28 at 2:34
  • 3
    $\begingroup$ @JoelDavidHamkins I was being foolish - of course it's not linear, since we can encode SAT instances! (Indeed, even the two-element structure's theory is PSPACE-complete, see this old MSE question of mine.) I've deleted my very silly comment. $\endgroup$ Commented May 28 at 3:42
  • 6
    $\begingroup$ Yes, a simple Ehrenfeucht–Fraïssé argument shows that it is PSPACE-complete. TYou can find this in Ferrante and Rackoff. $\endgroup$ Commented May 28 at 6:28

1 Answer 1

36
$\begingroup$

This theory is equivalent to the theory of a discrete linear order with a least element and no largest element, that is, the theory of $\langle\mathbb{N},<\rangle$. From max we can define the order and conversely, and from the order we can define successor. So you don't actually need the successor if you have max as it is definable. And of course $0$ is definable. No induction axiom is needed, since the theory is already complete when making only very basic assertions.

A discrete linear order is a linear order in which every non-maximal point has an immediate successor and every non-minimal point has an immediate predecessor. The theory of a discrete linear order is one of the standard theories studied in introductory model theory, and so let me mention a few of the notable model-theoretic properties.

  • The theory of a discrete linear order with minimal element $0$ and no maximal element admits elimination of quantifiers in the expansion with a constant for $0$ and the successor operation. That is, every assertion is equivalent to a quantifier-free assertion in this expanded language. (Similar results hold for the other endpoint situations.)
  • The models of this theory consist of $\mathbb{N}+\mathbb{Z}\cdot L$, that is, an initial copy of $\mathbb{N}$ followed by any number of $\mathbb{Z}$ chains, placed into any linear order $L$ amongst each other.
  • Since all these models agree on quantifier-free assertions in the language with 0 and successor, it follows by the quantifier-elimination result that the theory is complete, and so this is exactly the theory of $\langle\mathbb{N},0,<\rangle$.
  • The theory is not categorical in any infinite power, since we can take the $\mathbb{Z}$-chains in different non-isomorphic orders.
  • The theory is decidable. This follows from it being computably axiomatizable and complete, since we can search for proofs. But it also follows from the quantifier-elimination result, since any given sentence is provably equivalent to a quantifier-free sentence, which we can find by the quantifier-elimination process (or by searching for proofs), and the truth of quantifier-free sentences are easily decided, since such a sentence is a Boolean combination of trivial assertions about successors of $0$.

In particular, all these things will also hold of your theory (in the language with 0, $S$, max). Your theory admits elimination of quantifiers, has a simple complete axiomatization, has a clear spectrum of models that we understand completely, is not categorical in any infinite power, is decidable, and so forth.

Meanwhile, it is interesting to prove that max is not definable from successor, and so your theory is strictly stronger than the theory of successor. One can see this by observing that every model of the theory of successor consists of a copy of $\mathbb{N}$ and then some number of side-by-side $\mathbb{Z}$ chains, with successor acting as expected within each chain. Since we can permute those $\mathbb{Z}$ chains while preserving $S$, it shows that no linear order can be definable. And so neither is max. The theory of successor is not categorical for countable models---it has countably many models depending on the number of $\mathbb{Z}$ chains that are present, but it is categorical in all uncountable powers, since the number of $\mathbb{Z}$ chains will be the same as the size of the uncountable model, and so all models of a given uncountable cardinality are isomorphic.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.