The Löwenheim–Skolem theorem implies, among other things, that any first-order theory whose symbols are countable, and which has an infinite model, has a countably infinite model. This means that, in attempting to refer to uncountably infinite structures (such as in set theory), one "may as well" be referring to an only countably infinite structure, as far as proofs are concerned.

The main limitation I see with this theorem is that it preserves arbitrarily deep quantifier nesting. In Peano arithmetic, it is possible to form statements that correspond (under the standard interpretation) to arbitrary statements in the arithmetic hierarchy (by which I mean, the union of ${\Sigma }_n^0$ and ${\Pi }_n^0$ for arbitrary n). Not all of these statements are computable. In general, the question of whether a given statement is provable is a ${\Sigma }_1^0$ statement. So, even with a countable model, one can still believe one's self to be "referring" to high levels of the arithmetic hierarchy, despite the computational implausibility of this.

What I aim to show is that these statements that appear to refer to high levels of the arithmetic hierarchy are, in terms of provability, equivalent to different statements that only refer to a bounded level of hypercomputation. I call this "dequantification", as it translates statements that may have deeply nested quantifiers to ones with bounded or no quantifiers.

I first attempted translating statements in a consistent first-order theory T to statements in a different consistent first-order theory U, such that the translated statements have only bounded quantifier depth, as do the axioms of U. This succeeded, but then I realized that I didn't even need U to be first-order; U could instead be a propositional theory (with a recursively enumerable axiom schema).

Propositional theories and provability-preserving translations

Here I will, for specificity, define propositional theories. A propositional theory is specified by a countable set of proposition symbols, and a countable set of axioms, each of which is a statement in the theory. Statements in the theory consist of proposition symbols, $\top$, $\perp$, and statements formed from and/or/not and other statements. Proving a statement in a propositional theory consists of an ordinary propositional calculus proof that it follows from some finite subset of the axioms (I assume that base propositional calculus is specified by inference rules, containing no axioms).

A propositional theory is recursively enumerable if there exists a Turing machine that eventually prints all its axioms; assume that the (countable) proposition symbols are specified by their natural indices in some standard ordering. If the theory is recursively enumerable, then proofs (that specify the indices of axioms they use in the recursive enumeration) can be checked for validity by a Turing machine.

Due to the soundness and completeness of propositional calculus, a statement in a propositional theory is provable if and only if it is true in all models of the theory. Here, a model consists of an assignment of Boolean truth values to proposition symbols such that all axioms are true. (Meanwhile, Gödel's completeness theorem shows something similar for first-order logic: a statement is provable in a first-order theory if and only if it is true in all models. Inter-conversion between models as "assignments of truth values to sentences" and models as "interpretations for predicates, functions, and so on" is fairly standard in model theory.)

Let's start with a consistent first-order theory T, which may, like propositional theories, have a countable set of symbols and axioms. Also assume this theory is recursively enumerable, that is, there is a Turing machine printing its axioms.

The initial challenge is to find a recursively enumerable propositional theory U and a computable translation of T-statements to U-statements, such that a T-statement is provable if and only if its translation is provable.

This turns out to be trivial. We define U to have one propositional symbol per statement of T, and recursively enumerate U's axioms by attempting to prove every T-statement in parallel, and adding its corresponding propositional symbol as an axiom of U whenever such a proof is found. Now, if a T-statement is provable, its corresponding U-statement is as well, and if it is not provable, its U-statement is not (as no axioms of U will imply anything about this U-statement).

This is somewhat unsatisfying. In particular, propositional compositions of T-statements do not necessarily have equivalent provability to corresponding propositional compositions of the translations of these T-statements. For example, if ${\varphi }_1$ translates to ${\psi }_1$ and ${\varphi }_2$ translates to ${\psi }_2$, we would like ${\varphi }_1\vee {\varphi }_2$ to be provable in T if and only if ${\psi }_1\vee {\psi }_2$ is provable in U, but this is not necessarily the case with the specified U (in particular, ${\psi }_1\vee {\psi }_2$ is only provable in U whenever at least one of ${\varphi }_1$ or ${\varphi }_2$ is provable in T, but ${\varphi }_1\vee {\varphi }_2$ can be provable in T without either ${\varphi }_1$ or ${\varphi }_2$ being provable.).

We could attempt to solve this problem by introducing propositional variables corresponding to quantified statements, and an axiom schema to specify implications between these and other statements according to the inference rules of first-order logic. But first-order logic requires supporting unbound variables (e.g. from P(x) for unbound x, infer $\forall x:P\left(x\right)$), and this introduces unnecessary complexities. So I will give a different solution.

Recap of consistent guessing oracles

In a previous post, I introduced an uncomputable problem: given a Turing machine that returns a Boolean whenever it halts, give a guess for this Boolean that matches its answer if it halts, and can be anything if it doesn't halt. I called oracles solving this problem "arbitration oracles". Scott Aaronson has previously named this problem the "consistent guessing problem", and I will use this terminology due to temporal priority.

In my post, I noted that an oracle that solves the consistent guessing problem can be used to form a model of any consistent first-order theory. Here, "model" means an assignment of truth values to all statements of the theory, which are compatible with each other and the axioms. The way this works is that we number all statements of the theory in order. We start with the first, and ask the consistent guessing oracle about a Turing machine that searches for proofs and disproofs of this first statement in the theory, returning "true" if it finds a proof first, "false" if it finds a disproof first. We use its answer to assign a truth value to this first statement. For subsequent statements, we search for proofs/disproofs of the statement given the previous commitments to truth values already made. This is essentially the same idea as in the Demski prior, though using a consistent guessing oracle rather than a halting oracle (which I theorize to be more powerful than a consistent guessing oracle).

Applying consistent guessing oracles to dequantification

To apply this idea to our problem, start with some recursive enumeration of T's statements ${\varphi }_0,{\varphi }_1,{\varphi }_2,\dots$. Let M(i, j) refer to a Turing machine that searches for proofs and disproofs of ${\varphi }_j$ in the theory $T+{\varphi }_i$ (that is, T with the additional axiom that ${\varphi }_i$), returning "true" if it finds a proof first, "false" if it finds a disproof first. Note that, if $T+{\varphi }_i$ is consistent, one cannot prove both ${\varphi }_j$ and $\neg {\varphi }_j$ from $T+{\varphi }_i$.

We will now define the propositional theory U. The theory's propositional variables consist of $\left\{Q\right(i,j)|i,j\in N\}$; the statement Q(i, j) is supposed to represent a consistent guessing oracle's answer to M(i, j).

U's axioms constrain these Q(i, j) to be consistent guesses. We recursively enumerate U's axioms by running all M(i, j) in parallel; if any ever returns true, we add the corresponding Q(i, j) as an axiom, and if any ever returns false, we add the corresponding $\neg Q(i,j)$ as an axiom. This recursively enumerable axiom schema specifies exactly the condition that each Q(i, j) is a consistent guess for M(i, j). And U is consistent, because its proposition variables can be set according to some consistent guessing oracle, of which at least one exists.

Now, as explained before, we can use Q(i, j) to derive a model of T. We will do this by defining U-propositions Q'(i) for each natural i, each of which is supposed to represent the truth value of ${\varphi }_i$ in the model:

$Q^{\prime }\left(0\right):=Q(┌\top ┐,0)$

$j>0\Rightarrow Q^{\prime }\left(j\right):={\bigvee }_{x_0,\dots ,x_{j-1}\in 2}\left({\bigwedge }_{n=0\dots j-1}Y\right(x_n,n\left)\right)\wedge Q(┌{\bigwedge }_{n=0\dots j-1}Z(x_n,n)┐,j)$

$Y(0,n):=\neg Q^{\prime }\left(n\right)$

$Y(1,n):=Q^{\prime }\left(n\right)$

$Z(0,n):=\neg {\varphi }_n$

$Z(1,n):={\varphi }_n$

Notationally, $2$ refers to the set {0, 1}, $┌P┐$ refers to the numbering of P in the ordering of all T-statements, and $\bigvee$ and $\bigwedge$ refer to finite disjunctions and conjunctions respectively. My notation here with the quotations is not completely rigorous; what is important is that there is a computable way to construct a U-statement Q'(j) for any j, by expanding everything out. Although the expanded propositions are gigantic, this is not a problem for computability. (Note that, while the resulting expanded propositions contain Q(i, j) for constants i and j, this does not go beyond the notation of propositional theories, because Q(i, j) refers to a specific propositional variable if i and j are known.)

Semantically, what Q'(j) says is that, if we add assumptions that the ${\varphi }_i$ matches Q'(i) for i < j, then the consistent guessing oracle says that a machine searching for proofs and disproofs of ${\varphi }_j$ in T given these assumptions guesses that a proof is found before a disproof (noting, if there are neither proofs nor disproofs, the consistent guessing oracle can return either answer). Q' specifies the iterative logic of making decisions about each ${\varphi }_i$ in order, assuring consistency at each step, assuming T was consistent to start with.

We will translate a T-statement ${\varphi }_j$ to the corresponding U-statement Q'(j). What we wish to show is that this translation preserves provability of propositional combinations of T-statements. To be more precise, we assume some m and a function $g({\sigma }_1,\dots ,{\sigma }_m)$ that forms a new statement from a list of m propositions, using only propositional connectives (and, or, not). What we want to show is that $g({\varphi }_{j_1},\dots ,{\varphi }_{j_m})$ is provable in T if and only if $g\left(Q^{\prime }\right(j_1),\dots ,Q^{\prime }(j_m\left)\right)$ is provable in U.

Let us consider the first direction. Assume $g({\varphi }_{j_1},\dots ,{\varphi }_{j_m})$ is provable in T. By Gödel's completeness theorem, it is true in all models of T. In any model of U, Q' must represent a model of T, because Q' iteratively constructs a model of T using a consistent guessing oracle. Therefore, $g\left(Q^{\prime }\right(j_1),\dots ,Q^{\prime }(j_m\left)\right)$ is true in all models of U. Accordingly, due to completeness of propositional calculus, this statement is provable in U.

Let us consider the other direction. Assume $g({\varphi }_{j_1},\dots ,{\varphi }_{j_m})$ is not provable in T. By Gödel's completeness theorem, it is not true in all models of T. So there is some particular model of T in which this statement is false.

This model assigns truth values to ${\varphi }_{j_1},\dots ,{\varphi }_{j_m}$. We add a finite number of axioms to U, stating $Q^{\prime }\left(j_k\right)$ matches the model's truth value for ${\varphi }_{j_k}$ for $k=1\dots m$. To show that U with the addition of these axioms is consistent, we consider that it is possible to set Q'(0) to the model's truth value for ${\varphi }_0$, and for each $1\le j\le {max}_{k=1\dots m}{j}_k$, set $Q(┌{\bigwedge }_{n=0\dots j-1}Z(f\left(n\right),n)┐,j)$ to the model's truth value for ${\varphi }_j$, where f(n) specifies the model's truth value for ${\varphi }_n$. These assure that Q' matches the model of T, by setting Q values according to this model. We also know that $M(┌{\bigwedge }_{n=0\dots j-1}Z(f\left(n\right),n)┐,j)$ cannot return true if ${\varphi }_j$ is false in the model, and cannot return true if ${\varphi }_i$ is true in the model; this is because Gödel's completeness theorem implies no T-statement consistent with the model can be disproven.

This shows that U with these additional axioms is consistent. Therefore, a model of U plus these additional axioms exists. This model is also a model of U, and in this model, $g\left(Q^{\prime }\right(j_1),\dots ,Q^{\prime }(j_m\left)\right)$ is false, because Q' agrees with the model of T in which $g({\varphi }_{j_1},\dots ,{\varphi }_{j_m})$ is false. By soundness of propositional logic, there is no proof of this statement in U.

So we have shown both directions, implying that $g({\varphi }_{j_1},\dots ,{\varphi }_{j_m})$ is provable in T if and only if $g\left(Q^{\prime }\right(j_1),\dots ,Q^{\prime }(j_m\left)\right)$ is provable in U. What this means is that translating a propositional composition of T-statements to the same propositional composition of translated U-statements results in equivalent provability.

Conclusion

The upshot of this is that statements of a consistent first-order theory T can be translated to a propositional theory U (with a recursively enumerable axiom schema), in a way that preserves provability of propositional compositions. Philosophically, what I take from this is that, even if statements in a first-order theory such as Peano arithmetic appear to refer to high levels of the Arithmetic hierarchy, as far as proof theory is concerned, they may as well be referring to a fixed low level of hypercomputation, namely a consistent guessing oracle. While one can interpret Peano arithmetic statements as about high levels of the arithmetic hierarchy, this is to some extent a projection; Peano arithmetic fails to capture the intuitive notion of the standard naturals, as non-standard models exist.

One oddity is that consistent guessing oracles are underspecified: they may return either answer for a Turing machine that fails to halt. This is in correspondence with the way that sufficiently powerful first-order systems are incomplete (Gödel's first incompleteness theorem). Since some statements in Peano arithmetic are neither provable nor disprovable, they must be represented by some propositional statement that is neither provable nor disprovable, and so the uncertainty about Peano arithmetic statements translates to uncertainty about the consistent guessing oracle in U.

In Peano arithmetic, one can look at an undecidable statement, and think it still has a definite truth value, as one interprets the Peano statement as referring to the standard naturals. But as far as proof theory is concerned, the statement doesn't have a definite truth value. And this becomes more clear when discussing consistent guessing oracles, which one can less easily project definiteness onto compared with Peano arithmetic statements, despite them being equally underspecified by their respective theories.