Can there be a consistent strong effectively generated first order theory that is complete for all sentences of its language up to a specific length?

Question

Lets work with some specific way of measuring length of formulas of first order logic theories. Is it possible to have a consistent effectively generated first order theory [i.e. recursively enumerable], that can interpret PA, that is complete for all sentences of its language below a specified length? Of course here we mean sentences that has NO defined symbols in them.

Answer 1

As long as our language is finite, all reasonable notions of length I can think of have the property that there are only finitely many sentences of a given length. This means the answer to the question is trivially yes (e.g. let $PA[n]$ consist of $PA$ + all true sentences of length $<n$).

• It is of course true that the sequence of theories $\langle PA[n]\rangle_{n\in\mathbb{N}}$ isn't effective, but each specific theory $PA[n]$ is.

(And passing to an infinite language doesn't change anything: only finitely much of that language will be necessary to interpret $PA$, so just look at a theory trivializes the remaining symbols; for example set all function symbols to be projection onto the first coordinate, all constants to the element corresponding to $0$, and all relations to the emptyset.)

---

What if we demand a bit more than mere effectivity - namely, that we have an effective sequence of effective theories with the desired property? That is, we have a computable function $f$ such that for each $i$, $f(i)$ is an index for a consistent computable extension of PA which decides all statements of length $\le i$.

(I'm talking about extensions of PA rather than theories interpreting PA; this doesn't change anything and results in a simpler picture.)

This requirement is strong enough to prevent the silly argument above; in fact, now the answer to the question becomes no, there is no such sequence of theories. The proof isn't as simple as taking the union of the theories involved (since there's no requirement that our theories be jointly consistent, they simply have to be individually consistent). Instead, we use the diagonal lemma as follows.

Let $\langle p_i\rangle_{i\in\mathbb{N}}$ be some fixed effective enumeration of the sentences of arithmetic such that each $p_i$ has length $<i$. Suppose $f$ is as above. Let $q_i$ be $p_i$ if the $f(i)$th theory proves $p_i$ and $\neg p_i$ if the $f(i)$th theory proves $\neg p_i$. Note that the sequence $\langle q_i\rangle_{i\in\mathbb{N}}$ is computable since the function $f$ is computable and the $f(i)$th theory decides $p_i$. Moreover, we know that $PA\cup\{q_i\}$ is consistent for each $i$ (since the $f(i)$th theory extends $PA$ and proves $q_i$).

But from this we get a contradiction. By the diagonal theorem there is an $i\in\mathbb{N}$ such that $p_i$ is equivalent over $PA$ to "$q_i$ is $\neg p_i$" (appropriately expressed). But now we have a problem - since $PA$ is $\Sigma_1$-complete, it can compute each $q_i$ correctly, we can argue:

• Suppose $q_i=p_i$. Then $PA$ proves "$q_i$ is not $\neg p_i$," hence $PA$ proves $\neg p_i$. So $p_i$ is not consistent with $PA$, but this contradicts the requirement that $q_i$ is consistent with $PA$.

• Suppose $q_i=\neg p_i$. Then $PA$ proves "$q_i$ is $\neg p_i$," hence $PA$ proves $p_i$. So $\neg p_i$ is not consistent with $PA$, but this contradicts the requirement that $q_i$ is consistent with $PA$.