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.

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$4more comments