On the inevitability of the consistency operator
Antonio Montalbán James Walsh


Two Dimensional Discrete Dynamics of Integral Value Transformations
    Pabitra Pal Choudhury
    December 30, 2023
===================================================================




We examine recursive monotonic functions on the Lindenbaum algebra of 𝖤𝖠. We prove that no such function sends every consistent φ to a sentence with deductive strength strictly between φ and (φ∧𝖢𝗈𝗇(φ)). We generalize this result to iterates of consistency into the effective transfinite. We then prove that for any recursive monotonic function f, if there is an iterate of 𝖢𝗈𝗇 that bounds f everywhere, then f must be somewhere equal to an iterate of 𝖢𝗈𝗇.




§ INTRODUCTION


It is a well-known empirical phenomenon that natural axiomatic theories are well-ordered by their consistency strength. However, without a precise mathematical definition of “natural,” it is difficult to explain this observation in a strictly mathematical way. One expression of this phenomenon comes from ordinal analysis, a research program whereby recursive ordinals are assigned to theories as a measurement of their consistency strength. One method for calculating the proof-theoretic ordinal of a theory T involves demonstrating that T can be approximated over a weak base theory by a class of formulas that are well understood. In particular, the Π^0_1 fragments of natural theories are often proof-theoretically equivalent to iterated consistency statements over a weak base theory, making these theories amenable to ordinal analysis. For discussion, see, e.g., Beklemishev <cit.> and Joosten <cit.>. 

Why are the Π^0_1 fragments of natural theories proof-theoretically equivalent to iterated consistency statements? Our approach to this question is inspired by Martin's approach to another famous question from mathematical logic: why are natural Turing degrees well-ordered by Turing reducibility? Martin conjectured that (i) the non-constant degree invariant functions meeting a certain simplicity condition (f∈ L(ℝ))[Martin's Conjecture is stated under the hypothesis 𝖹𝖥+𝖠𝖣+𝖣𝖢, which is satisfied by L(ℝ) assuming that there are ω many Woodin cardinals with a measurable above them all.] are pre-well-ordered by the relation “f(a)≤_Tg(a) on a cone in the Turing degrees” and (ii) the successor for this well-ordering is induced by the Turing jump. Martin's conjecture is meant to capture the idea that the Turing jump and its iterates into the transfinite are the only natural non-trivial degree invariant functions.

In this paper we investigate analogous hypotheses concerning jumps on consistent axiomatic theories, namely, consistency statements. We fix elementary arithmetic 𝖤𝖠 as our base theory. 𝖤𝖠 is a subsystem of 𝖯𝖠 that is often used as a base theory in ordinal analysis and in which standard approaches to arithmetization of syntax can be carried out without substantial changes; see <cit.> for details. We write [φ] to denote the equivalence class of φ modulo 𝖤𝖠-provable equivalence. We write φ⊢ψ if 𝖤𝖠⊢φ→ψ and say that φ implies ψ. If φ⊢ψ but ψ⊬φ we say that φ strictly implies ψ. The Lindenbaum algebra of 𝖤𝖠 is the set of equivalence classes of sentences ordered by ⊢. We focus on recursive functions f that are monotonic, i.e.,

    if φ⊢ψ, then f(φ)⊢ f(ψ).
 
We note that (i) a function f is monotonic just in case f preserves implication over 𝖤𝖠 and (ii) all monotonic functions induce functions on the Lindenbaum algebra of 𝖤𝖠. We adopt the convention that all functions named “f” in this paper are recursive.

Our goal is to demonstrate that φ↦(φ∧𝖢𝗈𝗇(φ)) and its iterates into the transfinite are canonical among monotonic functions. Our first theorem to this end is the following.



Let f be monotonic. Suppose that for all consistent φ,

(i) φ∧𝖢𝗈𝗇(φ) implies f(φ) and

(ii) f(φ) strictly implies φ. 

Then for every true φ, there is a true ψ such that ψ⊢φ and [f(ψ)] = [ψ∧𝖢𝗈𝗇(ψ)].


 
There is no monotonic function f such that for all consistent φ, 

(i) φ∧𝖢𝗈𝗇(φ) strictly implies f(φ) and 

(ii) f(φ) strictly implies φ.


We note that this result depends essentially on the condition of monotonicity. Shavrukov and Visser <cit.> studied recursive functions f that are extensional over the Lindenbaum algebra of 𝖯𝖠, i.e., 

    if 𝖯𝖠⊢(φ↔ψ) , then 𝖯𝖠⊢(f(φ)↔ f(ψ)),
 
and proved the following theorem. 


(Shavrukov–Visser)
There is a recursive extensional function f such that for all consistent φ, 

(i) φ∧𝖢𝗈𝗇(φ) strictly implies f(φ) and 

(ii) f(φ) strictly implies φ.

In particular, Shavrukov and Visser proved that for any consistent φ, the sentence

    φ^⋆:=φ∧∀ x(𝖢𝗈𝗇(IΣ_x+φ)→𝖢𝗈𝗇(IΣ_x+φ+𝖢𝗈𝗇(IΣ_x+φ)))

has deductive strength strictly between φ and φ∧𝖢𝗈𝗇(φ), and that the map φ↦φ^⋆ is extensional. By a theorem of Kripke and Pour-El <cit.>, the Lindenbaum algebras of 𝖯𝖠 and 𝖤𝖠 are effectively isomorphic, whence Theorem <ref> also applies to 𝖤𝖠. Thus, Corollary <ref> cannot be strengthened by weakening the hypothesis of monotonicity to the hypothesis of extensionality.

We also note that Friedman, Rathjen, and Weiermann <cit.> introduced a notion of slow consistency with which they produced a Π^0_1 sentence 𝖲𝗅𝗈𝗐𝖢𝗈𝗇(𝖯𝖠) with deductive strength strictly between 𝖯𝖠 and 𝖯𝖠+𝖢𝗈𝗇(𝖯𝖠). In general, the statement 𝖲𝗅𝗈𝗐𝖢𝗈𝗇(φ) has the form

    ∀ x (F_ϵ_0(x)↓→𝖢𝗈𝗇(IΣ_x+φ))

where F_ϵ_0 is a standard representation of a recursive function that is not provably total in 𝖯𝖠. This is not in conflict with Corollary <ref>, however, since φ∧𝖢𝗈𝗇(φ) and φ∧𝖲𝗅𝗈𝗐𝖢𝗈𝗇(φ) are provably equivalent for all φ such that φ⊢∀ x F_ϵ_0(x)↓. On the other hand, changing the definition of the 𝖲𝗅𝗈𝗐𝖢𝗈𝗇(φ) so that the function in the antecedent varies with the input φ results in a map that is not monotonic.

Theorem <ref> generalizes to the iterates of 𝖢𝗈𝗇 into the effective transfinite. For an elementary presentation α of a recursive well-ordering (see Definition <ref>) and a sentence φ, we define sentences 𝖢𝗈𝗇^β(φ) for every β<α.

𝖢𝗈𝗇^0(φ):=   ⊤

𝖢𝗈𝗇^β+1(φ):=   𝖢𝗈𝗇(φ∧𝖢𝗈𝗇^β(φ))

𝖢𝗈𝗇^λ(φ):=   ∀β<λ(𝖢𝗈𝗇^β(φ))

For a precise definition using Gödel's fixed point lemma, see Definition <ref>. Note that for every φ, [𝖢𝗈𝗇^1(φ)]=[𝖢𝗈𝗇(φ)]. 


We warn the reader that there is some discrepancy between our notation and the notation used by other authors. Our iteration scheme 𝖢𝗈𝗇^α+1(φ)≡𝖢𝗈𝗇(φ∧𝖢𝗈𝗇^α(φ)) is sometimes denoted 𝖢𝗈𝗇((𝖤𝖠+φ)_α), e.g., <cit.>. Moreoever, the notation 𝖢𝗈𝗇^α+1(φ) is sometimes used to denote 𝖢𝗈𝗇(𝖢𝗈𝗇^α(φ)), e.g., <cit.>.


With each predicate 𝖢𝗈𝗇^α we associate a function 

    φ↦(φ∧𝖢𝗈𝗇^α(φ)).
 

Theorem <ref> then generalizes into the effective transfinite as follows.


Let f be monotonic. Suppose that for all φ, 

(i) φ∧𝖢𝗈𝗇^α(φ) implies f(φ),

(ii) if [f(φ)]≠[], then f(φ) strictly implies φ∧𝖢𝗈𝗇^β(φ) for all β<α. 

Then for every true φ, there is a true ψ such that ψ⊢φ and [f(ψ)] = [ψ∧𝖢𝗈𝗇^α(ψ)].



There is no monotonic f such that for all φ, if [φ∧𝖢𝗈𝗇^α(φ)]≠[], then both

(i) φ∧𝖢𝗈𝗇^α(φ) strictly implies f(φ) and

(ii) f(φ) strictly implies φ∧𝖢𝗈𝗇^β(φ) for all β<α.


Thus, if the range of a monotonic function f is sufficiently constrained, then for some φ and some α, 

    [f(φ)]=[φ∧𝖢𝗈𝗇^α(φ)]≠[].

This property still holds even when these constraints on the range of f are relaxed considerably. More precisely, if a monotonic function is everywhere bounded by a finite iterate of 𝖢𝗈𝗇, then it must be somewhere equivalent to an iterate of 𝖢𝗈𝗇.


Let n∈ℕ. Let f be a monotonic function such that for every φ, 

(i) φ∧𝖢𝗈𝗇^n(φ) implies f(φ) and 

(ii) f(φ) implies φ. 

Then for some φ and some k≤ n, [f(φ)]=[φ∧𝖢𝗈𝗇^k(φ)]≠[].


To generalize this result into the effective transfinite, we focus on a particular class of monotonic functions that we call Π^0_1. 


A function f is Π^0_1 if f(φ)∈Π^0_1 for all φ.


Our main theorem is the following: if a monotonic function is everywhere bounded by a transfinite iterate of 𝖢𝗈𝗇, then it must be somewhere equivalent to an iterate of 𝖢𝗈𝗇. This to say that the iterates of the consistency operator are inevitable; no monotonic function that is everywhere bounded by some iterate of 𝖢𝗈𝗇 can avoid all of the iterates of 𝖢𝗈𝗇.



Let φ↦ f(φ) be a monotonic Π^0_1 function Then either 

(i) for some β≤α and some φ, [φ∧ f(φ)]=[φ∧𝖢𝗈𝗇^β(φ)]≠[] or

(ii) for some φ, (φ∧𝖢𝗈𝗇^α(φ))⊬ f(φ).


The main theorem bears a striking similarity to the following theorem of Slaman and Steel <cit.>.



(Slaman–Steel) Suppose f: 2^ω→2^ω is Borel, order-preserving with respect to ≤_T, and increasing on a cone. Then for any α<ω_1 either

(i) for some β≤α, f(x)≡_Tx^(β) cofinally or

(ii) (x^(α)<_Tf(x)) cofinally.


There are two notable disanalogies between Theorem <ref> and Theorem <ref>. First, Theorem <ref> guarantees only that sufficiently constrained functions are somewhere equivalent to an iterate of 𝖢𝗈𝗇, whereas Theorem <ref> guarantees cofinal equivalence with an iterate of the Turing jump. Second, by assuming 𝖠𝖣, Slaman and Steel inferred that this behavior happens not only cofinally but also on a cone in the Turing degrees. There is no obvious analogue of 𝖠𝖣 from which one can infer that if cofinally many Lindenbaum degrees have a property then every element in some non-trivial ideal of Lindenbaum degrees has that property.

We then turn our attention to a generalization of consistency, namely, 1-consistency. Recall that a theory T is 1-consistent if T is consistent with the true Π^0_1 theory of arithmetic. Just as the Π^0_1 fragments of natural theories are often proof-theoretically equivalent to iterated consistency statements over a weak base theory, the Π^0_2 fragments of natural theories are often proof-theoretically equivalent to iterated 1-consistency statements over a weak base theory

Conservativity theorems relating 1-consistency and iterated consistency play an important role in the proof-theoretic analysis of arithmetic theories. For instance, it is a consequence of Beklemshev's reduction principle <cit.> that for any Π^0_1 φ, 

    𝖤𝖠 + 1𝖢𝗈𝗇(𝖤𝖠) ⊢φ if and only if 𝖤𝖠 + {𝖢𝗈𝗇^k(𝖤𝖠):k<ω}⊢φ.
 
This fact plays an integral role in Beklemishev's <cit.> consistency proof of 𝖯𝖠. We show that this conservativity result is drastically violated in the limit. For functions f and g, we say that f majorizes g if there is a consistent φ such that for all ψ, if ψ⊢φ then f(ψ)⊢ g(ψ); if in addition φ is true then we say that f majorizes g on a true ideal.


For any elementary presentation α of a recursive well-ordering, 1𝖢𝗈𝗇 majorizes 𝖢𝗈𝗇^α on a true ideal.


It is tempting to conjecture on the basis of this result that 1𝖢𝗈𝗇 is the weakest monotonic function majorizing each 𝖢𝗈𝗇^α for α a recursive well-ordering. We prove that this is not the case.


There are infinitely many monotonic functions f such that for every recursive ordinal α, there is an elementary presentation a of α such that f majorizes 𝖢𝗈𝗇^a on a true ideal but also 1𝖢𝗈𝗇 majorizes f on a true ideal.


Theorem <ref> demonstrates that for any monotonic f with a sufficiently constrained range, f must agree cofinally with 𝖢𝗈𝗇. We would like to strengthen cofinally to on a true ideal. One strategy for establishing this claim would be to show that every set that is closed under 𝖤𝖠 provable equivalence and that contains cofinally many true sentences also contains every sentence in some true ideal. We show that this strategy fails.


There is a recursively enumerable set 𝒜 that contains arbitrarily strong true sentences and that is closed under 𝖤𝖠 provable equivalence but does not contain any true ideals.


It is not clear whether Theorem <ref> can be strengthened in the desired manner.



§ NO MONOTONIC FUNCTION IS STRICTLY BETWEEN THE IDENTITY AND 𝖢𝗈𝗇


In this section we prove that no monotonic function sends every consistent φ to a sentence with deductive strength strictly between φ and (φ∧𝖢𝗈𝗇(φ)). Most of the work is contained in the proof of the following lemma.



Let f be a monotonic function such that for all consistent φ, f(φ) strictly implies φ. Then for every true sentence φ there is a true sentence θ such that θ⊢φ and f(θ)⊢ (θ∧𝖢𝗈𝗇(θ)).



Let f be as in the statement of the theorem. By assumption the following statement is true. 

    χ:=∀ζ(𝖢𝗈𝗇(ζ)→𝖢𝗈𝗇(ζ∧ f(ζ)))
 
Let φ be a true sentence. Then the sentence ψ:=φ∧χ is true. Let 
    θ:=(ψ∧ (f(ψ)→𝖢𝗈𝗇(ψ))).
 Note that θ⊢φ.


f(θ)⊢ (θ∧ f(ψ)).


Clearly θ⊢ψ. So f(θ)⊢ f(ψ) since f is monotonic. Also f(θ)⊢θ by assumption.


(θ∧ f(ψ))⊢ (ψ∧𝖢𝗈𝗇(ψ)).


Immediate from the definition of θ.


(ψ∧𝖢𝗈𝗇(ψ))⊢ (θ∧𝖢𝗈𝗇(θ)).


Clearly (ψ∧𝖢𝗈𝗇(ψ))⊢θ. It suffices to show that 
    (ψ∧𝖢𝗈𝗇(ψ))⊢𝖢𝗈𝗇(θ).
 We reason as follows.

(ψ∧𝖢𝗈𝗇(ψ))   ⊢∀ζ(𝖢𝗈𝗇(ζ)→𝖢𝗈𝗇(ζ∧f(ζ)))  by choice of ψ.

   ⊢𝖢𝗈𝗇(ψ)→𝖢𝗈𝗇(ψ∧f(ψ))  by instantiation.

    ⊢𝖢𝗈𝗇(ψ∧f(ψ))  by logic. 

    ⊢𝖢𝗈𝗇(θ)  by the definition of θ.
 
It is immediate from the preceding claims that f(θ)⊢ (θ∧𝖢𝗈𝗇(θ)).


A number of results follow immediately from the lemma.



Let f be monotonic. Suppose that for all consistent φ,

(i) φ∧𝖢𝗈𝗇(φ) implies f(φ) and

(ii) f(φ) strictly implies φ. 

Then for every true φ, there is a true ψ such that ψ⊢φ and [f(ψ)] = [ψ∧𝖢𝗈𝗇(ψ)].



By the lemma, for every true φ there is a true ψ such that ψ⊢φ and f(ψ)⊢ (ψ∧𝖢𝗈𝗇(ψ)). Since we are assuming that (ψ∧𝖢𝗈𝗇(ψ))⊢ f(ψ), it follows that [f(ψ)]=[ψ∧𝖢𝗈𝗇(ψ)].


We note that this theorem applies to a number of previously studied operators. For instance, the theorem applies to the notion of cut-free consistency, i.e., consistency with respect to cut-free proofs. 𝖤𝖠 does not prove the cut-elimination theorem, which is equivalent to the totality of super-exponentiation (over 𝖤𝖠), and does not prove the equivalence of cut-free consistency and consistency. Another such operator is the Friedman-Rathjen-Weiermann slow consistency operator discussed in §1. Theorem <ref> implies that these operators exhibit the same behavior as the consistency operator “in the limit.” Indeed, for any φ such that φ proves the cut-elimination theorem, φ∧𝖢𝗈𝗇(φ) and φ∧𝖢𝗈𝗇_𝖢𝖥(φ) are 𝖤𝖠-provably equivalent. Likewise, for any φ that proves the totality of F_ϵ_0, φ∧𝖢𝗈𝗇(φ) and φ∧𝖲𝗅𝗈𝗐𝖢𝗈𝗇(φ) are 𝖤𝖠-provably equivalent.

As a corollary of Theorem <ref> we note that no monotonic function reliably produces sentences strictly between those produced by the identity and by 𝖢𝗈𝗇.


There is no monotonic function f such that for all consistent φ, 

(i) φ∧𝖢𝗈𝗇(φ) strictly implies f(φ) and 

(ii) f(φ) strictly implies φ.


Shavrukov and Visser <cit.> studied functions over Lindenbaum algberas and discovered a recursive extensional uniform density function g for the Lindenbaum algebra of 𝖤𝖠, i.e., (i) for any φ and ψ such that ψ strictly implies φ, g(⟨φ,ψ⟩) is a sentence with deductive strength strictly between φ and ψ and (ii) if 𝖤𝖠⊢(φ↔ψ) then, for any θ, [g(⟨φ,θ⟩)]=[g(⟨ψ,θ⟩)] and [g(⟨θ,φ⟩)]=[g(⟨θ,ψ⟩)]. They asked whether this result could be strengthened by exhibiting a recursive uniform density function that is monotonic in both its coordinates. As a corollary of our theorem we answer their question negatively.


There is no monotonic uniform density function for the Lindenbaum algebra of 𝖤𝖠.



Suppose there were such a function g over the Lindenbaum algebra of 𝖤𝖠. Then given any input of the form ⟨φ,(φ∧𝖢𝗈𝗇(φ))⟩, g would produce a sentence with deductive strength strictly between φ and (φ∧𝖢𝗈𝗇(φ)). We then note that f:φ↦ g(⟨φ,(φ∧𝖢𝗈𝗇(φ))⟩) is monotonic, but that for every consistent φ, φ∧𝖢𝗈𝗇(φ) strictly implies f(φ) and f(φ) strictly implies φ, contradicting the previous theorem.


Our negative answer to the question raised by Shavrukov and Visser makes use of a Π^0_2 sentence ∀ζ(𝖢𝗈𝗇(ζ)→𝖢𝗈𝗇(ζ∧ f(ζ))). Shavrukov and Visser raised the following question in private communication.


Is there a recursive uniform density function for the lattice of Π^0_1 sentences over 𝖤𝖠 that is monotonic in both its coordinates?




It is clear from the proof of the lemma that any monotonic f meeting the hypotheses of Theorem <ref> is not only cofinally equivalent to 𝖢𝗈𝗇; for every true ψ that implies 
    χ:=∀ζ(𝖢𝗈𝗇(ζ)→𝖢𝗈𝗇(ζ∧ f(ζ))),
 there is a true θ such that θ⊢ψ and [ψ∧𝖢𝗈𝗇(ψ)]=[θ∧𝖢𝗈𝗇(θ)]=[f(θ)].


This observation points the way toward a corollary of our theorem; namely that any monotonic function strictly meeting the hypotheses of the theorem must have the same range as φ↦(φ∧𝖢𝗈𝗇(φ)) in the limit. To prove this, we first prove a version of jump inversion—φ↦ (φ∧𝖢𝗈𝗇(φ)) inversion—for Lindenbaum algebras. This is to say that the range of 𝖢𝗈𝗇 contains a true ideal in the Lindenbaum algebra. A similar result is established for true Π^0_2 sentences in <cit.>.


Suppose φ⊢𝖢𝗈𝗇(⊤). Then for some ψ, [φ]=[(ψ∧𝖢𝗈𝗇(ψ))].

 

Let ψ:=𝖢𝗈𝗇(⊤)→φ.


φ⊢(ψ∧𝖢𝗈𝗇(ψ)).


Trivially, φ⊢ψ. Since φ⊢𝖢𝗈𝗇(⊤), it follows that from the formalized second incompleteness theorem, i.e., 𝖢𝗈𝗇(⊤)⊢𝖢𝗈𝗇(𝖢𝗈𝗇(⊤)), that φ⊢𝖢𝗈𝗇(𝖢𝗈𝗇(⊤)). But 𝖢𝗈𝗇(⊤) is the first disjunct of ψ, so φ⊢𝖢𝗈𝗇(ψ).


(ψ∧𝖢𝗈𝗇(ψ))⊢φ.


Note that 𝖢𝗈𝗇(ψ)⊢𝖢𝗈𝗇(⊤). The claim then follows since clearly (ψ∧𝖢𝗈𝗇(⊤))⊢φ.



Let f be monotonic. Suppose that for all consistent φ,

(i) φ∧𝖢𝗈𝗇(φ) implies f(φ) and

(ii) f(φ) strictly implies φ.

Then the intersection of the ranges of f and 𝖢𝗈𝗇 in the Lindenbaum algebra contains a true ideal.



Let φ be a sentence such that φ⊢𝖢𝗈𝗇(⊤) and 

    φ⊢∀ζ(𝖢𝗈𝗇(ζ)→𝖢𝗈𝗇(ζ∧ f(ζ))).
 
Note that both of these sentences are true, and hence φ is in an element of a true ideal. By the previous proposition, there is a ψ such that [ψ∧𝖢𝗈𝗇(ψ)]=[φ]. By Remark <ref> there is a θ such that [f(θ)]=[ψ∧𝖢𝗈𝗇(ψ)], that is, φ is in the range of f.




§ ITERATING 𝖢𝗈𝗇 INTO THE TRANSFINITE


By analogy with Martin's Conjecture, we would like to show that there is a natural well-ordered hierarchy of monotonic functions and that the successor for this well-ordering is induced by 𝖢𝗈𝗇. Thus, we define the iterates of 𝖢𝗈𝗇 along elementary presentations of well-orderings.



By an elementary presentation of a recursive well-ordering we mean a pair (𝒟,<) of elementary formulas, such that (i) the relation < well-orders 𝒟 in the standard model of arithmetic and (ii) 𝖤𝖠 proves that < linearly orders the elements satisfying 𝒟, (iii) it is elementarily calculable whether an element represents zero or a successor or a limit and (iv) the elementary formulas defining the set of limit ordinals and the successor relation provably in 𝖤𝖠 satisfy their corresponding first order definitions in terms of <.




Given an elementary presentation ⟨α,<⟩ of a recursive well-ordering and a sentence φ, we use Gödel's fixed point lemma to define sentences 𝐂𝐨𝐧^⋆(φ,β) for β<α as follows.

    𝖤𝖠⊢𝐂𝐨𝐧^⋆(φ,β)↔∀γ<β, 𝖢𝗈𝗇(φ∧𝐂𝐨𝐧^⋆(φ,γ)).

We use the notation 𝖢𝗈𝗇^β(φ) for 𝐂𝐨𝐧^⋆(φ,β).



Note that, since the following clauses are provable in 𝖤𝖠.


  * 𝖢𝗈𝗇^0(φ) ↔⊤

  * 𝖢𝗈𝗇^γ+1(φ) ↔𝖢𝗈𝗇(φ∧𝖢𝗈𝗇^γ(φ))

  * 𝖢𝗈𝗇^λ(φ) ↔∀γ<λ, 𝖢𝗈𝗇^γ(φ) for λ a limit.



Note that this hierarchy is proper for true φ by Gödel's second incompleteness theorem. We need to prove that for transfinite α, 𝖢𝗈𝗇^α is monotonic over the Lindenbaum algebra of 𝖤𝖠. Before proving this claim we recall Schmerl's <cit.> technique of reflexive transfinite induction. Note that “𝖯𝗋(φ)” means that φ is provable in 𝖤𝖠.



(Schmerl) Suppose that < is an elementary linear order and that 𝖤𝖠⊢∀α(𝖯𝗋(∀β<α ,A(β))→ A(α)). Then 𝖤𝖠⊢∀α A(α).



From 𝖤𝖠⊢∀α(𝖯𝗋(∀β<α ,A(β))→ A(α)) we infer

𝖤𝖠⊢𝖯𝗋(∀αA(α))   →∀α𝖯𝗋(∀β<α,A(β))

   →∀αA(α).

Löb's theorem, i.e., 

    if 𝖤𝖠⊢𝖯𝗋(ζ)→ζ, then 𝖤𝖠⊢ζ,
 
then yields 𝖤𝖠⊢∀α A(α).




If φ⊢ψ, then 𝖢𝗈𝗇^α(φ)⊢𝖢𝗈𝗇^α(ψ).



Let 𝒜(β) denote the claim that 𝖢𝗈𝗇^β(φ)⊢𝖢𝗈𝗇^β(ψ).

We want to prove that 𝒜(α), without placing any restrictions on α. We prove the equivalent claim that 𝖤𝖠⊢𝒜(α). By Proposition <ref>, it suffices to show that

    𝖤𝖠⊢∀α(𝖯𝗋(∀β<α,𝒜(β))→𝒜(α)).

Reason within 𝖤𝖠. Suppose that 𝖯𝗋(∀β<α,𝒜(β)), which is to say that 

    𝖯𝗋(∀β<α,𝖯𝗋 (𝖢𝗈𝗇^β(φ) →𝖢𝗈𝗇^β(ψ))).

Since 𝖢𝗈𝗇^α(φ) contains 𝖤𝖠, we infer that

    𝖢𝗈𝗇^α(φ)⊢∀β<α𝖯𝗋(𝖢𝗈𝗇^β(φ) →𝖢𝗈𝗇^β(ψ)).

Since 𝖢𝗈𝗇^α(φ) proves that for all β<α, 𝖤𝖠⊬𝖢𝗈𝗇^β(φ) we infer that

    𝖢𝗈𝗇^α(φ)⊢∀β<α𝖢𝗈𝗇(𝖢𝗈𝗇^β(ψ)).

Thus, 

    𝖢𝗈𝗇^α(φ)⊢∀β<α(𝖢𝗈𝗇^β(ψ)).

This concludes the proof of the proposition.


Thus, for each predicate 𝖢𝗈𝗇^α the function 

    φ↦(φ∧𝖢𝗈𝗇^α(φ))

 is monotonic over the Lindenbaum algebra of 𝖤𝖠.
 
In this section we show that the functions given by iterated consistency are minimal with respect to each other. We fix an elementary presentation α of a recursive well-ordering. We assume that f is a monotonic function such that for every consistent φ, f(φ) strictly implies φ∧𝖢𝗈𝗇^β(φ) for all β<α. We would like to relativize the proof of Lemma <ref> to 𝖢𝗈𝗇^β. However, the proof of Lemma <ref> relied on the truth of the principle 

    ∀ζ(𝖢𝗈𝗇(ζ)→𝖢𝗈𝗇(ζ∧ f(ζ))).
 It is not in general clear that 𝖢𝗈𝗇^α(φ) implies 𝖢𝗈𝗇^α(φ∧ f(φ)). To solve this problem, we define a sequence of true sentences (θ_β)_β≤α such that for every sentence φ, if φ⊢θ_β then 𝖢𝗈𝗇^β(φ) implies 𝖢𝗈𝗇^β(φ∧ f(φ)). Thus, we are able to relativize the proof of Lemma <ref> for 𝖢𝗈𝗇^β to sentences that imply θ_β. 



Given an elementary presentation α of a recursive well-ordering, we use Gödel's fixed point lemma to define sentences θ^⋆(β) for β<α as follows.

𝖤𝖠⊢    θ^⋆(β)↔

    ∀γ<β(𝖳𝗋𝗎𝖾_Π_3(θ^⋆(γ))) ∧∀ζ((∀γ<β𝖯𝗋(ζ→θ^⋆(γ))) →(𝖢𝗈𝗇^β(ζ) →𝖢𝗈𝗇^β(ζ∧f(ζ)))).


We use the notation θ_β for θ^⋆(β).




Note that every sentence in the sequence (θ_β)_β≤α has complexity Π^0_3. Note moreover that for a successor β+1, θ_β+1 is equivalent to 

    θ_β∧∀ζ(𝖯𝗋(ζ→θ_β) →(𝖢𝗈𝗇^β+1(ζ)→𝖢𝗈𝗇^β+1(ζ∧ f(ζ)))).




Let f be monotonic such that, for all φ, 

(i) φ∧𝖢𝗈𝗇^α(φ) implies f(φ),

(ii) if [f(φ)]≠[], then f(φ) strictly implies φ∧𝖢𝗈𝗇^β(φ) for all β<α. 

Then for each β≤α, the sentence θ_β is true.



Let f be as in the statement of the lemma. We prove the claim by induction on β≤α. The base case β=0 is trivial.


For the successor case we assume that β<α and that θ_β is true; we want to show that θ_β+1 is true. So let ζ be a sentence such that ζ⊢θ_β. We want to show that 𝖢𝗈𝗇^β+1(ζ) implies 𝖢𝗈𝗇^β+1(ζ∧ f(ζ)). We prove the contrapositive, that 𝖢𝗈𝗇^β+1(ζ∧ f(ζ)) implies 𝖢𝗈𝗇^β+1(ζ).  So suppose 𝖢𝗈𝗇^β+1(ζ∧ f(ζ)), i.e., 

    †ζ∧ f(ζ)⊢𝖢𝗈𝗇^β(ζ∧ f(ζ)).
 
We reason as follows.

Since ζ⊢θ_β, ζ⊢∀γ<β, 𝖳𝗋𝗎𝖾_Π_3(θ_γ). From this we infer

    ⋆ζ⊢𝖯𝗋(ζ→∀γ<β, 𝖳𝗋𝗎𝖾_Π_3(θ_γ))
 
by Σ^0_1 completeness. Moreover, since ζ⊢θ_β,

ζ   ⊢∀φ((∀γ<β𝖯𝗋(φ→θ_γ)) →(𝖢𝗈𝗇^β(φ) →𝖢𝗈𝗇^β(φ∧f(φ)) ) )  by the definition of θ_β. 

   ⊢∀γ<β𝖯𝗋 (ζ→θ_γ) →(𝖢𝗈𝗇^β(ζ) →𝖢𝗈𝗇^β(ζ∧f(ζ)))  by instantiation. 

   ⊢𝖢𝗈𝗇^β(ζ)→𝖢𝗈𝗇^β(ζ∧f(ζ))  by (<ref>).

ζ∧f(ζ)   ⊢𝖢𝗈𝗇^β(ζ∧f(ζ)) by (<ref>).

   ⊢𝖢𝗈𝗇^β(ζ) by logic.

ζ   ⊢𝖢𝗈𝗇^β(ζ)→f(ζ)  by logic.

Thus, (ζ∧𝖢𝗈𝗇^β(ζ))⊢ f(ζ). Since f(φ) always strictly implies φ∧𝖢𝗈𝗇^β(φ), we infer that 

    [ζ∧𝖢𝗈𝗇^β(ζ)]=[].
 
This is to say that 𝖢𝗈𝗇^β+1(ζ).


For the limit case we let β be a limit ordinal and assume that for every γ<β, θ_γ is true. We want to show that θ_β is true. Let ζ be a sentence such that for every γ<β, ζ⊢θ_γ. We want to show that 𝖢𝗈𝗇^β(ζ) implies 𝖢𝗈𝗇^β(ζ∧ f(ζ)). So assume that 𝖢𝗈𝗇^β(ζ), i.e., for every γ<β, 𝖢𝗈𝗇^γ(ζ). Let γ<β. Since β is a limit ordinal, γ+1<β. So by the inductive hypothesis θ_γ+1 is true. That is, by the definition of θ_γ+1,

    ∀φ(𝖯𝗋(φ→θ_γ)→ (𝖢𝗈𝗇^γ(φ)→𝖢𝗈𝗇^γ(φ∧ f(φ)))).
 
By instantiation, we infer that 

    𝖯𝗋(ζ→θ_γ)→ ( 𝖢𝗈𝗇^γ(ζ)→𝖢𝗈𝗇^γ(ζ∧ f(ζ))).
 
Since ζ⊢θ_γ and 𝖢𝗈𝗇^γ(ζ), this means that 𝖢𝗈𝗇^γ(ζ∧ f(ζ)). Since γ was a generic ordinal less than β, we get that 
    ∀γ<β, 𝖢𝗈𝗇^γ(ζ∧ f(ζ)),
 i.e., 𝖢𝗈𝗇^β(ζ). This completes the proof of the lemma.



Let f be monotonic. Suppose that for all φ, 

(i) φ∧𝖢𝗈𝗇^α(φ) implies f(φ),

(ii) if [f(φ)]≠[], then f(φ) strictly implies φ∧𝖢𝗈𝗇^β(φ) for all β<α. 

Then for every true χ, there is a true ψ such that ψ⊢χ and [f(ψ)] = [ψ∧𝖢𝗈𝗇^α(ψ)].



Let χ be a true sentence. By the lemma, θ_α is true. So 
    φ:=χ∧θ_α
 is true. We let 
    ψ:=φ∧(f(φ)→𝖢𝗈𝗇^α(φ)).
 Note that ψ⊢χ. We now show that [ψ∧𝖢𝗈𝗇^α(ψ)]=[f(ψ)].


f(ψ)⊢ (ψ∧ f(φ)).


Since f is monotonic.


(ψ∧ f(φ))⊢ (φ∧𝖢𝗈𝗇^α(φ)).


By the definition of ψ.


(φ∧𝖢𝗈𝗇^α(φ))⊢ (ψ∧𝖢𝗈𝗇^α(ψ)).


It is clear from the definition of ψ that (φ∧𝖢𝗈𝗇^α(φ))⊢ψ. So it suffices to show that (φ∧𝖢𝗈𝗇^α(φ))⊢𝖢𝗈𝗇^α(ψ).

φ∧𝖢𝗈𝗇^α(φ)   ⊢∀ζ((∀β<α𝖯𝗋(ζ→θ_β)) →(𝖢𝗈𝗇^α(ζ)→𝖢𝗈𝗇^α(ζ∧f(ζ)))) by choice of φ.

   ⊢∀β<α𝖯𝗋(φ→θ_β) →(𝖢𝗈𝗇^α(φ)→𝖢𝗈𝗇^α(φ∧f(φ))) by instantiation.

   ⊢∀β<α𝖯𝗋(φ→θ_β)→𝖢𝗈𝗇^α(φ∧f(φ)) by logic.

Since 𝖢𝗈𝗇^α(φ∧ f(φ))⊢𝖢𝗈𝗇^α(ψ), to prove the desired claim it suffices to show that 
    φ∧𝖢𝗈𝗇^α(φ)⊢∀β<α𝖯𝗋(φ→θ_β).
 
We reason as follows.

φ   ⊢θ_α by choice of φ.

   ⊢∀β<α(𝖳𝗋𝗎𝖾_Π_3θ_β)  by definition of θ_α.

   ⊢𝖯𝗋(φ→∀β<α(𝖳𝗋𝗎𝖾_Π_3θ_β))  by Σ^0_1 completeness.

   ⊢∀β<α𝖯𝗋(φ→𝖳𝗋𝗎𝖾_Π_3 θ_β)

   ⊢∀β<α𝖯𝗋(φ→θ_β)

It is immediate from the preceding claims that f(ψ)⊢ψ∧𝖢𝗈𝗇^α(ψ). By assumption, ψ + 𝖢𝗈𝗇^α(ψ) ⊢ f(ψ), so it follows that [f(ψ)]=[ψ∧𝖢𝗈𝗇^α(ψ)].



There is no monotonic f such that for all φ, if [φ∧𝖢𝗈𝗇^α(φ)]≠[], then both 

(i) φ∧𝖢𝗈𝗇^α(φ) strictly implies f(φ) and

(ii) f(φ) strictly implies φ∧𝖢𝗈𝗇^β(φ) for all β<α.




§ FINITE ITERATES OF 𝖢𝗈𝗇 ARE INEVITABLE


In this section and the next section we prove that the iterates of 𝖢𝗈𝗇 are, in a sense, inevitable. First we show that, for every natural number n, if a monotonic function f is always bounded by 𝖢𝗈𝗇^n, then it is somewhere equivalent to 𝖢𝗈𝗇^k for some k≤ n. In §5, we turn to generalizations of this result into the effective transfinite.



Let n∈ℕ. Let f be a monotonic function such that for every φ, 

(i) φ∧𝖢𝗈𝗇^n(φ) implies f(φ) and 

(ii) f(φ) implies φ. 

Then for some φ and some k≤ n, [f(φ)]=[φ∧𝖢𝗈𝗇^k(φ)]≠[].



We suppose, towards a contradiction, that there is no ψ and no k≤ n such that [f(ψ)]=[ψ∧𝖢𝗈𝗇^k(ψ)]≠[]. We then let φ_1 be a true statement such that 

   φ_1⊢∀ζ(𝖢𝗈𝗇(ζ)→𝖢𝗈𝗇(ζ∧f(ζ)))

   φ_1 ⊢∀k∀ζ(𝖢𝗈𝗇^k+1(ζ)→𝖯𝗋((ζ∧𝖢𝗈𝗇^k(ζ))↔f(ζ))).

The first condition is that φ_1 proves that for every consistent φ, f(φ) strictly implies φ. The second condition is that φ_1 proves that f(ζ) never coincides with ζ∧𝖢𝗈𝗇^k(ζ), unless [ζ∧𝖢𝗈𝗇^k(ζ)]=[].

We define a sequence of statements, starting with φ_1, as follows: 
    φ_k+1:=φ_k∧(f(φ_k)→𝖢𝗈𝗇^k(φ_k)).
 We will use our assumption to show that, for all k, φ_k∧𝖢𝗈𝗇^k(φ_k)⊢𝖢𝗈𝗇^k(φ_k+1). From this we will deduce that [f(φ_n+1)]=[φ_n+1∧𝖢𝗈𝗇^n(φ_n+1)]≠[], contradicting the assumption that f and 𝖢𝗈𝗇^n never coincide. Most of the work is contained in the proof of the following lemma.



For all k, for all j≥ k, (φ_k∧𝖢𝗈𝗇^k(φ_k)) ⊢𝖢𝗈𝗇^k(φ_j).



We prove the claim by a double induction. The primary induction is on k. For the base case k=1, we prove the claim by induction on j. The base case j=1 follows trivially. For the inductive step we assume that (φ_1∧𝖢𝗈𝗇(φ_1))⊢𝖢𝗈𝗇(φ_j) and show that (φ_1∧𝖢𝗈𝗇(φ_1))⊢𝖢𝗈𝗇(φ_j+1).

φ_1∧𝖢𝗈𝗇(φ_1)   ⊢∀ζ(𝖢𝗈𝗇(ζ)→𝖢𝗈𝗇(ζ∧f(ζ))) by choice of φ_1.

   ⊢𝖢𝗈𝗇(φ_j)→𝖢𝗈𝗇(φ_j∧f(φ_j))  by instantiation.

φ_1∧𝖢𝗈𝗇(φ_1)   ⊢𝖢𝗈𝗇(φ_j) by the inductive hypothesis.

   ⊢𝖢𝗈𝗇(φ_j∧f(φ_j))  by logic.

   ⊢𝖢𝗈𝗇(φ_j+1)  by definition of φ_j+1.

For the inductive step we assume that the claim is true of k-1, i.e., 

    ∀ j≥ k-1((φ_k-1∧𝖢𝗈𝗇^k-1(φ_k-1))⊢(𝖢𝗈𝗇^k-1(φ_j))).
 
We prove the claim for k. Once again, we prove the claim by induction on j. The base case j=k follows trivially. For the inductive step we assume that φ_k∧𝖢𝗈𝗇^k(φ_k)⊢𝖢𝗈𝗇^k(φ_j). We want to prove that φ_k∧𝖢𝗈𝗇^k(φ_k)⊢𝖢𝗈𝗇^k(φ_j+1).

φ_k∧𝖢𝗈𝗇^k(φ_k)   ⊢∀x∀ζ(𝖢𝗈𝗇^x+1(ζ)→𝖯𝗋((ζ∧𝖢𝗈𝗇^x(ζ))↔f(ζ)))  by choice of φ_1.

   ⊢𝖢𝗈𝗇^k(φ_j)→𝖯𝗋((φ_j∧𝖢𝗈𝗇^k-1(φ_j))↔f(φ_j))  by instantiation.

φ_k∧𝖢𝗈𝗇^k(φ_k)   ⊢𝖢𝗈𝗇^k(φ_j)  by the inner inductive hypothesis.

   ⊢𝖯𝗋((φ_j∧𝖢𝗈𝗇^k-1(φ_j))↔f(φ_j))  by logic.

Thus, φ_k∧𝖢𝗈𝗇^k(φ_k) proves that one of the following cases holds.

    (φ_j∧𝖢𝗈𝗇^k-1(φ_j))⊬ f(φ_j)
 

    f(φ_j)⊬(φ_j∧𝖢𝗈𝗇^k-1φ_j)
 
We now show that φ_k∧𝖢𝗈𝗇^k(φ_k) refutes the second option.


φ_k∧𝖢𝗈𝗇^k(φ_k)⊢𝖯𝗋(f(φ_j)→(φ_j∧𝖢𝗈𝗇^k-1φ_j)).


By the outer inductive hypothesis, 𝖤𝖠 proves the following conditional: 

    θ:=((φ_j-1∧𝖢𝗈𝗇^k-1(φ_j-1))→(𝖢𝗈𝗇^k-1(φ_j))).
 
Thus, f(φ_j) (which contains 𝖤𝖠) also proves θ.  We now show that f(φ_j)⊢𝖢𝗈𝗇^k-1(φ_j).

f(φ_j)   ⊢φ_j∧f(φ_j-1)  since f is monotonic.

   ⊢(φ_j-1∧(f(φ_j-1)→𝖢𝗈𝗇^j-1(φ_j-1)))∧f(φ_j-1)  by the definition of φ_j.

   ⊢φ_j-1∧𝖢𝗈𝗇^j-1(φ_j-1)  by logic.

   ⊢φ_j-1∧𝖢𝗈𝗇^k-1(φ_j-1)  since j≥ k.

   ⊢𝖢𝗈𝗇^k-1(φ_j)  since f(φ_j) proves θ.

By Σ^0_1 completeness, (φ_k∧𝖢𝗈𝗇^k(φ_k))⊢𝖯𝗋(f(φ_j) →𝖢𝗈𝗇^k-1(φ_j)).


(φ_k∧𝖢𝗈𝗇^k(φ_k)) ⊢𝖢𝗈𝗇^k (φ_j+1).


We reason as follows.

(φ_k∧𝖢𝗈𝗇^k(φ_k))   ⊢𝖯𝗋((φ_j ∧𝖢𝗈𝗇^k-1(φ_j))→f(φ_j))  by the previous claim. 

   ⊢𝖢𝗈𝗇(φ_j∧f(φ_j)∧𝖢𝗈𝗇^k-1(φ_j)). 

   ⊢𝖢𝗈𝗇(φ_j+1∧𝖢𝗈𝗇^k-1(φ_j))  by the definition of φ_j+1.

   ⊢𝖢𝗈𝗇(φ_j+1∧𝖢𝗈𝗇^k-1(φ_j+1))  by the outer inductive hypothesis.

   ⊢𝖢𝗈𝗇^k(φ_j+1)  by definition of 𝖢𝗈𝗇^k.

This concludes the proof of the lemma.


As an instance of the lemma, we get that (φ_n∧𝖢𝗈𝗇^n(φ_n)) ⊢𝖢𝗈𝗇^n(φ_n+1). We reason as follows.

f(φ_n+1)   ⊢φ_n∧(f(φ_n)→𝖢𝗈𝗇^n(φ_n)) by the definition of φ_n+1.

f(φ_n+1)   ⊢f(φ_n) since f is monotonic.

   ⊢𝖢𝗈𝗇^n(φ_n) by logic.

   ⊢𝖢𝗈𝗇^n(φ_n+1) by the lemma.

On the other hand, φ_n+1∧𝖢𝗈𝗇^n(φ_n+1)⊢ f(φ_n+1) since f is everywhere bounded by 𝖢𝗈𝗇^n. Thus, [f(φ_n+1)]=[φ_n+1∧𝖢𝗈𝗇^n(φ_n+1)], contradicting the assumption that there is no ψ and no k≤ n such that [f(ψ)]=[ψ∧𝖢𝗈𝗇^k(ψ)]≠[]. 




§ TRANSFINITE ITERATES OF 𝖢𝗈𝗇 ARE INEVITABLE.


Generalizing the proof of Theorem <ref> into the transfinite poses the following difficulty. Recall that the proof of Theorem <ref> makes use of a sequence of sentences starting with φ_0:=⊤ where 
    φ_k+1:=φ_k∧(f(φ_k)→𝖢𝗈𝗇^k(φ_k)).
 It is not clear what the ωth sentence in the sequence should be. A natural idea is that for a limit ordinal λ the corresponding “limit sentence” should quantify over the sentences in the sequence beneath it and express, roughly, 

    ∀γ<λ(𝖳𝗋𝗎𝖾(φ_γ) ∧ (𝖳𝗋𝗎𝖾(f(φ_γ))→𝖢𝗈𝗇^γ(φ_γ))).
 
However, if the sentences in the sequence (φ_γ)_γ<λ have unbounded syntactic complexity, then we are not guaranteed to have a truth-predicate with which we can quantify over them.

Nevertheless, we show that Theorem <ref> generalizes into the transfinite given an additional assumption on complexity. Note that φ↦(φ∧𝖢𝗈𝗇(φ)) can be factored into two functions—the identity and φ↦𝖢𝗈𝗇(φ)—the latter of which always produces a Π^0_1 sentence. For the rest of this section, we will focus on monotonic functions φ↦φ∧ f(φ) where f is monotonic and also f(φ)∈Π^0_1 for all φ.


A function f is Π^0_1 if f(φ)∈Π^0_1 for all φ.


For the next theorem we fix an elementary presentation Γ of a recursive well-ordering. In the statement of the theorem and throughout the proof α, β, γ, δ, etc. are names of ordinals from the notation system Γ. 



Let f be a monotonic Π^0_1 function. Then either 

(i) for some β≤α and some φ, [φ∧ f(φ)]=[φ∧𝖢𝗈𝗇^β(φ)]≠[] or

(ii) for some φ, (φ∧𝖢𝗈𝗇^α(φ))⊬ f(φ).



Let f be a monotonic Π^0_1 function such that for every φ, 

    (φ∧𝖢𝗈𝗇^α(φ))⊢ (φ∧ f(φ)).
 
We assume, for the sake of contradiction, that there is no sentence ζ and no β≤α such that [ζ∧𝖢𝗈𝗇^β(ζ)]=[ζ∧ f(ζ)]≠[]. We then let φ be the conjunction of the following four sentences.

    ∀ζ(𝖢𝗈𝗇(ζ)→𝖢𝗈𝗇(ζ∧ f(ζ)))


    ∀β≤α∀ζ(𝖢𝗈𝗇^β(ζ)→∀δ<β, 𝖯𝗋((ζ∧𝖢𝗈𝗇^δ(ζ))↔ (ζ∧ f(ζ))))


    ∀ζ∀η( 𝖯𝗋(ζ→η) →𝖯𝗋(f(ζ)→ f(η)) )


    ∀ x (𝖯𝗋(𝖳𝗋𝗎𝖾_Π^0_2(x))→𝖳𝗋𝗎𝖾_Π^0_2(x))


The first expresses that for every consistent φ, f(φ) strictly implies φ. The second sentence expresses that if β<α, then f(ζ) and ζ∧𝖢𝗈𝗇^β(ζ) never coincide, unless [ζ∧𝖢𝗈𝗇^β(ζ)]=[] . The third sentence expresses the monotonicity of f. The fourth sentence expresses the Π^0_2 soundness of 𝖤𝖠. Note that each of these sentences is true, so their conjunction φ is also true. Each of the four sentences is Π^0_2, whence so is φ. 

We are interested in the following sequence (φ_β)_β≤Γ. Note that the sentences in the sequence (φ_β)_β≤Γ all have complexity Π^0_2. Note moreover that since φ_1 is true, so is φ_β for every β.

φ_1   :=φ.

φ_γ   := φ_1∧∀δ<γ(𝖳𝗋𝗎𝖾_Π_1(f(φ_δ))→𝖢𝗈𝗇^δ(φ_δ))  for γ>1.


Formally, we define the sequence (φ_β)_β≤Γ by Gödel's fixed point lemma as in Definition <ref>.



We may assume that the ordinal notation system Γ is provably linear in 𝖤𝖠. Thus, 𝖤𝖠⊢∀β≤α,∀γ<β(𝖳𝗋𝗎𝖾_Π_2(φ_β)→𝖳𝗋𝗎𝖾_Π_2(φ_γ)).


Our goal is to show that 

    [φ_α+1∧𝖢𝗈𝗇^α(φ_α+1)]=[φ_α+1∧ f(φ_α+1)]

contradicting the assumption that f and 𝖢𝗈𝗇^α never coincide. The main lemmas needed to prove this result are the following.


 𝖤𝖠⊢∀γ≤α𝖯𝗋( (φ_γ∧ f(φ_γ)) →φ_α).



 
𝖤𝖠⊢∀β≤α∀γ≤β𝖯𝗋((φ_β∧𝖢𝗈𝗇^γ(φ_β) )→𝖢𝗈𝗇^γ(φ_β∧ f(φ_β))).


Lemma <ref> is needed to derive Lemma <ref>. We now show how we use Lemma <ref> to derive Theorem <ref>. As an instance of Lemma <ref>, letting α=β=γ, we infer that

    𝖤𝖠⊢𝖯𝗋((φ_α∧𝖢𝗈𝗇^α(φ_α)) →𝖢𝗈𝗇^α(φ_α∧ f(φ_α))).

From the soundness of 𝖤𝖠, we infer that

    ∓φ_α + 𝖢𝗈𝗇^α(φ_α) ⊢𝖢𝗈𝗇^α(φ_α∧ f(φ_α)).

We then reason as follows.

φ_α+1   ⊢φ_α∧(f(φ_α)→𝖢𝗈𝗇^α(φ_α)) by the definition of φ_α+1.

 f(φ_α+1)   ⊢f(φ_α) since f is monotonic.

φ_α+1 + f(φ_α+1)   ⊢φ_α∧𝖢𝗈𝗇^α(φ_α) by logic.

   ⊢𝖢𝗈𝗇^α(φ_α+1) by ∓.

On the other hand, φ_α+1 + 𝖢𝗈𝗇^α(φ_α+1)⊢ f(φ_α+1) since f is everywhere bounded by 𝖢𝗈𝗇^α. Since φ_1 is true, so too is φ_α+1, whence we infer that 

    [φ_α+1∧𝖢𝗈𝗇^α(φ_α+1)]=[φ_α+1∧ f(φ_α+1)]≠[],
 
contradicting the claim that there is no sentence ζ and no β≤α such that [ζ∧𝖢𝗈𝗇^β(ζ)]=[ζ∧ f(ζ)]≠[].


It remains to prove Lemma <ref> and Lemma <ref>. We devote one subsection to each.



 §.§ Proof of Lemma <ref>


In this subsection we prove Lemma <ref>. First we recall the statement of the lemma.



    𝖤𝖠⊢∀γ≤α(𝖯𝗋(φ_γ∧ f(φ_γ)) →φ_α).





We reason in 𝖤𝖠. Let γ≤α. We assume that 

    η𝖳𝗋𝗎𝖾_Π_2(φ_γ)∧𝖳𝗋𝗎𝖾_Π_1(f(φ_γ)).


We we want to derive φ_α, i.e.

    φ_1∧∀σ<α(𝖳𝗋𝗎𝖾_Π_1(f(φ_σ))→𝖢𝗈𝗇^σ(φ_σ)).
 

The first conjunct follows trivially from the assumption that 𝖳𝗋𝗎𝖾_Π_2(φ_γ). We now prove the second conjunct of φ_α in two parts, first for all σ such that α>σ≥γ and then for all σ<γ. 

α>σ≥γ: From the assumption that 𝖳𝗋𝗎𝖾_Π^0_2(φ_γ) we infer that φ_1, whence we infer that f is monotonic. Thus, for all δ≥γ, f(φ_δ)⊢ f(φ_γ), i.e., 𝖤𝖠⊢(f(φ_δ)→ f(φ_γ)). From φ_1 we also infer that 𝖤𝖠 is Π^0_2 sound, and so we infer that for all δ≥γ, 𝖳𝗋𝗎𝖾_Π_1(f(φ_δ))→𝖳𝗋𝗎𝖾_Π_1(f(φ_γ)). From the assumption that 𝖳𝗋𝗎𝖾_Π_1(f(φ_γ)) we then infer that for all δ≥γ, 𝖳𝗋𝗎𝖾_Π_1(f(φ_δ)), whence for all δ≥γ, 𝖳𝗋𝗎𝖾_Π_1(f(φ_δ))→𝖢𝗈𝗇^δ(φ_δ).

σ< γ: By Remark <ref>, <ref> implies that 

    ∀σ<γ (𝖳𝗋𝗎𝖾_Π_1(f(φ_σ))→𝖢𝗈𝗇^σ(φ_σ)).
 

This completes the proof of Lemma <ref>.




 §.§ Proof of Lemma <ref>


In this subsection we prove Lemma <ref>. We recall the statement of Lemma <ref>.



    𝖤𝖠⊢∀β≤α∀γ≤β𝖯𝗋(φ_β +𝖢𝗈𝗇^γ(φ_β) →𝖢𝗈𝗇^γ(φ_β∧ f(φ_β))).



The proof of this lemma is importantly different from the proof of Lemma <ref>. In particular, to push the induction through limit stages we need to know not only that the inductive hypothesis is true but also that it is provable in 𝖤𝖠. We resolve this issue by using Schmerl's technique of reflexive transfinite induction (see Proposition <ref>).

In the proof of the lemma, we let 𝒞(γ,δ) abbreviate the claim that 

    φ_δ+𝖢𝗈𝗇^γ(φ_δ)⊢𝖢𝗈𝗇^γ(φ_δ∧ f(φ_δ)).



We want to show that 

    𝖤𝖠⊢∀β≤α(∀γ≤β(𝒞(γ,β))).

By Proposition <ref> it suffices to show that 

    𝖤𝖠⊢∀α(𝖯𝗋(∀β≤α∀γ≤β𝒞(γ,β))→∀γ≤α𝒞(γ,α)).[The reader might expect that we need to write “β<α” instead of “β≤α” in the antecedent for this to match the statement of Proposition <ref>. However, it is clear from the proof of Proposition <ref> that this suffices.]

Thus, we reason in 𝖤𝖠 and fix α. We assume that

    △𝖯𝗋(∀β≤α, ∀γ≤β, 𝒞(γ,β)).

We let γ≤α and we want to show that 𝒞(γ,α).

Since φ_α⊢φ we infer that 

    ♯φ_α+𝖢𝗈𝗇^γ(φ_α)⊢∀δ<γ, 𝖯𝗋((φ_α∧𝖢𝗈𝗇^δ(φ_α)) ↔ (φ_α∧ f(φ_α))).


We first note that both

φ_α   ⊢∀δ<γ(𝖳𝗋𝗎𝖾_Π_1(f(φ_δ))→𝖢𝗈𝗇^δ(φ_δ))  by the definition of φ_α and also

φ_α+ f(φ_α)   ⊢∀δ<γ𝖯𝗋(f(φ_α) →f(φ_δ))  since φ_1 proves the monotonicity of f.

    ⊢∀δ<γ(f(φ_α)→𝖳𝗋𝗎𝖾_Π_1(f(φ_δ)))  since φ_1 proves the Π^0_2 soundness of 𝖤𝖠.

   ⊢∀δ<γ, 𝖳𝗋𝗎𝖾_Π_1(f(φ_δ))  by logic.

Thus, we may reason as follows.

φ_α+f(φ_α)   ⊢∀δ<γ, 𝖢𝗈𝗇^δ(φ_δ)

   ⊢∀δ<γ, 𝖢𝗈𝗇^δ(φ_δ∧f(φ_δ)))  since (<ref>) delivers 𝒞(δ,δ).

   ⊢∀δ<γ, 𝖢𝗈𝗇^δ(φ_α)  by Lemma <ref>.

Thus, by Σ^0_1 completeness,

    𝖤𝖠⊢∀δ<γ𝖯𝗋( (φ_α∧ f(φ_α)) →𝖢𝗈𝗇^δ(φ_α)).

Combined with (<ref>), this delivers

φ_α+𝖢𝗈𝗇^γ(φ_α)   ⊢∀δ<γ𝖯𝗋 ( (φ_α ∧𝖢𝗈𝗇^δ(φ_α)) →f(φ_α)).

   ⊢∀δ<γ, 𝖢𝗈𝗇(φ_α ∧f(φ_α) ∧𝖢𝗈𝗇^δ(φ_α)).

   ⊢∀δ<γ, 𝖢𝗈𝗇(φ_α ∧f(φ_α) ∧𝖢𝗈𝗇^δ(φ_α∧f(φ_α)))  since (<ref>) delivers 𝒞(δ,α).

   ⊢𝖢𝗈𝗇^γ(φ_α∧f(φ_α)).

This completes the proof of Lemma <ref>.


Theorem <ref> shows the inevitability of the consistency operator. For a sufficiently constrained monotonic function f, f must coincide with an iterate of 𝖢𝗈𝗇 on some non-trivial sentence. However, it is not clear from the proofs of Theorem <ref> or Theorem <ref> that f must coincide with 𝖢𝗈𝗇 on a true sentence.


Let f be a monotonic Π^0_1 function. Suppose that for every φ, 
    (φ∧𝖢𝗈𝗇^α(φ))⊢ f(φ).
 Must there be some β≤α and some true φ such that 
    [φ∧ f(φ)]=[φ∧𝖢𝗈𝗇^β(φ)]?





§ 1-CONSISTENCY AND ITERATED CONSISTENCY


Just as the Π^0_1 fragments of natural theories can often be approximated by iterated consistency statements, the Π^0_2 fragments of natural theories can often be approximated by iterated 1-consistency statements. A theory T is 1-consistent if T+Th_Π^0_1(ℕ) is consistent. The 1-consistency of 𝖤𝖠+φ can be expressed by the following Π^0_2 sentence, 1𝖢𝗈𝗇(φ): 
    ∀ x (𝖳𝗋𝗎𝖾_Π^0_1(x)→𝖢𝗈𝗇(φ∧𝖳𝗋𝗎𝖾_Π^0_1(x))).


In this section, we investigate the relationship between 1-consistency and iterated consistency. First, we show that 1𝖢𝗈𝗇 majorizes every iterate of 𝖢𝗈𝗇^α.



For any elementary presentation α of a recursive well ordering, there is a true sentence φ such that for every ψ, if ψ⊢φ, then (ψ∧ 1𝖢𝗈𝗇(ψ)) implies (ψ∧𝖢𝗈𝗇^α(ψ)). Moreover, if [ψ∧𝖢𝗈𝗇^α(ψ)]≠[] then (ψ∧ 1𝖢𝗈𝗇(ψ)) strictly implies (ψ∧𝖢𝗈𝗇^α(ψ)).


 

Let α be an elementary presentation of a recursive well-ordering. Let φ be a true sentence such that φ⊢𝖳𝖨^α_Π^0_1, i.e., φ implies the validity of transfinite induction along α for Π^0_1 predicates. We prove that 

    (φ∧ 1𝖢𝗈𝗇(φ))⊢𝖢𝗈𝗇^α+1(φ).


Since φ∧ 1𝖢𝗈𝗇(φ)⊢𝖳𝖨^α_Π^0_1, it suffices to show that:

Base case: (φ∧ 1𝖢𝗈𝗇(φ))⊢𝖢𝗈𝗇(φ)

Successor case: (φ∧ 1𝖢𝗈𝗇(φ))⊢∀β<α( 𝖢𝗈𝗇^β(φ)→𝖢𝗈𝗇^β+1(φ))

Limit case: (φ∧ 1𝖢𝗈𝗇(φ))⊢∀λ(lim(λ)→((∀β<λ𝖢𝗈𝗇^β(φ))→𝖢𝗈𝗇^λ(φ)))

The base case and the limit case are both trivial. For the successor case we first note that by the definition of 1𝖢𝗈𝗇(φ),

    1𝖢𝗈𝗇(φ)⊢∀ x (𝖳𝗋𝗎𝖾_Π^0_1(x)→𝖢𝗈𝗇(φ∧𝖳𝗋𝗎𝖾_Π^0_1(x))),

and so by substituting 𝖢𝗈𝗇^β(φ) in for x,

    ⊕
    1𝖢𝗈𝗇(φ)⊢𝖳𝗋𝗎𝖾_Π^0_1(𝖢𝗈𝗇^β(φ))→𝖢𝗈𝗇(φ∧𝖳𝗋𝗎𝖾_Π^0_1(𝖢𝗈𝗇^β(φ))).

Thus, we reason as follows.

1𝖢𝗈𝗇(φ)⊢𝖢𝗈𝗇^β(φ)   →𝖢𝗈𝗇(φ∧𝖳𝗋𝗎𝖾_Π^0_1(𝖢𝗈𝗇^β(φ)))  by (<ref>).

   →𝖢𝗈𝗇(φ∧𝖢𝗈𝗇^β(φ)).

   →𝖢𝗈𝗇^β+1(φ)  by the definition of 𝖢𝗈𝗇^β+1.

It is clear that the implication φ∧1𝖢𝗈𝗇(φ)⊢φ∧𝖢𝗈𝗇^α(φ) is strict as long as [φ∧𝖢𝗈𝗇^α(φ)]≠[]. This completes the proof of the proposition.


In light of the previous proposition, one might conjecture that 1𝖢𝗈𝗇 is the weakest monotonic function majorizing every function of the form 𝖢𝗈𝗇^α for some recursive well-ordering α on true sentences. However, this is not so. To demonstrate this, we use a recursive linear order that has no hyperarithmetic infinite descending sequences. Harrison <cit.> introduced such an ordering with order-type ω_1^CK×(1+ℚ); see also Feferman and Spector <cit.> who consider such orderings in the context of iterated reflection principles. We use a presentation ℋ of Harrison's ordering such satisfying the conditions explicated in Definition <ref>. We note that since ℋ has no hyperarithmetic descending sequences, transfinite induction along ℋ for Π^0_1 properties is valid. Our idea is to produce a function stronger than each 𝖢𝗈𝗇^α but weaker than 1𝖢𝗈𝗇 by iterating 𝖢𝗈𝗇 along the Harrison linear order. 


There are infinitely many monotonic functions f such that for every recursive ordinal α, there is an elementary presentation a of α such that f majorizes 𝖢𝗈𝗇^a on a true ideal but also 1𝖢𝗈𝗇 majorizes f on a true ideal.



In Definition <ref>, we used Gödel's fixed point lemma to produce iterates of 𝖢𝗈𝗇 along an elementary well-ordering. We similarly use Gödel's fixed point lemma to define sentences 𝐂𝐨𝐧^⋆(φ,β) for β∈ℋ as follows.

    𝖤𝖠⊢𝐂𝐨𝐧^⋆(φ,β)↔∀γ<_ℋβ, 𝖢𝗈𝗇(φ∧𝐂𝐨𝐧^⋆(φ,γ)).

We use the notation 𝖢𝗈𝗇^β(φ) for 𝐂𝐨𝐧^⋆(φ,β).
Recall that we are assuming that it is elementarily calculable whether an element of ℋ is zero or a successor or a limit. Thus, the following clauses are provable in 𝖤𝖠.


  * 𝖢𝗈𝗇^0(φ) ↔⊤

  * 𝖢𝗈𝗇^γ+1(φ) ↔𝖢𝗈𝗇(φ∧𝖢𝗈𝗇^γ(φ))

  * 𝖢𝗈𝗇^λ(φ) ↔∀γ<_ℋλ, 𝖢𝗈𝗇^γ(φ) for λ a limit.



For γ∈ℋ, the function φ↦Con^γ(φ) is monotonic.


This follows immediately from Proposition <ref>. Note that in the statement of Lemma <ref> we assume only that < is an elementary linear ordering, not a well-ordering. 


There are infinitely many monotonic functions f such that for every recursive well-ordering α, there is an elementary presentation a of α such that f majorizes 𝖢𝗈𝗇^a on true sentences.


If x<_ℋy then 𝖢𝗈𝗇^y(φ) strictly implies 𝖢𝗈𝗇^x(φ) for every φ such that 𝖢𝗈𝗇^x(φ)≠[]. Given the order type of ℋ, this means that for infinitely many γ, for every recursive well-ordering α, 𝖢𝗈𝗇^γ majorizes 𝖢𝗈𝗇^a where a represents α in ℋ.


1𝖢𝗈𝗇 majorizes 𝖢𝗈𝗇^a on true sentences for each a∈ℋ.

Since every Π^0_1 definable subset of ω has an ℋ-least element, the sentence 𝖳𝖨^ℋ_Π^0_1, which expresses the validity of transfinite induction along ℋ for Π^0_1 predicates, is true. But then if φ⊢𝖳𝖨^ℋ_Π^0_1, then for any γ∈ℋ, (φ∧ 1𝖢𝗈𝗇(φ)) strictly implies (φ∧𝖢𝗈𝗇^γ(φ)) as long as [(φ∧𝖢𝗈𝗇^γ(φ))]≠[], as in Proposition <ref>.




§ AN UNBOUNDED RECURSIVELY ENUMERABLE SET THAT CONTAINS NO TRUE IDEALS


In this section we prove a limitative result. Theorem <ref> demonstrates that if f is monotonic and that for all consistent φ, (i) φ∧𝖢𝗈𝗇(φ) implies f(φ) and (ii) f(φ) strictly implies φ, then for cofinally many true φ, [f(φ)] = [φ∧𝖢𝗈𝗇(φ)]. It is natural to conjecture that cofinal equivalence with 𝖢𝗈𝗇 be strengthened to equivalence to 𝖢𝗈𝗇 in the limit, i.e., on a true ideal. One strategy to strengthen Theorem <ref> in this way would be to show that every recursively enumerable set that contains arbitrarily strong true sentences and that is closed under provable equivalence contains a true ideal.

We now show that the aforementioned strategy fails. To this end, we define a recursively enumerable set 𝒜 that contains arbitrarily strong true sentences and that is closed under provable equivalence but does not contain any true ideals. We are grateful to Matthew Harrison-Trainor for simplifying the proof of the following proposition.



There is a recursively enumerable set 𝒜 that contains arbitrarily strong true sentences and that is closed under 𝖤𝖠 provable equivalence but does not contain any true ideals.



Let {φ_0,φ_1,...} be an effective Gödel numbering of the language of arithmetic. We describe the construction of 𝒜 in stages. During a stage n we may activate a sentence ψ, in which case we say that ψ is active until it is deactivated at some later stage n+k. After describing the construction of 𝒜 we verify that A has the desired properties.

Stage 0: Numerate φ_0 and φ_0 into 𝒜. Activate the sentences (φ_0∧𝖢𝗈𝗇(φ_0)) and (φ_0∧𝖢𝗈𝗇(φ_0)).

Stage n+1: There are finitely many active sentences. For each such sentence ψ, numerate θ_0:=(ψ∧φ_n+1) and θ_1:=(ψ∧φ_n+1) into 𝒜. Deactivate the sentence ψ and activate the sentences (θ_0∧𝖢𝗈𝗇(θ_0)) and (θ_1∧𝖢𝗈𝗇(θ_1)).

We dovetail the construction with a search through 𝖤𝖠 proofs. If we ever see that 𝖤𝖠⊢φ↔ψ for some φ that we have already numerated into 𝒜, then we numerate ψ into 𝒜.

Now we check that 𝒜 has the desired properties. It is clear that 𝒜 is recursively enumerable and that 𝒜 is closed under 𝖤𝖠 provable equivalence.


𝒜 contains arbitrarily strong true sentences. That is, for each true sentence φ, there is a true sentence ψ such that ψ⊢φ and ψ∈𝒜.


At any stage in the construction of 𝒜, there are finitely many active sentences, ψ_0, ..., ψ_k. An easy induction shows that exactly one of ψ_0,...,ψ_k is true. Indeed, exactly one of φ_0 or φ_0 is true, and hence so is exactly one of φ_0∧𝖢𝗈𝗇(φ_0) and φ_0∧𝖢𝗈𝗇(φ_0). And if θ is true, then so is exactly one of ζ_0:=θ∧φ_k and ζ_1:=θ∧φ_k, and hence so too is exactly one of ζ_0∧𝖢𝗈𝗇(ζ_0) and ζ_1∧𝖢𝗈𝗇(ζ_1).

Let φ_k be a true sentence. At stage k in the construction of 𝒜 there are only finitely many active sentences ψ_0,...,ψ_n. We have already seen that exactly one of ψ_i is true. But then φ_k∧ψ_i is true, (φ_k∧ψ_i⊢φ_k), and (φ_k∧ψ_i) is numerated into 𝒜.


𝒜 contains no true ideals.


An easy induction shows that if ψ_0 and ψ_1 are both active at the same stage, then for any θ, if θ implies both ψ_0 and ψ_1 then θ∈[].

Let φ be a true sentence in 𝒜. By the previous remark, the only sentences in 𝒜 that strictly imply φ are (i) 𝖤𝖠 refutable sentences and (ii) sentences that imply φ∧𝖢𝗈𝗇(φ). Since the Lindenbaum algebra of 𝖤𝖠 is dense, this means there is some ψ such that (φ∧𝖢𝗈𝗇(φ)) strictly implies ψ strictly implies φ but ψ∉𝒜. 


The following questions remain.


Is the relation of cofinal agreement on true sentences an equivalence relation on recursive monotonic operators?



Let f be recursive and monotonic. Suppose that for all consistent φ,

(i) φ∧𝖢𝗈𝗇(φ) implies f(φ) and

(ii) f(φ) implies φ. 

Must f be equivalent to the identity or to 𝖢𝗈𝗇 on a true ideal?


  plain
  





