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.

completefinitely axiomatizable first-order theory is always decidable. Is this not the case? $\endgroup$4more comments