Decidable theories with arbitrary complexity

Question

Are there complete finitely axiomatizable first order theories (with equality) with arbitrarily high computational complexity?

Here, arbitrarily high (computational) complexity means that for every computable predicate $P$ one can choose a theory $T$ (as above) such that $P$ is polynomial time computable from $T$.

Variations:
- A variation is to drop equality.
- A natural weakening is to replace 'complete' with 'decidable'.
- Existence of finitely axiomatizable theories with arbitrary c.e. Turing degrees was proved by William Hanf in "Model-theoretic methods in the study of elementary logic". The proof might be adaptable to give complete (or at least decidable) finitely axiomatizable theories with arbitrarily high complexity.

Without finite axiomatization, there are examples:
- If $P⊆ℕ$ is decidable and every finite pattern occurs in $P$, i.e. $∀k \, ∀S⊆k \, ∃n \, ∀k'<k \, (P(n+k') ⇔ S(k'))$, then the monadic second order theory of $(ℕ, <, P)$ is decidable. Proof sketch: Reduce a sentence to acceptance of $P$ by a deterministic infinite automaton; the structure of $P$ ensures that we eventually reach a terminal strongly connected component of states, and reach all of its states infinitely often.
- We can also encode (with linear time encoding and decoding) a decidable predicate on strings for decidability together with S2S (the monadic second order theory of binary strings with functions $s→s0$ and $s→s1$ but no other operations). I suspect S2S with a decidable predicate $P$ is decidable if $P$ is sufficiently generic, specifically $∀S \, ∀k∈ℕ \, ∀(\text{infinite branch } T)$ $∃t∈T \, ∀v (|v|<k) (P(tv) ⇔ S(v))$ where $|v|$ is the length of $v$.

Without first order logic, there are finitely presented equational theories of arbitrarily high complexity, including I believe the word problem for a finitely presented group.

With first order logic, for appropriate computations I think the theory of the computation graph with a sequential write-only output tape is decidable, but I am not sure how to formalize and prove it. Note that first order logic can only express local properties, and for bounded graph degree, formulas can be converted to Hanf normal form. Perhaps, there are also groups with finitely axiomatizable theories of arbitrarily high complexity.

As an aside, for "natural" (not necessarily finitely axiomatizable) decidable theories, the highest complexity that I know is iterated exponential, which occurs for S2S, S1S, WS2S, WS1S, and related theories. For natural decidable problems more generally, reachability in vector addition systems has Ackermann complexity.

Answer 1

There are complete decidable finitely axiomatizable theories of arbitrary high computational complexity.

As Dmytro already sketched in his question there are complete decidable theories of arbitrary high computational complexity. Now we want to switch to finitely axiomatizable theories. This could be achieved using a theorem of Peretyatkin (see his book [1] and also a review of his book [2]; I haven't read the book myself and taking the formulation of the theorem from [2]):

Theorem(Peretyat'kin) There is a method of constructing, effectively in the c.e. index m of T, a finitely axiomatizable model-complete theory F(m) and an effective interpretation I of the theory T in F(m) such that I induces one-one correspondece between the completions of T and F(m).

Since a theory is complete and consistent iff it has a unique completion, if we apply this to a complete decidable theory $T$, then we would get a complete finitely axiomatizable theory $T'$ interpreting $T$. And, of course, the presence of the interpretation guarantees that $T$ is polynomial time reducible to $T'$. As James Hanson pointed in the comments, any complete finitely axiomatizable theory is decidable, hence we get complete decidable finitely axiomatizable theories of arbitrary high computational complexity.

Comment: Dmytro's example of complete decidable theories of arbitrary high computational complexity could be slightly simplified if instead of the monadic theory of $(\mathbb{N},<,P)$ the elementary theory of $(\mathbb{N},S,P)$ would be considered; then decidability could be proved by a more elementary quantifier elimination argument instead of Büchi automatons, see https://mathoverflow.net/a/426389/36385. There also an option to use the technique from my paper with Juvenal Murwanashyaka and Albert Visser [3]. There we define theory $\mathsf{J}$ (based on a theory earlier considered by Janiczak) and a polynomial time computable sequence of sentences $\mathsf{A}_i$ indexed by naturals $i$ such that $\mathsf{J}$ is consistent with any propositionally consistent Boolean combination of $\mathsf{A}_i$ and over $\mathsf{J}$ any sentence is equivalent to a Boolean combination of $\mathsf{A}_i$. Now given a decidable set $P$ we could consider theory $$\mathsf{J}+\{\mathsf{A}_i\mid i\in P\}\cup\{\lnot\mathsf{A}_i\mid i\not\in P\},$$ that is a complete consistent decidable theory such that $P$ is polynomial time reducible to it.

P.S. As I already indicated in the comments, I have learned about the book of Peretyat'kin from Albert Visser.

[1]Mikhail, G. Peretyat'kin. "Finitely Axiomatizable Theories." Siberian School of Algebra and Logic. Consultants Bureau, New York (1997).

[2]Vivienne Morley. Review of M.G. Peretyat'kin "Finitely Axiomatizable Theories.". https://doi.org/10.2307/2586818

[3]Juvenal Murwanashyaka, Fedor Pakhomov, and Albert Visser. "There are no minimal essentially undecidable Theories." arXiv preprint arXiv:2207.08174 (2022). https://arxiv.org/abs/2207.08174v2