7
$\begingroup$

It is known that there are a number of expansions of the structure $\mathfrak{N}:=(\mathbb{N};+)$ which are decidable (= have computable theories); one such example is the expansion by a predicate naming the powers of $2$, or even the function $x\mapsto 2^x$, see here. In each such case that I'm aware of, the proof of decidability of the expansion in fact establishes something more, namely that Presburger arithmetic + a small set of axioms for the additional structure is a complete theory.

This motivates the following question (conflating relations and symbols naming them for simplicity):

(Question 1) For $n\in\mathbb{N}$ and $A\subseteq\mathbb{N}^n$, let $\mathfrak{N}_A$ be the expansion of $\mathfrak{N}$ by (a relation symbol interpreted as) $A$. If $\mathfrak{N}_A$ is decidable, must there be some finite $\{+,A\}$-theory $T$ such that $T$ + the full induction scheme for $\{+,A\}$-formulas axiomatizes $Th(\mathfrak{N}_A$)?

My suspicion is that the answer is negative, but I don't see how to prove it. There is, though, a natural(-to-me) additional hypothesis on $A$ we can add to make a positive answer more plausible:

(Question 2) What if in Question 1 we additionally required $A$ to have the property that there is a finite $\{+,A\}$-theory $S$ such that $\mathfrak{N}_A\models S$ and the characteristic function of $A$ is strongly representable in $S$ + the full induction scheme for $\{+,A\}$-formulas?

I have no intuition for what the answer for Question 2 may be.

$\endgroup$
4
  • $\begingroup$ It would be fairly easy to show that the answer to Question 1 is negative via the reduction to $\mathsf{MSO}(\mathbb{N};0,S)$. There we have the property that definable classes of sets of naturals are if treated as languages of infinite $\{0,1\}$-words are precisely $\omega$-regular languages (i.e. languages of the form $L_1L_2^\omega=\{\alpha\beta_0\beta_1\ldots\beta_n\ldots\mid \alpha\in L_1,\beta_i\in L_2\}$ where $L_1$ and $L_2$ are regular). $\endgroup$ Commented Aug 8, 2023 at 17:34
  • $\begingroup$ Using the characterization above pick a set $B$ of naturals such that it is not definable by a monadic formula (i.e. is no finally periodic), but the set of monadic $\varphi(X)$ that are true on $B$ is decidable (note that we could go back and forth between monadic formulas and $\omega$-regular expressions). I think that it should be relatively easy to show that for $B=\{n^2\mid n\in\mathbb{N}\}$ we could effectively check if it as an $\omega$-word of $0$ and $1$'s lies in a particular language $L_1L_2^\omega$. $\endgroup$ Commented Aug 8, 2023 at 17:34
  • $\begingroup$ Then we pick $A=\{2^n\mid n\in B\}$ and observe that $\mathsf{Th}(\mathbb{N};+,A)$ isn't finitely axiomatizable over induction (here we using interpretation of (\mathbb{N};+) in $(\mathbb{N},\mathcal{P}(\mathbb{N};S)$, where naturals are interpreted by finite sets of naturals representing their binary expansions). $\endgroup$ Commented Aug 8, 2023 at 17:34
  • $\begingroup$ This method, of course, doesn't help for Question 2, since if $A$ would be strongly representable over finite set of axioms, $B$ would be definable in MSO. $\endgroup$ Commented Aug 8, 2023 at 17:36

0

You must log in to answer this question.