9
$\begingroup$

Recall that $\mathsf{R}$ is the theory of arithmetic consisting of the quantifier-free theory of $(\mathbb{N};+,\times,0,1,<)$ together with, for each $k\in\mathbb{N}$, the sentence $$\forall x[(\bigwedge_{i\le k}x\not=\underline{i})\rightarrow \underline{k}<x]$$ where $\underline{n}$ is the numeral standing for $n$. $\mathsf{R}$ is strong enough to be subject to the first incompleteness theorem (see Beklemishev and Jerabek for some relevant information on this point) and is not finitely axiomatizable (in contrast with Robinson's more famous arithmetic $\mathsf{Q}$).

My question is whether $\mathsf{R}$ is finitely axiomatizable when we allow schemes, in a limited sense, as well as sentences. By "scheme" here I mean the following:

A scheme of sentences in a given language $\Sigma$ is a sentence $\sigma$ in the language gotten by adding a new relation symbol $A$ (of some finite arity) to $\Sigma$. An instance of a scheme $\sigma$ is then a sentence of the form $$\forall y_1,...,y_n(\sigma[A/\varphi(y_1,...,y_n,x_1,....,x_k)])$$ where $\varphi$ is some $(n+k)$-ary formula in the original language $\Sigma$ and $\sigma[A/\varphi(y_1,...,y_n,x_1,..., x_k)]$ is the $L$-formula gotten by replacing each "$A(t_1,...,t_k)$" with "$\varphi(y_1,...,y_n,t_1,...,t_k)$" throughout $\sigma$.

See here for some comments on this notion. A theory is scheme-finitely axiomatizable if it can be axiomatized by a finite set of sentences together with the set of all instances of finitely many schemes in the above sense. Clearly every scheme-finitely axiomatizable theory is computably axiomatizable, but the converse fails even for finite languages. I suspect that in fact $\mathsf{R}$ witnesses the failure of the converse - basically, $\mathsf{R}$ doesn't seem to entail any nontrivial schemes in this particular sense at all - but I don't see how to prove that. Separately, I don't believe that the Visser/Vaught result on axiomatization by schemes can give a positive answer here, since $\mathsf{R}$ seems to lack the needed coding power.

$\endgroup$
5
  • 1
    $\begingroup$ And, indeed, R cannot interpret $\mathrm{VS}_2$ at all (let alone directly), as $\mathrm{VS}_2$ is a finite theory with no finite models, while R is locally finitely satisfiable. $\endgroup$ Nov 18, 2020 at 9:14
  • $\begingroup$ @EmilJeřábek Fascinating, I wasn't aware of that! $\endgroup$ Nov 18, 2020 at 13:36
  • $\begingroup$ Harvey Friedman youtube.com/watch?v=ne7V_9RTeTc recently raised the same question. What I figured out after a bit of thinking about that is that there is a locally finitely satisfiable theory axiomatized by finitely many schemes that doesn't have a finite model. Namely, the theory of discrete linear orders with the scheme $\exists x \exists y( x<y \land \forall z (x\le z \land z\le y \to (F(x)\leftrightarrow F(z)))$ (for any definable set $A$ either $A$ or its complement contains an interval of the size $\ge 2$). The trick here is to use $o$-minimality of discrete linear orders. $\endgroup$ Feb 23, 2022 at 16:39
  • 1
    $\begingroup$ Also I know how under a certain plausible complexity-theoretic assumption (a strengthening of $\mathtt{PH}\ne\mathtt{PSPACE}$) to construct a locally finitely satisfiable extension of $\mathsf{R}$ axiomatized by finitely many schemes. Note that by a result of Visser citeseerx.ist.psu.edu/viewdoc/… theory $\mathsf{R}$ is the interpretability-greatest locally finitely satisfiable theory. Hence this extension of $\mathsf{R}$ will be mutually interpretable with $\mathsf{R}$. $\endgroup$ Feb 23, 2022 at 19:15
  • 1
    $\begingroup$ @FedorPakhomov While that doesn't fully answer the question, it does make significant progress - could you add it as an answer so I can award it the bounty? $\endgroup$ Feb 27, 2022 at 4:20

1 Answer 1

4
+400
$\begingroup$

This answer is merely an advancement on the original question rather than a full answer.

Recall that a theory is locally finitely satisfiable if all its finite subtheories have finite models. Below I sketch a proof of the following theorem.

Theorem. There exists an extension $\mathsf{U}$ of $\mathsf{R}$ that is axiomatized by finitely many schemes such that the assumption $\mathtt{PH}\ne\mathtt{ExpTime}$ implies that $\mathsf{U}$ is locally finitely satisfiable.

Note that there is a result of Visser [1] that $\mathsf{R}$ interprets any locally finitely satisfiable theory. Thus the theorem above implies that if $\mathtt{PH}\ne\mathtt{ExpTime}$, then there is a locally finitely satisfiable theory that is mutually interpretable with $\mathsf{R}$.

Proof. Let us fix a theory $\mathsf{U}_0$ axiomatized by finitely many schemes such that all its infinite models are models of $\mathsf{R}$ and its finite models are precisely the rings $\mathbb{Z}_{2^n}$ (the order in $\mathbb{Z}_{2^n}$ is the standard order on the set $\{0,1,\ldots,2^n-1\}$).

We identify elements of $\mathbb{Z}_{2^n}$ with the binary strings of the length $n$, where each number corresponds to its own binary expansion. For formulas $\varphi(x)$ we consider the languages $$D_\varphi=\{\alpha\mid \mathbb{Z}_{2^{|\alpha|}}\models\varphi(\alpha)\}.$$ If $\varphi(x)$ is a first-order arithmetical formula, then clearly $D_\varphi\in\texttt{PH}$. Observe that $$\{D_\varphi\mid \varphi(x)\in \Sigma^1_1\}=\bigcup_{k\in\omega} \mathtt{NTime}(2^{xk}),$$ where in $\Sigma^1_1$-formulas we allow quantification over predicates of any finite arity.

Fix an $\mathtt{ExpTime}$-complete language $L$ such that $L\in \mathtt{Time}(2^{xk})$, for some $k$. Clearly, $L,\bar{L}\in \mathtt{NTime}(2^{xk'})$, for some $k'$. Fix $\Sigma^1_1$-formulas $\varphi_0(x)$ and $\varphi_1(x)$ such that $S_{\varphi_0}=L$ and $S_{\varphi_0}=\bar L$. For $i\in\{0,1\}$ the formula $\varphi_i(x)$ is of the form $\exists X^{(n_i)} \psi_i(x,X^{(n_i)})$. Let $U$ be the extension of $U_0$ by the scheme $$\exists x (\lnot \psi_0(x,X^{(n_0+1)}\upharpoonright x)\land \lnot \psi_1(x,Y^{(n_1+1)}\upharpoonright x)),$$ where $X^{(n+1)}\upharpoonright x$ is the $n$-ary relation $\{(y_1,\ldots,y_n)\mid (x,y_1,\ldots,y_n)\in X^{(n+1)}\}$.

Observe that $U$ doesn't have finite models. Indeed any model $\mathbb{Z}_{2^n}$ clearly satisfies the $\Sigma^1_1$-sentence corresponding to the negation of the scheme above: $$\exists X^{(n_0+1)}, Y^{(n_1+1)}\forall x ( \psi_0(x,X^{(n_0+1)}\upharpoonright x)\lor \psi_1(x,Y^{(n_1+1)}\upharpoonright x)).$$ Thus for any $n$ we could construct an instance of the scheme that would fail in $\mathbb{Z}_{2^n}$.

To finish the proof we use the assumption $\mathtt{PH}\ne \mathtt{ExpTime}$ to show that any finite fragment of $U$ has a finite model. Otherwise there would be $N$ and fisrt-order formulas $\theta_{i,j}(x,y_1,\ldots,y_{n_j},\vec{p}_i)$, $0\le i<N$, and $j\in\{0,1\}$ such that $$\mathbb{Z}_{2^n}\models \bigvee\limits_{0\le i<N}\exists \vec{p}_i\forall x (\bigvee_{j\in\{0,1\}} \psi_j(x,\{(y_1,\ldots,y_{n_j})\mid \theta_{i,j}(x,y_1,\ldots,y_{n_j})\})).$$ But in fact this implies that $L$ is equal to $D_\eta$, where $\eta(x)$ is $$\bigvee\limits_{0\le i<N}\exists \vec{p}_i(\psi_0(x,\{(y_1,\ldots,y_{n_0})\mid \theta_{i,0}(x,y_1,\ldots,y_{n_0})\})).$$ Thus $L\in\mathtt{PH}$, contradicting the assumption that $\mathtt{PH}\ne\mathtt{ExpTime}$. QED

[1] Visser, A. "Why the theory R is special." Logic Group preprint series 279 (2009).

$\endgroup$
5
  • $\begingroup$ @NoahSchweber Yes, sure. $\endgroup$ Feb 28, 2022 at 0:02
  • $\begingroup$ Why is $U_0$ axiomatizable by finitely many axiom schemata? $\endgroup$ Feb 28, 2022 at 7:39
  • $\begingroup$ @EmilJeřábek Of course I meant that we should fix $\mathsf{U}_0$ axiomatized by finitely many schemes (I have edited the answer to clarify this). I have in mind the following axiomatization of $\mathsf{U}_0$: 1. < is a linear order, where 0 is the least element and there is the greatest element $m$; 2. $0+1=1$; 3. $m+1=0$; 4. $x<x+1$ and $(x,x+1)=\emptyset$, for $0\le x <m$; 5. $x+0=x$; 6. $x+(y+1)=(x+y)+1$; 7. $x0=0$; 8. $x(y+1)=xy+x$; 9. either $0=m$ or there is $u<m$ s.t. $(u+1)+u=m$ and for any $0<x<u+1$ and $1<p<u+1$ if $xp=u+1$ and $p$ isn't $zw$ for any $1<z,w<p$, then $p=1+1$. $\endgroup$ Feb 28, 2022 at 8:49
  • $\begingroup$ Oh I see; it didn’t occur to me that one can force the universe to be a power of $2$ with finitely many axioms like this. Presumably you want $1<p\le u+1$ rather than $1<p<u+1$, as otherwise the axioms also hold in $\mathbb Z_{2p}$ for odd primes $p$. $\endgroup$ Feb 28, 2022 at 10:33
  • $\begingroup$ @EmilJeřábek Yes, indeed it should have been $1<p\le u+1$, thank you. $\endgroup$ Feb 28, 2022 at 12:45

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.