Dequantifying first-order theories

post by jessicata (jessica.liu.taylor) · 2024-04-23T19:04:49.000Z · LW · GW · 9 comments

This is a link post for https://unstableontology.com/2024/04/23/dequantifying-first-order-theories/

Contents

  Propositional theories and provability-preserving translations
  Recap of consistent guessing oracles
  Applying consistent guessing oracles to dequantification
  Conclusion
None
9 comments

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 and for arbitrary n). Not all of these statements are computable. In general, the question of whether a given statement is provable is a 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, , , 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 translates to and translates to , we would like to be provable in T if and only if is provable in U, but this is not necessarily the case with the specified U (in particular, is only provable in U whenever at least one of or is provable in T, but can be provable in T without either or 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 ), 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 . Let M(i, j) refer to a Turing machine that searches for proofs and disproofs of in the theory (that is, T with the additional axiom that ), returning "true" if it finds a proof first, "false" if it finds a disproof first. Note that, if is consistent, one cannot prove both and from .

We will now define the propositional theory U. The theory's propositional variables consist of ; 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 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 in the model:

Notationally, refers to the set {0, 1}, refers to the numbering of P in the ordering of all T-statements, and and 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 matches Q'(i) for i < j, then the consistent guessing oracle says that a machine searching for proofs and disproofs of 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 in order, assuring consistency at each step, assuming T was consistent to start with.

We will translate a T-statement 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 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 is provable in T if and only if is provable in U.

Let us consider the first direction. Assume 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, 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 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 . We add a finite number of axioms to U, stating matches the model's truth value for for . 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 , and for each , set to the model's truth value for , where f(n) specifies the model's truth value for . These assure that Q' matches the model of T, by setting Q values according to this model. We also know that cannot return true if is false in the model, and cannot return true if 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, is false, because Q' agrees with the model of T in which is false. By soundness of propositional logic, there is no proof of this statement in U.

So we have shown both directions, implying that is provable in T if and only if 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.

9 comments

Comments sorted by top scores.

comment by AlexMennen · 2024-04-24T05:57:59.341Z · LW(p) · GW(p)

I think what you proved essentially boils down to the fact that a consistent guessing oracle can be used to compute a completion of any consistent recursively axiomatizable theory. (In fact, it turns out that a consistent guessing oracle can be used to compute a model (in the sense of functions and relations on a set) of any consistent recursively axiomatizable theory; this follows from what you showed and the fact that an oracle for a complete theory can be used to compute a model of that theory.)

I disagree with

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.

The translation from T to U is computable. The consistent guessing oracle only came in to find a completion of U, but it could also find a completion of T (in fact, a completion of U can be computably translated to a completion of T), so the consistent guessing oracle doesn't really have anything to do with the relationship between T and U.

Replies from: jessica.liu.taylor
comment by jessicata (jessica.liu.taylor) · 2024-04-24T12:14:04.485Z · LW(p) · GW(p)

U axiomatizes a consistent guessing oracle producing a model of T. There is no consistent guessing oracle applied to U.

In the previous post I showed that a consistent guessing oracle can produce a model of T. What I show in this post is that the theory of this oracle can be embedded in propositional logic so as to enable provability preserving translations.

Replies from: AlexMennen
comment by AlexMennen · 2024-04-25T04:29:41.521Z · LW(p) · GW(p)

I see that when I commented yesterday, I was confused about how you had defined U. You're right that you don't need a consistent guessing oracle to get from U to a completion of U, since the axioms are all atomic propositions, and you can just set the remaining atomic propositions however you want. However, this introduces the problem that getting the axioms of U requires a halting oracle, not just a consistent guessing oracle, since to tell whether something is an axiom, you need to know whether there actually is a proof of a given thing in T.

Replies from: jessica.liu.taylor
comment by jessicata (jessica.liu.taylor) · 2024-04-25T14:41:25.154Z · LW(p) · GW(p)

The axioms of U are recursively enumerable. You run all M(i,j) in parallel and output a new axiom whenever one halts. That's enough to computably check a proof if the proof specifies the indices of all axioms used in the recursive enumeration.

Replies from: AlexMennen
comment by AlexMennen · 2024-04-29T04:16:31.831Z · LW(p) · GW(p)

Yeah, sorry that was unclear; there's no need for any form of hypercomputation to get an enumeration of the axioms of U. But you need a halting oracle to distinguish between the axioms and non-axioms. If you don't care about distinguishing axioms from non-axioms, but you do want to get an assignment of truthvalues to the atomic formulas Q(i,j) that's consistent with the axioms of U, then that is applying a consistent guessing oracle to U.

comment by AlexMennen · 2024-04-24T05:30:00.106Z · LW(p) · GW(p)

a consistent guessing oracle rather than a halting oracle (which I theorize to be more powerful than a consistent guessing oracle).

This is correct. Or at least, the claim I'm interpreting this as is that there exist consistent guessing oracles that are strictly weaker than a halting oracle, and that claim is correct. Specifically, it follows from the low basis theorem that there are consistent guessing oracles that are low, meaning that access to a halting oracle makes it possible to tell whether any Turing machine with access to the consistent guessing oracle halts. In contrast, access to a halting oracle does not make it possible to tell whether any Turing machine with access to a halting oracle halts.

Replies from: jessica.liu.taylor
comment by jessicata (jessica.liu.taylor) · 2024-04-24T12:15:23.805Z · LW(p) · GW(p)

Thanks, didn't know about the low basis theorem.

comment by AlexMennen · 2024-04-24T05:24:48.137Z · LW(p) · GW(p)

I don't understand what relevance the first paragraph is supposed to have to the rest of the post.

Replies from: jessica.liu.taylor
comment by jessicata (jessica.liu.taylor) · 2024-04-24T12:10:42.755Z · LW(p) · GW(p)

LS shows to be impossible one type of infinitarian reference, namely to uncountably infinite sets. I am interested in showing to be impossible a different kind of infinitarian reference. "Impossible" and "reference" are, of course, interpreted differently by different people.