Evitable iterates of the consistency operator

Abstract

Why are natural theories pre-well-ordered by consistency strength? In previous work, an approach to this question was proposed. This approach was inspired by Martin’s Conjecture, one of the most prominent conjectures in recursion theory. Fixing a reasonable subsystem T of arithmetic, the goal was to classify the recursive functions that are monotone with respect to the Lindenbaum algebra of T. According to an optimistic conjecture, roughly, every such function must be equivalent to an iterate ${Con}_{T}^{α}$ of the consistency operator “in the limit” within the ultrafilter of sentences that are true in the standard model.

In previous work the author established the first case of this optimistic conjecture; roughly, every recursive monotone function is either as weak as the identity operator in the limit or as strong as ${Con}_{T}$ in the limit. Yet in this note we prove that this optimistic conjecture fails already at the next step; there are recursive monotone functions that are neither as weak as ${Con}_{T}$ in the limit nor as strong as ${Con}_{T}^{2}$ in the limit. In fact, for every α, we produce a function that is cofinally equivalent to ${Con}_{T}^{α}$ yet cofinally equivalent to ${Con}_{T}$ .

Keywords

Proof theory consistency Martin’s Conjecture

1. Introduction

Why are natural axiomatic theories pre-well-ordered by consistency strength? It is not clear how to answer this question, nor even how to ask it mathematically, since there is no clear mathematical definition of the “natural” theories. Yet the informal question remains a well-known conceptual open problem.

In [5,9] an approach to this problem was proposed. The approach in question was inspired by Martin’s approach to an analogous question in recursion theory: Why are the natural Turing degrees well-ordered by Turing reducibility? To state Martin’s Conjecture, let’s introduce some important notions. First, a function $f : R \to R$ is degree-invariant if for all reals x, y: $\begin{matrix} x \equiv_{T} y ⟹ f (x) \equiv_{T} f (y) . \end{matrix}$ It seems that by relativizing the definition of a natural Turing degree one always produces a degree-invariant function on the reals. Second, a Turing cone is any set of the form ${x ∣ x ⩾_{T} y}$ . Assuming $AD$ , Martin proved that every degree-invariant set of reals (i.e., every set closed under Turing-equivalence) either contains a Turing cone or is disjoint from a Turing cone. This yields a ${0, 1}$ -valued measure on degree-invariant sets; a degree-invariant set has measure 0 if it is disjoint from a Turing cone and measure 1 if it contains a cone. When we say almost everywhere, we mean almost everywhere with respect to this measure. Finally, we say that $f ⩽_{m} g$ if $f (x) ⩽_{T} g (x)$ for almost all x. Martin’s Conjecture is stated as follows:

Conjecture 1.1 (Martin).

Assume $ZF + AD + DC$ .

If $f : 2^{ω} \to 2^{ω}$ is degree-invariant and it’s not the case that f is increasing almost everywhere, then f is constant almost everywhere.

$⩽_{m}$ pre-well-orders the set of degree-invariant functions that are increasing almost everywhere. If f has $⩽_{m}$ -rank α, then $f^{'}$ has $⩽_{m}$ -rank $α + 1$ , where $f^{'} (x) = f {(x)}^{'}$ for all x.

Roughly speaking, Martin’s Conjecture says that the only definable degree-invariant functions, up to $\equiv_{m}$ , are the constant functions, the identity function, and the iterates of the Turing jump.1

¹
Of course, the notion of “definable” is left vague in what I have written. More precisely, note that Martin’s Conjecture is stated under the hypothesis $AD$ . So Martin’s Conjecture will apply to Borel functions and to ever more capacious notions of “definable function” depending on the large cardinal axioms one assumes.

The optimistic hope in [5,9] was that an analogue of Martin’s Conjecture holds for axiomatic theories. Let’s fix a sound (i.e., true in the standard model) recursively extension T of elementary arithmetic. Say that a recursive function $g$ is extensional if for all φ and ψ: $\begin{matrix} T ⊢ φ \leftrightarrow ψ ⟹ T ⊢ g (φ) \leftrightarrow g (ψ) . \end{matrix}$ Shavrukov and Visser [7] proved that there is a recursive extensional density function on the Lindenbaum algebra of T, which precludes any direct analogue Martin’s Conjecture in this context. Nevertheless, positive results are available if we replace extensionality with the stronger condition of monotonicity. Say that a recursive function $g$ is monotone if for all φ and ψ: $\begin{matrix} T ⊢ φ \to ψ ⟹ T ⊢ g (φ) \to g (ψ) . \end{matrix}$ We will be exclusively concerned with recursive monotone $g$ in this paper. We will be primarily interested in truth-preserving operators with this property, such as the consistency operator.

Monotonicity is an analogue of the recursion-theoretic notion order-preserving; f is order-preserving if for all reals x and y: $\begin{matrix} x ⩽_{T} y ⟹ f (x) ⩽_{T} f (y) . \end{matrix}$ Note that Lutz and Siskind [4] proved Part 1 of Martin’s Conjecture for order-preserving functions and Slaman and Steel [8] proved Part 2 of Martin’s Conjecture for order-preserving Borel functions.

Gödel’s second incompleteness theorem tells us that the monotone function $\begin{matrix} φ \mapsto (φ \land {Con}_{T} (φ)) \end{matrix}$ produces a strictly stronger sentence whenever φ is true in the standard model. That is, the consistency operator acts like a jump on sound finite extensions of T. Just as with the Turing jump, there are iterates of the consistency operator into the effective transfinite.2

Unlike with Turing degrees, however, transfinite iterates of the consistency operator depend on the presentation of the base theory and the well-ordering.

Indeed, fixing a suitable elementary presentation ≺ of a well-ordering, we may define the iterates of the consistency operator using the fixed point lemma:

\begin{matrix} T ⊢ {Con}_{T}^{α} (φ) \leftrightarrow \forall β ≺ α {Con}_{T} (φ \land {Con}_{T}^{β} (φ)) .^{3} \end{matrix}

A definition of suitable ordinal notations is given in §2.2.

In [5,9] a number of results relating recursive monotone functions to iterates of the consistency operator are established. To state one such theorem, we introduce a definition. Note that whenever we mention sentences being “true,” we mean “true in the standard structure

N

.”

Definition 1.2.

A cone is any set $C$ such that, for some φ, $C = {ψ ∣ T ⊢ ψ \to φ}$ . A true cone is a cone that contains a true sentence.

Now here is a precise statement of a theorem from [9]:

Theorem 1.3.

Let $g$ be recursive and monotone such that, for some $k \in N$ , for all φ, $g (φ)$ is $Π_{k}$ . Then one of the following holds:

For all φ in a true cone, $T + φ ⊢ g (φ)$ .

For all φ in a true cone, $T + φ + g (φ) ⊢ {Con}_{T} (φ)$ .

Roughly, this says that any sufficiently nice operator must either be as weak as the identity operator in the limit or as strong as the consistency operator in the limit.

We had conjectured that this would be the first step of a classification of recursive monotone operators. Our hope was to prove—along the lines of Martin’s conjecture—that any function meeting the hypotheses of the theorem would either be as strong as ${Con}_{T}^{α}$ in the limit or as weak as ${Con}^{β}$ for some $β ≺ α$ in the limit. That is, we had hoped to prove a result of the following sort:4

⁴

Note that Hoped For Result 1.4 follows from Conjecture 1.8 in [9].

Hoped For Result 1.4.

Let $g$ be recursive and monotone such that, for some $k \in N$ , for all φ, $g (φ)$ is $Π_{k}$ . Then, for every $α ≻ 0$ , one of the following holds:

For all φ in a true cone, there is a $β ≺ α$ such that $T + φ + {Con}_{T}^{β} (φ) ⊢ g (φ)$ .

For all φ in a true cone, $T + φ + g (φ) ⊢ {Con}_{T}^{α} (φ)$ .

Of course, Theorem 1.3 already covers the $α = 1$ case of the hoped for result. Some results from [5] provided optimism for the $α ≻ 1$ cases. Before stating these results, let’s introduce some definitions. We say that cofinally many true sentences belong to a set $A$ if $A$ is cofinal in the ultrafilter of true sentences, i.e., for every true φ there is a true ψ such that $T ⊢ ψ \to φ$ and $ψ \in A$ . ${[φ]}_{T}$ is the equivalence class of φ modulo T-provable equivalence. That is: $\begin{matrix} {[φ]}_{T} = {ψ ∣ T ⊢ φ \leftrightarrow ψ} . \end{matrix}$ If $T ⊢ φ \to ψ$ , let’s say that φ T-provably implies ψ. If φ T-provably implies ψ and ψ does not T-provably imply φ then we say that φ strictly T-provably implies ψ. Here are the positive results from [5]:

Theorem 1.5.

Let $g$ be recursive and monotone. Suppose that for all φ both of the following hold:

$φ \land {Con}_{T}^{α} (φ)$ T-provably implies $g (φ)$ .

If ${[g (φ)]}_{T} \neq {[⊥]}_{T}$ , then for all $β ≺ α$ , $g (φ)$ strictly T-provably implies ${Con}_{T}^{β} (φ)$ .

Then for cofinally many true φ,

{[g (φ)]}_{T} = {[φ \land {Con}_{T}^{α} (φ)]}_{T}

This result says that if the range of a recursive monotone $g$ is sufficiently constrained, then $g$ must coincide cofinally with an iterate of the consistency operator. In particular, if $g$ is everywhere as weak as ${Con}_{T}^{α}$ but everywhere strictly stronger than ${Con}_{T}^{β}$ for all $β ≺ α$ , then $g$ must coincide cofinally with ${Con}_{T}^{α}$ . As a corollary we infer that:

Corollary 1.6.

There is no recursive monotone $g$ such that for all φ such that ${[φ \land {Con}_{T}^{α} (φ)]}_{T} \neq {[⊥]}_{T}$ , both of the following hold:

$φ \land {Con}_{T}^{α} (φ)$ strictly T-provably implies $g (φ)$ .

For all $β ≺ α$ , $g (φ)$ strictly T-provably implies $φ \land {Con}^{β} (φ)$ .

This is just to say that there is no recursive monotone function of strictly intermediate strength, i.e., a function that is everywhere strictly stronger than ${Con}^{β}$ for all $β ≺ α$ yet strictly weaker than ${Con}_{T}^{α}$ . This rules out the most obvious sort of counter-example one might expect to Hoped For Result 1.4.

Nevertheless, in this paper we will see that this hoped for result fails. In fact, it fails already at the very next step, i.e., $α = 2$ . For any $α ≻ 0$ , we can construct a function that is cofinally as strong than ${Con}_{T}^{α}$ yet cofinally as weak as ${Con}_{T}$ :

Theorem 1.7.

For every $α ≻ 0$ , there is a recursive monotone $g$ such that, for all φ, $g (φ)$ is $Π_{1}$ , and both of the following hold:

For cofinally many true φ: $\begin{matrix} {[φ \land g (φ)]}_{T} = {[φ \land {Con}_{T}^{α} (φ)]}_{T} . \end{matrix}$

For cofinally many true φ: $\begin{matrix} {[φ \land {Con}_{T} (φ)]}_{T} = {[φ \land g (φ)]}_{T} . \end{matrix}$

This the most dramatic possible failure of the Hoped For Result 1.4 that is consistent with Theorem 1.3.

Of course, this result is somewhat negative considering the context in which it is proved. That is, it shows that the hoped for analogue of Martin’s Conjecture fails. Yet this result also highlights something rather surprising about the consistency operator. Indeed, the consistency operator stands apart from its iterates with respect to its inevitability.

Here is our plan for the rest of the paper. In §2, we will cover some preliminaries. In §3 we will cover the main technical aspect of our result, which is the construction of pathological recursively enumerable sets. In particular, these sets contain cofinally many true sentences but do not contain any true cones. In §4 we will present the proof of the main theorem. In §5 we will conclude with some observations; in particular, we will discuss the relationship between the negative Theorem 1.7 and the positive Theorem 1.3.

2. Preliminaries

In this section we will fix some notation and cover some preliminaries. The main goal of this section is to introduce the iterations of the consistency operator (relative to a fixed ordinal notation system) and prove that they are monotone.

2.1. Base theory

The theories we will be interested in are extensions of elementary arithmetic or $EA$ . The signature of $EA$ is the usual signature of $PA$ with a function symbol for $2^{x}$ . $EA$ has as axioms the ${PA}^{-}$ axioms plus induction for all formulas bounded in an exponential term. $EA$ is just strong enough to carry out the standard arithmetization of syntax in the usual manner. For details about $EA$ see [3].

One of the crucial features of $EA$ is $Σ_{1}$ -completeness, which we will use. This is just to say that for any T extending $EA$ and any $Σ_{1}$ sentence φ: $\begin{matrix} N ⊨ φ \Rightarrow T ⊢ φ . \end{matrix}$

From here on out we will fix a sound, elementarily axiomatized extension T of $EA$ . By saying that T is sound we mean that for all φ: $\begin{matrix} T ⊢ φ \Rightarrow N ⊨ φ . \end{matrix}$ Of course, this means that for every $Σ_{1}$ sentence φ we have: $\begin{matrix} N ⊨ φ \Leftrightarrow T ⊢ φ . \end{matrix}$

2.2. Ordinal notations

There are many ways of reasoning with ordinal notations in elementary arithmetic. We will not need to work with ordinal notation systems in much detail; much of what we do can be done given any “reasonable” choice. For present purposes, it is enough to briefly mention a few properties our ordinal notations will have. We will call our presentations suitable presentations.

Every suitable ordinal notation system is a pair $(D, ≺)$ of elementary formulas, such that:

the relation ≺ well-orders D in the standard model of arithmetic;

D is provably closed under successor;

$EA$ proves that ≺ linearly orders the elements satisfying D;5

⁵
The referee has pointed out that provable linearity is not required; rather, we only need that the relation is T-provably transitive and irreflexive.

the elementary formulas defining the initial ordinal 0 (which need not be the natural number 0), the set of limit ordinals, and the successor relation provably in $EA$ satisfy their corresponding first order definitions in terms of ≺.

2.3. Iterated consistency

Fixing a suitable elementary presentation ≺ of a well-ordering, we may define the iterates of the consistency operator using the fixed point lemma. Technically, we find a formula ${Con}^{⋆}$ in two variables: $\begin{matrix} T ⊢ {Con}^{⋆} (α, φ) \leftrightarrow \forall β ≺ α {Con}_{T} (φ \land {Con}_{T}^{⋆} (β, φ)) . \end{matrix}$ We write ${Con}_{T}^{α} (φ)$ as an abbreviation for ${Con}^{⋆} (α, φ)$ .

Remark 2.1.
We warn the reader that there is some discrepancy between our notation and the notation used by other authors. Our iteration scheme $\begin{matrix} {Con}_{T}^{α + 1} (φ) \equiv {Con}_{T} (φ \land {Con}_{T}^{α} (φ)) \end{matrix}$ is sometimes denoted $Con {(T + φ)}_{α}$ ; see, e.g., [1]. Moreover, the notation ${Con}_{T}^{α + 1} (φ)$ is sometimes used to denote ${Con}_{T} ({Con}_{T}^{α} (φ))$ ; see, e.g., [2].
Remark 2.2.
Note that all of the iterates of the consistency operator we have defined are sentences. This is appropriate for the current investigation since we are interested in functions on the Lindenbaum algebra of T. For instance, given our definition, for a limit λ, the sentence ${Con}_{T}^{λ} (φ)$ says $\forall α ≺ λ {Con}_{T} (φ \land {Con}_{T}^{α} (φ))$ . This clashes with the conventions adopted in some other papers, wherein ${Con}_{T}^{λ} (φ)$ is used as a name for the infinite set ${{Con}_{T}^{α} (φ) ∣ α ≺ λ}$ .

Note that:6
⁶
Here we use the fourth clause of our discussion of suitable ordinal notation systems.

$\begin{array}{l} T ⊢ {Con}_{T}^{0} (φ) \leftrightarrow ⊤ \\ T ⊢ {Con}_{T}^{1} (φ) \leftrightarrow {Con}_{T} (φ) \end{array}$ Since suitable ordinal notations define well-orderings over the standard structure $N$ , it follows by induction that for true φ, ${Con}_{T}^{α} (φ)$ is also true. Thus, for true φ the hierarchy ${Con}_{T}^{α} (φ)$ is proper by Gödel’s second incompleteness theorem.

It is immediate from the definition that, for any φ, the sentence ${Con}_{T}^{α} (φ)$ is $Π_{1}$ .

To verify that each function $φ \mapsto {Con}_{T}^{α} (φ)$ is monotone, we rely on Schmerl’s [6] technique of reflexive induction. Reflexive induction is a way of simulating large amounts of transfinite induction in weak theories. It is particularly useful for proving claims about iterated reflection principles. The technique is facilitated by the following theorem; we include the proof, since it is so short.
Theorem 2.1 (Schmerl).

Let T be a recursively axiomatized theory containing $EA$ . Suppose that $\begin{matrix} T ⊢ \forall α (\Pr_{T} (\forall β ≺ α A (β)) \to A (α)) . \end{matrix}$ Then $T ⊢ \forall α A (α)$ . 7

⁷
Schmerl proves his result using the base theory $PRA$ . Beklemishev has shown that $EA$ suffices.

Proof.

Suppose that $T ⊢ \forall α (\Pr_{T} (\forall β ≺ α A (β)) \to A (α))$ . We infer that: $\begin{array}{l} T ⊢ \Pr_{T} (\forall α A (α)) & \to \forall α \Pr_{T} (\forall β ≺ α A (α)) \\ \to \forall α A (α) . \end{array}$

Löb’s Theorem then yields $T ⊢ \forall α A (α)$ . □

We now will verify that the function $φ \mapsto {Con}_{T}^{α} (φ)$ is monotone.

Lemma 2.2.

For any φ and ψ, if $T ⊢ φ \to ψ$ then $T ⊢ \forall α ({Con}_{T}^{α} (φ) \to {Con}_{T}^{α} (ψ))$ .

Proof.

Suppose that: $\begin{matrix} (1) & T ⊢ φ \to ψ . \end{matrix}$ We prove the claim by reflexive induction.

Reason in T: Let α be arbitrary. Assume the reflexive induction hypothesis: $\begin{matrix} (2) & \Pr_{T} (\forall β ≺ α ({Con}_{T}^{β} (φ) \to {Con}_{T}^{β} (ψ))) . \end{matrix}$

We reason as follows: $\begin{array}{l} {Con}_{T}^{α} (φ) & \to \forall β ≺ α {Con}_{T} (φ \land {Con}_{T}^{β} (φ)) by definition of {Con}_{T}^{α}; \\ \to \forall β ≺ α {Con}_{T} (ψ \land {Con}_{T}^{β} (φ)) by (1) and monotonicity of {Con}_{T}; \\ \to \forall β ≺ α {Con}_{T} (ψ \land {Con}_{T}^{β} (ψ)) by (2); \\ \to {Con}_{T}^{α} (ψ) by definition of {Con}_{T}^{α} . \end{array}$

Reasoning externally now: Let $A (γ)$ denote the claim: $\begin{matrix} {Con}_{T}^{γ} (φ) \to {Con}_{T}^{γ} (ψ) \end{matrix}$

We have shown that: $\begin{matrix} T ⊢ \forall α (\Pr_{T} (\forall β ≺ α A (β)) \to A (α)) . \end{matrix}$ By applying Lemma 2.1, we infer that $T ⊢ \forall α A (α)$ . □

We want to see not only that α-iterated consistency is monotone but also that it is provably monotone in T. We carry out this argument in two steps. Corollary 2.3.

$T ⊢ \forall φ \forall ψ (\Pr_{T} (φ \to ψ) \to \Pr_{T} (\forall α ({Con}_{T}^{α} (φ) \to {Con}_{T}^{α} (ψ))))$ .

Proof.

Since the proof of Lemma 2.2 can be carried out in T. □

Corollary 2.4.

$T ⊢ \forall φ \forall ψ (\Pr_{T} (φ \to ψ) \to \forall α ({Con}_{T}^{α} (φ) \to {Con}_{T}^{α} (ψ)))$ .

Proof.

Reason in T: Let φ and ψ be arbitrary. Suppose that: $\begin{matrix} (3) & T ⊢ φ \to ψ . \end{matrix}$ Let α be arbitrary. We reason as follows: $\begin{array}{l} {Con}_{T}^{α} (φ) & \to \forall β ≺ α {Con}_{T} (φ \land {Con}_{T}^{β} (φ)) by definition of {Con}_{T}^{α}; \\ \to \forall β ≺ α {Con}_{T} (ψ \land {Con}_{T}^{β} (φ)) by (3) and monotonicity of {Con}_{T}; \\ \to \forall β ≺ α {Con}_{T} (ψ \land {Con}_{T}^{β} (ψ)) by Corollary 2.3; \\ \to {Con}_{T}^{α} (ψ) by definition of {Con}_{T}^{α} . \end{array}$ This completes the proof of the corollary. □

3. Constructing pathological sets

The main technical aspect of our result is the construction of recursively enumerable sets that contain arbitrarily strong true sentences but that have wide gaps. In this section (and the next) we will work with a fixed suitable ordinal notation system ≺; see §2.2. We will define a set $A_{α}$ for each ordinal notation $α ⪰ 0$ ; the size of the gaps that we leave in the set will depend on α.

Similar constructions of recursively enumerable sets appear in [5,9]. The goal in the construction of these sets was merely to include arbitrarily strong true sentences and to omit arbitrarily strong true sentences. These sets did not leave large enough gaps for present purposes.

Here is how we define the set $A_{α}$ :

Let $φ_{0}, φ_{1}, \dots$ , be an effective Gödel numbering of arithmetical sentences. We describe the construction of $A_{α}$ in stages. During a stage n we may activate finitely many sentences; if ψ is some such sentence we say that ψ is active until ψ is deactivated at the later stage $n + 1$ .

Stage 0: Numerate ⊤ into $A_{α}$ ; activate $⊤ \land {Con}_{T}^{α + 1} (⊤)$ .

Stage $n + 1$ : There are finitely many active sentences. For each active sentence ψ, numerate $θ_{0} : = ψ \land φ_{n}$ and $θ_{1} : = ψ \land \neg φ_{n}$ into $A_{α}$ . Deactivate the sentence ψ and activate the sentences $θ_{0} \land {Con}_{T}^{α + 1} (θ_{0})$ and $θ_{1} \land {Con}_{T}^{α + 1} (θ_{1})$ .

It can be useful to visualize, along with the construction of $A_{α}$ , the construction of a tree that is binary branching. The tree has ⊤ as its root. The nodes in the tree are the sentences that are numerated into $A_{α}$ . Informally, the immediate descendants of any sentence ψ are the sentences that are numerated into $A_{α}$ immediately after ψ on account of ψ. More formally, for any sentence ψ numerated into $A_{α}$ at stage n, say that $ψ < ψ \land {Con}_{T}^{α + 1} (ψ) \land \pm φ_{n}$ ; the tree ordering is the transitive closure of the ordering < (note that this ordering is defined only on sentences numerated into $A_{α}$ ).

We will call the branches through this tree $A_{α}$ -branches. If φ and ψ share an $A_{α}$ -branch and φ was numerated into $A_{α}$ at stage n and ψ was numerated into $A_{α}$ at stage k where $k > n$ , we say that ψ is a descendant of φ. If $k = n + 1$ we say that ψ is an immediate descendant of φ.

Remark 3.1.
Note that for each ordinal notation α we get a set $A_{α}$ . The gaps that we leave in $A_{α}$ depend on α in the following sense: If φ is numerated into $A_{α}$ , then φ’s immediate descendants imply ${Con}_{T}^{α + 1} (φ)$ .

We can easily check some basic properties of this set $A_{α}$ .
Lemma 3.1.
$A_{α}$ is recursively enumerable.
Proof.
By construction. □
Remark 3.2.
An important consequence of the recursive enumerability of $A_{α}$ is that for any φ, if $φ \in A_{α}$ then $T ⊢ φ \in A_{α}$ . This follows since T is $Σ_{1}$ -complete.
Lemma 3.2.
$A_{α}$ contains arbitrarily strong true sentences.
Proof.
Let $φ_{n}$ be a true sentence. By induction it is easy to see that there is one true active sentence at each stage. Let’s say that going into stage $n + 1$ the true active sentence is ψ. Then at stage $n + 1$ we numerate $ψ \land φ_{n}$ into $A_{α}$ . □

$A_{α}$ -branches are sets of formulas, so reasoning about $A_{α}$ -branches might seem to require second-order expressive resources. Yet we have assumed only that T contains elementary arithmetic. Nevertheless, elementary arithmetic suffices for reasoning about the descendant relation. The claims we make about $A_{α}$ -branches in this paper could be translated into T-intelligible claims about the descendant relation. In the following lemma, for instance, we will prove a claim within T about $A_{α}$ -branches. All such claims can be translated into claims about the descendant relation, though we will not give an explicit translation here. Lemma 3.3.
Provably in T, if ψ and θ both belong to $A_{α}$ but do not share an $A_{α}$ -branch, then ψ and θ are jointly T-inconsistent.
Proof.
Reason in T: First observe that for any two sentences φ and ψ in the tree, if φ is a descendant of ψ then $T + φ ⊢ ψ$ .

Now let ψ and θ be arbitrary sentences in $A_{α}$ that do not share an $A_{α}$ -branch. Then there is some node $ζ_{0}$ that has immediate descendants $\begin{matrix} ζ_{1} : = ζ_{0} \land {Con}_{T}^{α + 1} (ζ_{0}) \land φ_{n} \end{matrix}$ and $\begin{matrix} ζ_{2} : = ζ_{0} \land {Con}_{T}^{α + 1} (ζ_{0}) \land \neg φ_{n} \end{matrix}$ such that $T + ψ ⊢ ζ_{1}$ and $T + θ ⊢ ζ_{2}$ . But $ζ_{1}$ and $ζ_{2}$ are jointly inconsistent whence ψ and θ are too. □
Lemma 3.4.
Provably in T, some T-refutable sentence θ belongs to $A_{α}$ .
Proof.
Let $T ⊢ \neg ψ$ . Note that ψ is $φ_{n}$ for some n. At stage $n + 1$ , we numerate a sentence θ that T-provably implies ψ into $A_{α}$ . Note that T proves both that $T ⊢ \neg θ$ and that $θ \in A_{α}$ , since T is $Σ_{1}$ -complete. □

4. The proof

Now we are ready to prove the main theorem. In this section we provide an example of a recursive monotone function that oscillates between behaving like ${Con}_{T}^{α}$ and behaving like ${Con}_{T}$ . Note that this refutes the optimistic Hoped For Result 1.4. Indeed, no function that oscillates cofinally between behaving like ${Con}_{T}^{α}$ and behaving like ${Con}_{T}$ can converge on either in the limit (assuming that $α ≻ 1$ ).

For convenience, we restate Theorem 1.7 here.

Theorem 4.1.
For every $α ≻ 0$ , there is a recursive monotone $g$ such that, for all φ, $g (φ)$ is $Π_{1}$ , and both of the following hold:
For cofinally many true φ: $\begin{matrix} {[φ \land g (φ)]}_{T} = {[φ \land {Con}_{T}^{α} (φ)]}_{T} . \end{matrix}$

For cofinally many true φ: $\begin{matrix} {[φ \land {Con}_{T} (φ)]}_{T} = {[φ \land g (φ)]}_{T} . \end{matrix}$

Proof.
Given $α ≻ 0$ , let: $\begin{matrix} g (φ) : = \forall θ \in A_{α} (\Pr_{T} (φ \to θ) \to {Con}_{T}^{α} (θ)) . \end{matrix}$

Note that $g$ is clearly recursive. It is routine to check that, for all φ, $g (φ) \in Π_{1}$ and (using Corollary 2.4) that $g$ is monotone.

Let $φ \in A_{α}$ . By $Σ_{1}$ -completeness of T: $\begin{matrix} (△) & T ⊢ φ \in A_{α} . \end{matrix}$

We reason as follows: $\begin{array}{l} T + g (φ) ⊢ \forall θ \in A_{α} (\Pr_{T} (φ \to θ) \to {Con}_{T}^{α} (θ)) by choice of g; \\ T + g (φ) ⊢ \Pr_{T} (φ \to φ) \to {Con}_{T}^{α} (φ) by (△); \\ T + g (φ) ⊢ {Con}_{T}^{α} (φ) by Σ_{1} -completeness . \end{array}$

On the other hand, the monotonicity of ${Con}_{T}^{α}$ is provable in T (see Corollary 2.4). Whence: $\begin{array}{l} T + {Con}_{T}^{α} (φ) ⊢ \forall θ (\Pr_{T} (φ \to θ) \to {Con}_{T}^{α} (θ)); \\ T + {Con}_{T}^{α} (φ) ⊢ g (φ) . \end{array}$

Since cofinally many true sentences belong to $A_{α}$ , this already takes care of (1).

Now we pick some true $ψ \in A_{α}$ . We consider the sentence $φ : = ψ \land {Con}_{T}^{α} (ψ)$ . Claim 4.2.
T proves that if φ is consistent, then ψ is the strongest sentence in $A_{α}$ that φ T-provably implies.

To see that the claim is true, we reason in T: Suppose that φ is consistent. Note that φ T-provably implies ψ. Note, moreover, that ψ is inconsistent with every sentence in $A_{α}$ with which ψ does not share an $A_{α}$ -branch by Lemma 3.3. So, since φ is consistent, the only $A_{α}$ sentences that φ T-provably implies must share an $A_{α}$ -branch with ψ. By construction of $A_{α}$ , every descendant of ψ T-provably implies ${Con}_{T}^{α + 1} (ψ)$ . But, since φ is consistent, φ does not T-provably imply ${Con}_{T}^{α + 1} (ψ)$ by Gödel’s second incompleteness theorem. This delivers the claim.

We then reason as follows: $\begin{array}{l} T + φ + {Con}_{T} (φ) ⊢ \forall θ \in A_{α} (\Pr_{T} (φ \to θ) \to \Pr_{T} (ψ \to θ)) by the claim; \\ T + φ + {Con}_{T} (φ) ⊢ \forall θ \in A_{α} (\Pr_{T} (φ \to θ) \to ({Con}_{T}^{α} (ψ) \to {Con}_{T}^{α} (θ))) by Corollary 2.4; \\ T + φ + {Con}_{T} (φ) ⊢ \forall θ \in A_{α} (\Pr_{T} (φ \to θ) \to {Con}_{T}^{α} (θ)) since T + φ ⊢ {Con}_{T}^{α} (ψ); \\ T + φ + {Con}_{T} (φ) ⊢ g (φ) by the definition of g . \end{array}$

For the converse: $\begin{array}{l} T ⊢ \exists θ \in A_{α} \neg {Con}_{T} (θ) by Lemma 3.4; \\ T + \neg {Con}_{T} (φ) ⊢ \exists θ \in A_{α} (\Pr_{T} (φ \to θ) \land \neg {Con}_{T}^{α} (θ)); \\ T + \neg {Con}_{T} (φ) ⊢ \neg g (φ) by the definition of g . \end{array}$

This takes care of (2). □

5. Observations

Theorem 1.7 refutes Hoped For Result 1.4. Yet what happens in the case $α = 0$ ? That is, why can’t the proof of Theorem 1.7 be adapted to the $α = 0$ case, thereby contradicting Theorem 1.3? The answer exhibits an important feature that the notion of consistency does not share with its iterates.

Recall that we construct $A_{α}$ so that whenever φ is numerated into $A_{α}$ , then φ’s immediate descendants T-provably imply ${Con}_{T}^{α + 1} (φ)$ . In particular, whenever φ is numerated into $A_{0}$ , then φ’s immediate descendants T-provably imply ${Con}_{T} (φ)$ . Let’s consider the function: $\begin{matrix} g_{0} (φ) : = \forall θ \in A_{0} (\Pr_{T} (φ \to θ) \to {Con}_{T} (θ)) . \end{matrix}$

Surprisingly, $g_{0}$ is actually equivalent to the consistency operator. That is:

Proposition 5.1.

For every φ, $T ⊢ {Con}_{T} (φ) \leftrightarrow g_{0} (φ)$ .

Proof.

Left to right: $\begin{array}{l} T ⊢ {Con}_{T} (φ) & \to \forall θ (\Pr_{T} (φ \to θ) \to {Con}_{T} (θ)); \\ \to g_{0} (φ) . \end{array}$

Right to left: $\begin{array}{l} T ⊢ \neg {Con}_{T} (φ) & \to \exists θ \in A_{0} (\Pr_{T} (φ \to θ) \land \neg {Con}_{T} (θ)) by Lemma 3.4; \\ \to \neg g_{0} (φ) . \end{array}$ This completes the proof. □

Note the appeal to Lemma 3.4. Here we use that $A_{0}$ is guaranteed to contain an inconsistent sentence; the important point is that if φ is T-inconsistent, then some sentence that φ T-provably implies belongs to $A_{0}$ . Indeed, the fact that all T-inconsistent sentences T-provably imply each other is used in the proof of the positive Theorem 1.3 (see the proof of Theorem 2.4 Case 2 in [9]). By contrast, if we merely knew $\neg {Con}_{T}^{α + 1} (φ)$ , we would not be able to conclude that some T-consequence of φ belongs to $A_{α}$ . Nor for any of the other iterates of the consistency operator.

There are ways of modifying $g_{0}$ to avoid Proposition 5.1. Rather than quantifying over the T-implications of φ in $A_{0}$ and saying that they are all consistent, we can let $g (φ)$ merely assert the conjunction according to which each is consistent. That is: $\begin{matrix} g_{0}^{⋆} (φ) : = \{\begin{matrix} ⋀ {{Con}_{T} (ζ) ∣ ζ \in A_{0} and T + φ ⊢ ζ} & if {[φ]}_{T} \neq {[⊥]}_{T}, \\ ⊥ & otherwise \end{matrix} \end{matrix}$

In previous work we have shown that $g_{0}^{⋆}$ oscillates between behaving like the identity and the consistency operator (see Theorem 3.7 in [9]). However, computing the function $g_{0}^{⋆}$ requires access to the oracle $0^{'}$ . Indeed, to calculate $g_{0}^{⋆} (φ)$ we must know whether ${[φ]}_{T} \neq {[⊥]}_{T}$ , which requires $0^{'}$ . So $g_{0}^{⋆}$ demonstrates that recursiveness is also a necessary condition in Theorem 1.3; it cannot be weakened to limit-recursiveness.

Footnotes

Acknowledgements

Thanks to the referee for extensive and helpful suggestions and corrections.

References

Beklemishev, Iterated local reflection versus iterated consistency, Annals of Pure and Applied Logic 75(1–2) (1995), 25–48. doi:10.1016/0168-0072(95)00007-4.

L.D.

Beklemishev, Provability logics for natural Turing progressions of arithmetical theories, Studia Logica (1991), 107–128. doi:10.1007/BF00370390.

L.D.

Beklemishev, Reflection principles and provability algebras in formal arithmetic, Russian Mathematical Surveys 60(2) (2005), 197–268. doi:10.1070/RM2005v060n02ABEH000823.

Lutz, Results on Martin’s Conjecture, Bulletin of Symbolic Logic 27(2) (2021), 219–220. doi:10.1017/bsl.2021.27.

Montalbán and

Walsh, On the inevitability of the consistency operator, The Journal of Symbolic Logic 84(1) (2019), 205–225. doi:10.1017/jsl.2018.65.

R.U.

Schmerl, A fine structure generated by reflection formulas over primitive recursive arithmetic, in: In Studies in Logic and the Foundations of Mathematics, Vol. 97, Elsevier, 1979, pp. 335–350.

V.Y.

Shavrukov and

Visser, Uniform density in Lindenbaum algebras, Notre Dame Journal of Formal Logic 55(4) (2014), 569–582. doi:10.1215/00294527-2798754.

T.A.

Slaman and

J.R.

Steel, Definable functions on degrees, in: Cabal Seminar 81–85, Springer, 1988, pp. 37–55. doi:10.1007/BFb0084969.

Walsh, A note on the consistency operator, Proceedings of the American Mathematical Society 148(6) (2020), 2645–2654. doi:10.1090/proc/14948.

Evitable iterates of the consistency operator

Abstract

Keywords

1. Introduction

Conjecture 1.1 (Martin).

2.1. Base theory

2.2. Ordinal notations

5 The referee has pointed out that provable linearity is not required; rather, we only need that the relation is T-provably transitive and irreflexive.

7 Schmerl proves his result using the base theory PRA . Beklemishev has shown that EA suffices.

Footnotes

Acknowledgements

References

⁵
The referee has pointed out that provable linearity is not required; rather, we only need that the relation is T-provably transitive and irreflexive.

⁷
Schmerl proves his result using the base theory $PRA$ . Beklemishev has shown that $EA$ suffices.