The Kaufmann--Clote question on end extensions of models of arithmetic and the weak regularity principle
Mengzhou Sun


§ ABSTRACT 
    We investigate the end extendibility of models of arithmetic with restricted elementarity. By utilizing the restricted ultrapower construction in the second-order context, for each n∈ and any countable model of Σ_n+2, we construct a proper Σ_n+2-elementary end extension satisfying Σ_n+1, which answers a question by Clote positively. 
    We also give a characterization of countable models of Σ_n+2 in terms of their end extendibility similar to the case of Σ_n+2. 
    Along the proof, we will introduce a new type of regularity principles in arithmetic called the weak regularity principle, which serves as a bridge between the model's end extendibility and the amount of induction or collection it satisfies.

[
    [
    
=====



§ INTRODUCTION

End extensions are of significant importance and have been studied intensively in the model theory of arithmetic: The classical MacDowell–Specker theorem <cit.> showed that every model of  admits a proper elementary end extension. Around two decades later, Paris and Kirby <cit.> studied the hierarchical version of the MacDowell–Specker theorem for fragments of . In fact, they showed that for countable models, end extendibility with elementarity characterizes the collection strength of the ground model.

    Let M be a countable model of Δ_0. For each n∈, M satisfies Σ_n+2 if and only if M has a proper Σ_n+2-elementary end extension K.

For the left-to-right direction, the theorem above does not explicitly specify what theory the end extension K can satisfy.
This amount of elementarity stated in the theorem already implies KΣ_n, and Paris–Kirby's proof actually indicates that K cannot always satisfy Σ_n+1, since this would imply MΣ_n+3. Moreover,  for each n∈, Cornaros and Dimitracopoulos <cit.> constructed a countable model of Σ_n+2 which does not Σ_n+1-elementarily end extend to any model of Σ_n+1.
So with Σ_n+2-elementarity, the theory that the end extension K may satisfy lies between Σ_n and Σ_n+1, and the following question arises naturally:
[Kaufmann–Clote]
    For n∈, does every countable model MΣ_n+2 have a proper Σ_n+2-elementary end extension KΣ_n+1?

The question was included in the list of open problems in <cit.> edited by Clote and Krajíček.
It was first raised by Clote in <cit.>, where he noted that the same question in the context of models of set theory had been previously posed by Kaufmann in <cit.>.
In the same paper, Clote <cit.> showed that every countable model MΣ_n+2 admits a Σ_n+2-elementary proper end extension to some K M-Σ_n+1, which means all the instances of Σ_n+1:

    x a yϕ(x,y)→ b x a y bϕ(x,y)

where a∈ M while parameters in K are allowed in ϕ(x,y)∈Σ_n+1(K).
Cornaros and Dimitracopoulos <cit.> showed that every countable model MΣ_n+2 has a Σ_n+2-elementary proper end extension KΣ_n+1^-(the parameter-free Σ_n+1-collection).
In this paper, we give an affirmative answer to Question <ref>.

The original proof of Paris–Kirby's theorem is based on a first-order restricted ultrapower construction. The ultrapower is generated by a single element when viewed from the ground model. One can show that, by relativizing the proof of pointwise Σ_n+1-definable models do not satisfy Σ_n+1 (e.g., <cit.>, such ultrapowers always fail to satisfy Σ_n+1 in the question.
To tackle this issue, we expand our model into a second-order structure satisfying _0 and the end extension K will be a second-order restricted ultrapower with respect to that structure.



For us, one of the motivations of studying this question is to find a model-theoretic characterization of (countable) models of Σ_n+2 analogous to Theorem <ref>.
Despite the fact that the extension in Question <ref> is insufficient for characterization, a slight generalization of it will suffice.
We will show that for any countable model MΔ_0+exp,
MΣ_n+2 if and only if M admits a proper Σ_n+2-elementary end extension K MΣ_n+1, whose definition is similar to MΣ_n+1.


The regularity principle is the key to connecting end extensions with the arithmetic theories that the models satisfy.
Through the end extension, we can employ a `nonstandard analysis' style argument to prove certain types of regularity principle in the ground model.
Here we provide an example of such an argument. Notice that KΣ_n+1 plays an crucial role in the proof. 

    For each n∈, let MΔ_0. If M admits a proper Σ_n+2-elementary end extension KΣ_n+1, then M satisfies the following principle:
    
    x y aϕ(x,y)→ y a xϕ(x,y).

    where a∈ M, ϕ(x,y)∈Π_n+1(M) and ∃^ x abbreviates b∃ x>b. 


    Suppose M x y aϕ(x,y), then it is equivalent to a Π_n+1-formula over Σ_n+1. Since both M and K are models of Σ_n+1,
    
    K satisfies the same formula by elementarity.
    Pick some arbitrary d>M in K and let c<a such that Kϕ(d,c). Now for each b∈ M, K x bϕ(x,c) and it is witnessed by d. Transferring each of these formulas back to M by elementarity, we have M x bϕ(x,c) for any b∈ M, which means M xϕ(x,c).

We call the principle above weak regularity principle, and denote it by ϕ.

The proposition above, together with the affirmative answer to Question <ref>, implies that Σ_n+2⊢Π_n+1 for each n∈.



Similar to the argument above, we will show that if the extension K MΣ_n+1, then the ground model M will satisfy some other form of weak regularity principle that implies Σ_n+2.

The paper is organized as follows: 
In Section 2, we present the necessary notations and fundamental facts regarding models of arithmetic
In Section 3 we review the definition of the second-order restricted ultrapower, and state some basic properties of it. 
In Section 4, we provide an affirmative answer to Question <ref> and present the construction of an end extension that characterizes countable models of Σ_n+2 as mentioned above.
In Section 5, we formally introduce the weak regularity principle ϕ, and calibrate its strength within the I-B hierarchy.
Finally, putting the results in Section 4 and Section 5 together, we establish a model-theoretic characterization of countable models of Σ_n+2 analogous to Theorem <ref>.



§ PRELIMINARIES


We assume the reader is familiar with some basic concepts and facts in model theory of first- and second-order arithmetic <cit.>. We reserve the symbol  for the set of standard natural numbers. 

For each n∈, let Σ_n and Π_n be the usual classes of formulas in the arithmetic hierarchy of first-order arithmetic.
Given a model of first-order arithmetic M, a formula is Δ_n over M if it is equivalent to both a Σ_n and a Π_n formula in M, or simply Δ_n if the model involved is clear from the context.

Σ_n∧Π_n is the class of formulas which is the conjunction of a Σ_n- and a Π_n-formula, and Σ_n∨Π_n is defined similarly.
Σ_0(Σ_n) is the closure of Σ_n formulas under Boolean operations and bounded quantification.
Σ_n^0, Π_n^0, Δ_n^0 and Σ_0(Σ_n^0) are their second-order variants respectively.
Given a model of first-order arithmetic M, Δ_n(M) is the class of Δ_n-formulas over M, potentially including parameters from 
M that are not explicitly shown.
Σ_n(M), Π_n(M) are defined similarly, as well as their second-order variants Δ_n^0(M,𝒳), Σ_n^0(M,𝒳) and Π_n^0(M,𝒳) for some model of second-order arithmetic (M,𝒳).
Finally, x… is the abbreviation of bxb….For each n∈, let Σ_n and Σ_n be the collection scheme and the induction scheme for Σ_n formulas respectively. We assume that all the Σ_n include Δ_0, and all the theories considered include ^-, which is the theory of non-negative parts of discretely ordered rings. Σ_n^0 and Σ_n^0 are their second-order counterparts, respectively.

For any element c in some model MΔ_0+exp, we identify c with a subset of M by defining x∈ c to mean the x-th digit in the binary expansion of c is 1.

_0 is the subsystem of second-order arithmetic consisting of Robinson arithmetic, Σ_1^0, Δ_1^0-comprehension, and _0 consists of _0 and a statement asserting that every infinite binary tree has an infinite path.
A tree T in the second-order universe is called bounded if there is a total function f in the second-order universe such that σ(x)<f(x) for any σ∈ T and x<σ. 
It is provable in _0 that every infinite bounded tree has an infinite path <cit.>. For each n∈, every countable model of Σ_n+2^0 admits a countable ω-extension (i.e., an extension only adding second-order objects) to some model satisfying _0+Σ_n+2^0 <cit.>.

Considering extensions of models of arithmetic, we say an extension M⊆ K of models of first-order arithmetic is Σ_n-elementary, if all the Σ_n(M)-formulas are absolute between M and K, and we write M_Σ_n K.
We say an extension M⊆ K is an end extension, if every element of K∖ M is greater than any element of the ground model M.
This is denoted by M⊆_K, or M_,Σ_nK if we also have M_Σ_nK.
Strictly speaking, We view second-order structures as two-sorted first-order structures, so by extensions of second-order structures, we mean extensions of the corresponding two-sorted first-order structures. 
We write (M,𝒳)_Σ_n^0(K,𝒴) if all the Σ_n^0(M,𝒳)-formulas are absolute between the two structures. We say an extension of second-order structures is an end extension if its first-order part is an end extension, and we denote this by (M,𝒳)⊆_(K,𝒴), or (M,𝒳)_,Σ_n^0(K,𝒴) if we also have (M,𝒳)_Σ_n^0(K,𝒴).



§ SECOND-ORDER RESTRICTED ULTRAPOWERS

The second-order restricted ultrapower resembles the usual ultrapower construction in model theory, but instead of working on the class of all subsets of the model and all functions from the model to itself, we only consider the sets and functions in the second-order universe. For completeness, we review the definition and some basic facts about it.
All the results appear in <cit.> except Lemma <ref> and Corollary <ref>. Throughout this section we fix some arbitrary second-order structure (M,𝒳)_0.

    The second-order part of (M,𝒳) forms a Boolean algebra under inclusion and Boolean operations. Let $̆ be an ultrafilter on𝒳such that all the elements of$̆ are cofinal in M, and  be the class of all the total functions from M to M in 𝒳. Define an equivalence relation ∼ on  by 
    
    f∼ g{i∈ M| f(i)=g(i)}∈,̆

    where f,g∈.
    The second-order restricted ultrapower of M, denoted by , is the set of equivalence classes [f] for f∈ modulo ∼.
    The interpretations of symbols in the language of first-order arithmetic are defined similarly:
    
    [f]+[g]=[f+g],

    
    [f]×[g]=[f× g],

    
    [f]<[g]{i∈ M| f(i)<g(i)}∈.̆

    Here f+g and f× g are the pointwise sum and product of f and g as functions.
    M naturally embeds into  by identifying elements of M with constant functions.
    Moreover,  is a proper extension of M since the equivalence class of identity function of M is greater than any equivalence class of constant function.
     admits a natural second-order expansion inherited from 𝒳, namely for A∈𝒳 and [f]∈, we define
    
    [f]∈ A{i∈ M| f(i)∈ A}∈.̆

    We denote the expanded structure of the ultrapower by (,𝒳).
    It is easy to show that for i∈ M and A∈𝒳, i∈ A holds in (M,𝒳) if and only if it holds in (,𝒳), so we may view (,𝒳) as an extension of (M,𝒳), where the second-order part is an injection. 

The first-order restricted ultrapower is defined similarly, but with  and $̆ replaced by the corresponding first-order definable classes.
For example, theΔ_1ultrapower uses the class ofΔ_1-definable subsets andΔ_1-definable total functions. 

From now on we also fix an ultrafilter$̆ on 𝒳 such that all the elements of $̆ are cofinal inM.

Generally, Ł oś's theorem does not hold for restricted ultrapowers, but a restricted version of it does hold:


    Let (,𝒳) be the second-order restricted ultrapower. Then the following holds:
    
  *  If ϕ( x) is a Σ_1^0(M,𝒳)-formula, then 
        
    (,𝒳)ϕ([f])∃A∈, A⊆{i∈ M| (M,𝒳)ϕ(f(i))}.

  *  If ϕ( x) is a Δ_1^0(M,𝒳) formula over (M,𝒳), then 
        
    (,𝒳)ϕ([f]){i∈ M| (M,𝒳)ϕ(f(i))}∈.̆

    Here the right-hand side makes sense in view of Δ_1^0-comprehension of (M,𝒳). (M,𝒳)_Σ_2^0(,𝒳).

    Let (M,𝒳) x yψ(x,y) for some ψ(x,y)∈Δ_0^0(M,𝒳). By picking the least witness y of ψ(x,y), we may assume ψ(x,y) defines a total function f∈, so (M,𝒳)ψ(x,f(x)) for all x∈ M. In particular, for each g∈,
    
    (M,𝒳)ψ(g(x),f∘ g(x)).

    Here f∘ g is the composition of f and g. By restricted Ł oś's theorem, (,𝒳)ψ([g],[f∘ g]) for each [g]∈, so that (,𝒳) x yψ(x,y).

    
    We say $̆ is additive if wheneverf∈is bounded, then there is ac∈ Msuch that{i∈ M| f(i)=c}∈$̆.

    If $̆ is additive, thenis an end extension ofM.

    If [f]<b for some b∈ M, then we may define 
    
    g(i)=
    			0,    if f(i)≥ b.
    
                f(i),    if f(i)<b.
[g]=[f] and g is a total bounded function in 𝒳. The additiveness of $̆ implies that there isc∈ Msuch that{i∈ M| g(i)=c}∈$̆, that is, [g]=[f]=c.

The following lemma and corollary enable us to transfer the comprehension in(M,𝒳)into the ultrapower viaΣ_2^0-elementarity, and reduce the case ofΣ_n+2toΣ_2^0uniformly in the construction of our main result. 
    For each n≥ 1, if (M,𝒳) satisfies Σ_n-comprehension, then each instance of Σ_n- and Π_n-comprehension in (M,𝒳) transfers to (,𝒳). Formally speaking, for any first-order formula ϕ(x) in Σ_n(M) or Π_n(M), if there is some A∈𝒳 such that
    
    (M,𝒳) x(x∈ A↔ϕ(x)),

    then (,𝒳) x(x∈ A↔ϕ(x)) as well.
    

    We prove the statement for all the ϕ(x) in Σ_k(M) and Π_k(M) simultaneously by induction on k≤ n.
    For k=1, let ϕ(x) be any formula in Σ_1(M) or Π_1(M), then x(x∈ A↔ϕ(x)) is a Π_2^0(M,𝒳)-formula, so the same holds in (,𝒳) by Corollary <ref>. For the induction step, suppose the statement holds for all the formulas in Σ_k(M) and Π_k(M), and take any ϕ(x):= yψ(x,y)∈Σ_k+1(M) where ψ(x,y)∈Π_k(M). By Σ_n-comprehension in (M,𝒳), there exist A,B∈𝒳 such that
    
    (M,𝒳) x(x∈ A↔ yψ(x,y)),

    (M,𝒳)⟨ x,y⟩(⟨ x,y⟩∈ B↔ψ(x,y)).

    By induction hypothesis, the second clause transfers to (,𝒳). We also have the following relation of A and B from the two statements above:
    
    (M,𝒳) x(x∈ A↔ y⟨ x,y⟩∈ B).

    This fact also transfers to (,𝒳) by Corollary <ref>. 
    Putting the two statements in (,𝒳) together, we have
    
    (,𝒳) x(x∈ A↔ yψ(x,y)).

    The case for ϕ(x)∈Π_k+1(M) is exactly the same. This completes the induction.
 
    If (M,𝒳) satisfies Σ_n-comprehension for some n∈, then M_Σ_n+2 as an extension between models of first-order arithmetic.
    

    Let M x  yψ(x,y) for some ψ(x,y)∈Π_n(M). Take A∈𝒳 such that 
    
    (M,𝒳)⟨ x,y⟩(⟨ x,y⟩∈ A↔ψ(x,y)),

    (M,𝒳) x y⟨ x,y⟩∈ A.

    By Lemma <ref> and Corollary <ref>, both formulas hold in (,𝒳), which implies (,𝒳) x  yψ(x,y).
    
    
    
    
    
    


§ CONSTRUCTIONS OF END EXTENSIONS

In this section, we present the constructions of end extensions by the second-order ultrapower.


We first answer Question <ref> affirmatively. In view of Corollary <ref>, we only need to deal with the case for the base level in the second-order context.

    For any countable model (M,𝒳)Σ_2^0+_0, there is a proper end extension (M,𝒳)_,Σ_2^0(K,𝒳)Σ_1^0.

We will give two proofs: The first proof is suggested by Tin Lok Wong. We ensure that the second-order ultrapower satisfiesΣ_1^0by properly embedding it into a coded ultrapower as an initial segment;
the second proof guaranteesΣ_1^0directly in the construction of the ultrafilter._0plays a central role in both constructions.

    Following the construction in <cit.>, by an iterated arithmetic completeness theorem within (M,𝒳), there is an end extension M⊆_LΔ_0 such that 𝒳=_M(L).
    We build a coded ultrapower with respect to both M and L. Let
    
    ={g∈ L| g codes a total function from M to L},

    ={f∈ L| f  codes a total function from M to M},

    and $̆ be an ultrafilter on𝒳. Following the construction by Paris and Kirby <cit.>, let/$̆ be the coded ultrapower with respect to  and $̆.
    Similar to the second-order ultrapower, coded ultapowers also satisfy restricted Ł oś's theorem forΔ_0-formulas and thusL_Δ_0/$̆.
    Moreover, /$̆ is a cofinal extension ofL, as each element[g]∈/$̆ is bounded by its code g∈ L.
    So L_Σ_1/$̆ and in particular,/Δ_0.
    
    Since⊆,is a substructure of/$̆.
    On the other hand, since 𝒳=_M(L),  is isomorphic to a second-order ultrapower with respect to 𝒳 and $̆, so(M,𝒳)_,Σ_2^0(,𝒳).
    
     
    We want to pick a sufficiently generic ultrafilter$̆, such that both M and  are proper initial segments of 𝒢/$̆.
    We construct$̆ in countably many stages. For each k∈ we construct some A_k∈𝒳 that is cofinal in M, and A_k⊇ A_k+1.
    We enumerate all the pairs ⟨ f,g⟩ such that f∈ and g∈𝒢 as {⟨ f_k,g_k⟩}_k∈, and all the functions in  bounded by some b∈ M as {h_k}_k∈.Stage 0: Let A_0=M.Stage 2k+1(⊆_/$̆): Consider 
    
    A=A_2k∩{x∈ M| L g_k(x)<f_k(x)}.

    SinceLΔ_0,A∈_M(L)=𝒳.
    IfAis cofinal inM, then letA_2k+1=A. Otherwise letA_2k+1=A_2kand move on to the next stage.Stage 2k+2(M⊆_): Assumeh_kis bounded byb∈ M.
    Then
    
    (M,𝒳) x y b(x∈ A_2k+1∧ h_k(x)=y).

    Since(M,𝒳)Σ_2^0, there is somec<bsuch that 
    
    {x∈ M| (M,𝒳) x∈ A_2k+1∧ h_k(x)=c}

    is cofinal inM. Let this set beA_2k+2and move on to the next stage.
    Finally, let=̆{A∈𝒳| k  A_k⊆ A}. It is not hard to see that$̆ is an ultrafilter and each element of $̆ is cofinal inM. This completes the construction of$̆.Verification: We verify that M⊆_⊆_/$̆. For⊆_/$̆, fix any g∈.
    For each f∈, take k∈ such that ⟨ f_k,g_k⟩=⟨ f,g⟩.
    At stage 2k, if 
    
    A=A_2k∩{x∈ M| g(x)<f(x)}

    is cofinal in M, then {x∈ M| g(x)<f(x)}∈$̆.
    Letĝ∈𝒢be defined by 
    
    ĝ(x)=
    			g(x),    if g(x)< f(x).
    
                0,    if g(x)≥ f(x).

   Then[ĝ]∈and[g]=[ĝ]in/$̆. Otherwise, if A is bounded in M, then we are forced to have {x∈ M| g(x)≥ f_k(x)}∈$̆. By the restricted Ł oś's theorem in/$̆, /[g]>[f_k]. So  is an proper initial segment of /$̆, which implies(,_(/)̆)Σ_1^0.
   
   ForM⊆_, supposeh∈is bounded. Then, takek∈such thath=h_k, and at stage2k+2the choice ofA_2k+2forces{x∈ M| (M,𝒳) h(x)=c}∈$̆ for some c∈ M. So $̆ is additive with respect to, andM⊆_by Lemma <ref>.
   For eachA∈𝒳, leta∈ Lbe the element that codesA⊆ M. By the restricted Ł oś's theorem forΔ_0-formulas in bothand/$̆, it is not hard to prove that for each f∈, 
    
    (,𝒳) [f]∈ A(/,̆𝒳) [f]∈ a.

    So we may embed the second-order part 𝒳 of (,𝒳) into _(/)̆.
    Since (,_(/)̆)Σ_1^0, we have (,𝒳)Σ_1^0.

    For each n∈ and any countable model MΣ_n+2, there is a Σ_n+2-elementary proper end extension M_,Σ_n+2KΣ_n+1.

    We first expand M to a second-order structure satisfying Σ_2^0 by adding all the Σ_n-definable sets into the second-order universe, then we further ω-extend it to some countable (M,𝒳)Σ_2^0+_0. By Theorem <ref>, there is an ultrapower (M,𝒳)_,Σ_2^0(,𝒳) which satisfies Σ_1^0. Since all the Σ_n-definable sets of M are in 𝒳, (M,𝒳) satisfies Σ_n-comprehension and M_,Σ_n+2 by Corollary <ref>.
    
    For Σ_n+1, suppose x [g] yθ(x,y,[f]) for some [g]∈ and θ∈Π_n where [f]∈ is the only parameter in θ.
    By Π_n-comprehension in M, let A∈𝒳 such that 
    
    (M,𝒳)⟨ x,y,z⟩ (⟨ x,y,z⟩∈ A↔θ(x,y,z)).
(,𝒳) satisfies the same formula by Lemma <ref>, and thus
    
    (,𝒳) x [g] y⟨ x,y,[f]⟩∈ A.

    By Σ_1^0 in (,𝒳),
    
    (,𝒳) b x [g] y b⟨ x,y,[f]⟩∈ A,
which means b x [g] y bθ(x,y), so Σ_n+1.

Yet simple, this construction does not reveal a syntactical proof ofΣ_n+2⊢Π_n+1. We make(,𝒳)Σ_1^0by embedding it into a larger ultrapower/$̆ as an initial segment, and the core argument is wrapped inside the construction of /$̆.
Here we present another construction that directly guarantees each instance ofΣ_1^0in the ultrapower, and hence provide more insights. The construction relies on a simple yet powerful lemma resulting from_0, which states that if aΠ_1^0-definable bounded multi-valued function is total, then we may select a single-valued choice function of it within the second-order universe.
The lemma also leads to a syntactical proof ofΣ_n+2⊢Π_n+1.
 
    Fix a model (M,𝒳)_0. Let θ(x,y,z)∈Δ_0^0(M,𝒳). If (M,𝒳) x yf(x) zθ(x,y,z) for some total function f∈𝒳, then there is a total function P∈𝒳 such that:
        
    (M,𝒳) x(P(x)<f(x)∧ zθ(x,P(x),z)).

    Consider the following tree T which is Δ_1^0-definable in (M,𝒳):
    
    σ∈ Tx,zσ(σ(x)<f(x)∧θ(x,σ(x).z))

Obviously T is bounded by f, so we only need to show that T is infinite.
Let F(x)=max_x'< xf(x'). 
For any x∈ M, by Σ_1^0, let σ_x∈ M be a coded sequence of length x such that for any x'<x and y'<F(x),

    σ_x(x')=y' (M,𝒳) zθ(x',y',z)∧ w y' zθ(x',w,z).


Then we have

    (M,𝒳)x'x z(σ_x(x')<f(x)∧θ(x',σ_x(x'),z)).
 
This means σ_x is an element of T of length x, so T is infinite.
By _0, take an infinite path P of T. Clearly P satisfies the two requirements above.

    We construct an ultrafilter $̆ on𝒳inωmany stages. 
    Along the construction, we gradually guarantee that the ultrapower(,𝒳)Σ_1^0and$̆ is additive.
    Enumerate all the triples {⟨ z θ_k(x,y,z),f_k, g_k⟩}_k∈, where θ_k(x,y,z)∈Δ_0^0(M,𝒳) and f_k,g_k are total functions in 𝒳, and enumerate all the bounded total functions in 𝒳 as {h_k}_k∈. For each k∈, at stage k we construct a cofinal set A_k∈𝒳 such that A_k⊇ A_k+1 for all k∈, and the resulting ultrafilter =̆{A∈𝒳|k A⊇ A_k}.Stage 0: Set A_0=M∈𝒳.Stage 2k+1((,𝒳)Σ_1^0):
    At these stages we want to guarantee the following instances of Σ_1^0:
    
    y[g_k] zθ_k([f_k],y,z)→ by[g_k]zbθ_k([f_k],y,z).

    The general idea is that we first try to `force' the consequent of above implication to be true in (,𝒳). If we succeed, then the entire statement is true. Otherwise, we apply Lemma <ref> to argue that the antecedent is already guaranteed to be false in the ultrapower.
    Consider the Σ_1^0-definable set 
    
    A=A_2k∩{x∈ M| byg_k(x)zbθ_k(f_k(x),y,z)}.

    If it is cofinal in M, then there is a cofinal subset A^*∈𝒳 of A by Hájek–Pudlák <cit.>. Let A_2k+1=A^* and proceed to stage 2k+2. If A is not cofinal in M, we let A_2k+1=A_2k and proceed directly to stage 2k+2.Stage 2k+2(Additiveness of $̆): This part is exactly the same as the construction of stage2k+2in the first proof of Theorem <ref>.
    
    
    
    
    
    Finally, let=̆{A∈𝒳| k A⊇ A_k}. It is not hard to see that$̆ is an ultrafilter, and each element of $̆ is cofinal inM. This completes the whole construction. Verification: Let(,𝒳)be the corresponding second-order restricted ultrapower. We show that(M,𝒳)_,Σ_2^0(,𝒳)and(,𝒳)Σ_1^0. The elementarity is given by Corollary <ref>.(M,𝒳)⊆_(,𝒳)follows from the exact same reasoning as in the first proof of Theorem <ref>. For(,𝒳)Σ_1^0, consider an arbitrary instance ofΣ_1^0in(,𝒳):
    
    y[g] zθ([f],y,z)→ by[g]zbθ([f],y,z),

    whereθ∈Δ_0^0(M,𝒳). Here without loss of generality, we assume there is only one first-order parameter[f]∈inθ. 
    Assume at stage2k+1, we enumerate⟨ z θ_k(x,y,z),f_k, g_k⟩=⟨ zθ(x,y,z),f,g⟩, andA_2k∈𝒳is the cofinal subset ofMwe obtained from the previous stage.
    Suppose we are in the first case of the construction in this stage, i.e.,
    
    A=A_2k∩{x∈ M| byg(x)zbθ(f(x),y,z)}

    is cofinal inM, then by the construction there exists someA^*⊆ Ain$̆. By restricted Ł oś's theorem, (,𝒳) by[g]zbθ([f],y,z), so the instance of Σ_1^0 is true. If we are in the second case, assuming A is bounded by d∈ M, then
    
    (M,𝒳) x d(x∈ A_2k→ b y g(x) z bθ(f(x),y,z)).

    By Σ_1^0 in M, this fact is equivalent to: 
    
    (M,𝒳)xdyg(x)(x∈ A_2k→ zθ(f(x),y,z)).

    By Lemma <ref>, there is a total function P∈𝒳 such that 
    
  * (M,𝒳)xd P(x)<g(x).
  * (M,𝒳)xd (x∈ A_2k→ zθ(f(x),P(x),z) ).
    The first clause implies (,𝒳) [P]<[g] by restricted Ł oś's theorem. Suppose (,𝒳) zθ([f],[P],z), then by restricted Ł oś's theorem for Σ_1^0 formulas, there is some A'∈$̆ such thatA'⊆{x∈ M| zθ(f(x),P(x),z)}, but by the second clause,A'∩ A_2kis bounded byd, which contradictsA'∩ A_2k∈$̆. So (,𝒳) zθ([f],[P],z), and the instance of Σ_1^0 considered is vacuously true.



We now proceed to the construction of end extensions for characterizing countable models ofΣ_n+2. We first defineK MΣ_n+1for an end extensionM_ K, and introduce some equivalent definitions of it.

    For each n∈, let M,K be models of Δ_0+exp and M⊆_ K.
        We say K MΣ_n+1 if for any ϕ(x)∈Σ_n+1(K) and a∈ M,
        
    Kϕ(0)∧ x a(ϕ(x)→ϕ(x+1))→ x aϕ(x).

    Notice that we allow parameters in K in ϕ while the bound a must be in M.

    For each n∈, let M be a model of Δ_0+exp, KΣ_n and M⊆_ K, then the following are equivalent:
    
  * K MΣ_n+1.
        
  * 
        For any ϕ(x)∈Σ_n+1(K) and a∈ M,
        
    K cx a(ϕ(x)↔ x∈ c).

  * 
        For any θ(x,y)∈Π_n(K) and a∈ M,
        
    K b x a( yϕ(x,y)↔ y bθ(x,y)).

    We show lem:equivMind:1⇔lem:equivMind:2 and lem:equivMind:2⇔lem:equivMind:3. 
    For lem:equivMind:1⇒lem:equivMind:2, first by modifying a standard argument, one can show that lem:equivMind:1 implies the least number principle for Π_n+1-formulas that is satisfied by some element of M.
    Then we pick the least c<2^a∈ M such that 
    
    K x a(ϕ(x)→ x∈ c).

    Such c will code ϕ(x) for x<a by the minimality of c.
    For lem:equivMind:2⇒lem:equivMind:1, take the code c of ϕ(x) below a∈ M. Then, one can prove the instance of MΣ_n+1 for ϕ(x) by replacing ϕ(x) with x∈ c and applying KΔ_0.
    For lem:equivMind:2⇒lem:equivMind:3, take the code c of {x<a| K yθ(x,y)} by lem:equivMind:2. Consider the Σ_n+1-formula
    
    Φ(v):= b x v(x∈ c↔ y bθ(x,y)).

    It is not hard to show that KΦ(0)∧ v(Φ(v)→Φ(v+1)).
    By MΣ_n+1 (from lem:equivMind:2⇒lem:equivMind:1) we have KΦ(a), which implies lem:equivMind:3. For lem:equivMind:3⇒lem:equivMind:2, let ϕ(x):= yθ(x,y) for some θ∈Π_n(K). 
    By lem:equivMind:3, there is some b∈ K such that
    
    K x a( yθ(x,y)↔ y bθ(x,y)).

    By Σ_n in K, there is some c∈ K that codes {x<a| K y bθ(x,y)}. Such c will serve as the witness for lem:equivMind:2.

    For any countable model (M,𝒳)Σ_2^0, there is a proper end extension (M,𝒳)_,Σ_2^0(K,𝒳) such that for any Σ_1^0(K,𝒳)-formula ϕ(z) and a∈ M, the set {z<a| (K,𝒳)ϕ(z)} is coded in K.

    The construction is a mild generalization of the construction in <cit.>. 
    
    We make the ultrapower (,𝒳) satisfy the coding requirement by maximizing each Σ_1^0-definable subset of  that is bounded by some element of M.

    Enumerate all the pairs {⟨ yθ_k(x,y,z),a_k⟩}_k∈ where θ_k(x,y,z)∈Δ_0^0(M,𝒳) and a_k∈ M, and enumerate all the bounded total functions in 𝒳 as {h_k}_k∈.
    At each stage k we construct a cofinal set A_k∈𝒳 such that A_k⊇ A_k+1 for all k∈, and the resulting ultrafilter =̆{A∈𝒳|k A⊇ A_k}.
    
    Stage 0: Let A_0=M.Stage 2k+1(coding Σ_1^0 sets): Consider the following Π_2^0-formula where c<2^a_k:
    
    x(x∈ A_2k∧ z c yθ_k(x,y,z)).

    By (M,𝒳)Σ_2^0, there exists a maximal c_0<2^a_k satisfying the formula above.
    Similar to the alternative proof of Theorem <ref>, let A_2k+1∈𝒳 be a cofinal subset of the following Σ_1^0-definable subset of M:
    
    {x∈ M| (M,𝒳) x∈ A_2k∧ z c_0 yθ_k(x,y,z)}.
Stage 2k+2 (Additiveness of $̆): This part is exactly the same as stage2k+2in the proof of Theorem <ref>.
    
    
    
    
    
    Finally, let=̆{A∈𝒳| k A⊇ A_k}. It is not hard to see that$̆ is an ultrafilter, and each element of $̆ is cofinal inM. This completes the whole construction.
    
    Verification: Let(,𝒳)be the corresponding second-order restricted ultrapower.(M,𝒳)_,Σ_2^0(,𝒳)follows in exactly the same way as in Theorem <ref>.
    

    For the coding requirement of(,𝒳), consider anyΣ_1^0-formula yθ([f],y,z)whereθ∈Δ_0^0(,𝒳)and[f]∈is the only first-order parameter ofθ.
    For anya∈ M, assume for somek∈, at stage2k+1we enumerate the pair⟨ yθ(f(x),y,z),a⟩. We show that the maximalc_0∈ Mwe obtained in the construction codes{z<a| (,𝒳) yθ([f],y,z)}.

    For eachz<asuch thatz∈ c_0, sinceA_2k+1is a subset of{x∈ M| (M,𝒳) yθ(f(x),y,z)},(,𝒳) yθ([f],y,z)by restricted Ł oś's theorem forΣ_1^0-formulas.
    On the other hand, for eachz'<asuch thatz'∉ c_0, if(,𝒳) yθ([f],y,z'), then by restricted Ł oś's theorem forΣ_1^0-formula again there is someB∈$̆ such that
    
    B⊆{x∈ M| (M,𝒳) yθ(f(x),y,z')}.

    Since B∩ A_2k+1∈$̆ is still cofinal inM, we have
    
    x(x∈ A_2k∧ z c_0∪{z'} yθ(f(x),y,z)),

    which contradicts the maximality ofc_0in the construction.
    So(,𝒳) yθ([f],y,z').

    For each n∈ and any countable model MΣ_n+2, there is an Σ_n+2-elementary proper end extension M_,Σ_n+2K MΣ_n+1.

    The proof is mostly the same as Theorem <ref>. 
    We expand M to a second-order structure (M,𝒳) satisfying Σ_2^0+_0 by adding all the Δ_n+1-definable subsets of M into the second-order universe.
    Such (M,𝒳) satisfies Σ_n-comprehension.
    By Theorem <ref>, there exists a second-order ultrapower extension (M,𝒳)_,Σ_2^0(,𝒳) that codes all the Σ_1^0-definable subset bounded by some element of M. Since all the Σ_n-definable sets of M are in 𝒳, (M,𝒳) satisfies Σ_n-comprehension and M_,Σ_n+2 by Corollary <ref>. 
    
    For M Σ_n+1, we only need to show that  satisfies condition lem:equivMind:3 in Lemma <ref>. 
    Let ϕ(x):= yθ(x,y,[f]) be any Σ_n+1-formula, where θ∈Π_n and [f]∈ is the only parameter in θ, and a be some element of M. Since (M,𝒳) satisfies Σ_n-comprehension, there is some A∈𝒳 such that 
    
    (M,𝒳)⟨ x,y,z⟩ (⟨ x,y,z⟩∈ A↔θ(x,y,z)).

    The same formula holds in (,𝒳) by Lemma <ref>, and thus
    
    (,𝒳) x( y⟨ x,y,[f]⟩∈ A↔ϕ(x)).

    There is some c∈ K that codes {x<a| (,𝒳) y⟨ x,y,[f]⟩∈ A}.
    Such c will also code {x<a|ϕ(x)}.  
    
    
    
    
    


§ THE WEAK REGULARITY PRINCIPLE

In the final section we provide an application of Lemma <ref>: We introduce the weak regularity principleϕ, a variant of the regularity principle, and determine its strength within the I-B hierarchy. One of the main application is to prove the converse of Theorem <ref>, and give a model-theoretic characterization of countable models ofΣ_n+2analogous to Theorem <ref>.

Mills and Paris <cit.> introduced the regularity principleϕto be the universal closure of the following formula:

    x yaϕ(x,y)→ y a  xϕ(x,y).

For any formula classΓ, let

    Γ=Δ_0∪{ϕ|ϕ∈Γ}.

It is also shown in <cit.> thatΠ_n⇔Σ_n+1⇔Σ_n+2for eachn∈.

The weak regularity principle is defined by replacing the∃^ xby∀ xin the antecedent of implication inϕ. 

    Let ϕ(x,y) be a formula in first-order arithmetic with possibly hidden variables. The weak regularity principleϕ denotes the universal closure of the following formula:
    
    x yaϕ(x,y)→ya xϕ(x,y).

    For any formula class Γ, define 
    
    Γ=Δ_0∪{ϕ|ϕ∈Γ}.

The strength of the weak regularity principle behaves more complicated within the arithmetic hierarchy compared to the regularity principle.
The principle for most of the natural class of formulas correspond to collection schemes, whereas induction schemes are only equivalent to the principle for a highly restricted subclass ofΣ_0(Σ_n+1)-formulas.  

We will show that for eachn∈,Σ_0(Σ_n),Σ_n+1,Π_n+1and(Σ_n+1∨Π_n+1)are all equivalent toΣ_n+2,

and(Σ_n+1∧Π_n+1)is equivalent toΣ_n+2.

The weak regularity principle may also be viewed as an infinitary version of the pigeonhole principle, and similar phenomenon arises with the strength of pigeonhole principle in the I-B hierarchy.
Dimitracopoulos and Paris <cit.> proved thatΣ_n+1andΠ_n+1are equivalent toΣ_n+1.(Σ_n+1∨Π_n+1)andΣ_0(Σ_n+1)are equivalent toΣ_n+1.




     For each n∈, Σ_n+2⊢Π_n+1.
     

    We only show the case of n=0 and the rest can be done by relativizing to the Σ_n universal set. Let MΣ_2, we first expand M to a second-order structure (M,𝒳)Σ_2^0+_0.
    Let ϕ(x,y):= z θ(x,y,z) for some θ∈Δ_0.  
    Suppose M x yaϕ(x,y). By applying Lemma <ref> with θ and f(x) ≡ a as a constant function, we obtain some total function P∈𝒳 such that (M,𝒳) x(P(x)<a∧ zθ(x,P(x),z)). By Σ_2^0, there is some y_0<a such that there are infinitely many x satisfying P(x)=y_0, which implies M y a x ϕ(x,y). So MΠ_1.

    For each n∈, Σ_n+2⊢(Σ_n+1∨Π_n+1).

    Fix n∈ and let MΣ_n+2, ϕ(x,y)∈Σ_n+1(M) and ψ(x,y)∈Π_n+1(M). Suppose M x y a(ϕ(x,y)∨ψ(x,y)) for some a∈ M.
    
    If M x b y aψ(x,y) for some b∈ M, then by Lemma <ref>, M x y aψ(x,y) and the conclusion holds.
    Otherwise M x y aϕ(x,y), then by Σ_n+1, M y a xϕ(x,y) and the conclusion holds again.

    There is also a direct model-theoretic proof similar to Proposition <ref>. One only need to notice that over Σ_n+1, x y a(ϕ(x,y)∨ψ(x,y)) is equivalent to a Π_n+2-formula.
    
    
    
    

    For each n∈, (Σ_n∧Π_n)⊢Σ_n+1.

    We prove for each k≤ n, Σ_k+(Σ_n∧Π_n)⊢Σ_k+1, and the lemma follows by induction.
    Let MΣ_k+(Σ_n∧Π_n), suppose MΣ_k+1, then there is a proper cut I⊆ M defined by ϕ(y):= xθ(x,y), where θ(x,y)∈Π_k(M). Let μ(x,y):=y' yx' xθ(x',y'). Then μ(x,y)∈Π_k(M) over Σ_k and ϕ^*(y)= xμ(x,y) also defines a cut J⊆ I.
    J is closed under successor by its definition.
    For any x∈ M, if Mμ(x,y) for all y∈ J, then y∈ J is defined by μ(x,y) in M, which contradicts MΣ_k. So for each x∈ M, we may take the largest y∈ J satisfying μ(x,y) by Σ_k. Fixing some arbitrary a>J, we have 
    
    M x y a(μ(x,y)∧μ(x,y+1)).

    Applying (Σ_n∧Π_n), there is some y_0<a such that
    
    M x(μ(x,y_0)∧μ(x,y_0+1)).

    By the definition of μ(x,y), this implies y_0∈ J and y_0+1∉ J, which contradicts the fact that J is a proper cut of M closed under successor.
    So MΣ_k+1.

    For each n∈, Σ_0(Σ_n)⊢Σ_n+2.

    Let MΣ_0(Σ_n). We show MΠ_n, which is equivalent to Σ_n+2. 
    By Lemma <ref>, MΣ_n+1.
    Suppose M x  y a ϕ(x,y) for some ϕ∈Π_n(M), and without loss of generality, we assume M y aϕ(0,y).
    For each z∈ M, we find the largest x<z such that M y aϕ(x,y), and `color' z by the witness y. Formally,
    
    M z y a x z(ϕ(x,y)∧x'(x,z) y aϕ(x',y)),

    where (x,z) refers to the open interval between x and z.
    By Σ_0(Σ_n), 
    
    M y a z x z(ϕ(x,y)∧x'(x,z) y aϕ(x',y)).

    which implies M y a xϕ(x,y).

    For each n∈, Σ_0(Σ_n)⇔(Σ_n+1∨Π_n+1)⇔Σ_n+2.
Σ_0(Σ_n)⊢Σ_n+2 follows from Lemma <ref>. Σ_n+2⊢(Σ_n+1∨Π_n+1) follows from Corollary <ref>. (Σ_n+1∨Π_n+1)⊢Σ_0(Σ_n) is trivial.

There is an analog of Proposition <ref> forM_,Σ_n+2K MΣ_n+1and(Σ_n+1∧Π_n+1). It also leads to a model-theoretic proof ofΣ_n+2⊢(Σ_n+1∧Π_n+1).

    Let MΔ_0+exp. For each n∈, if there is a proper Σ_n+2-elementary end extension M_,Σ_n+2K MΣ_n+1, then M(Σ_n+1∧Π_n+1). 

    Let θ(x,y,z)∈Σ_n(M), σ(x,y,w)∈Π_n(M) and ϕ(x,y):= zθ(x,y,z)∧ wσ(x,y,w)∈Σ_n+1∧Π_n+1. Suppose M x y aϕ(x,y) for some a∈ M. 
    Over Σ_n+1, it is equivalent to the following Π_n+2 formula 
    
    x  b y a( z bθ(x,y,z)∧ wσ(x,y,w)).

    So both M and K satisfy the formula above by elementarity. Pick some arbitrary d∈ K∖ M, then
    
    K b y a( z bθ(d,y,z)∧ wσ(d,y,w)).

    By Lemma <ref>lem:equivMind:2, there is some b∈ K such that 
    
    K y a( zθ(d,y,z)↔ z bθ(d,y,z)),

    which implies
    
    K y a( zθ(d,y,z)∧ wσ(d,y,w)).

    Pick a witness c<a in M such that K zθ(d,c,z)∧ wσ(d,c,w), i.e., Kϕ(d,c). Now for each b∈ M, K x bϕ(x,c), where this is witnessed by d. Transferring each of these formulas to M, we have M x bϕ(x,c) for any b∈ M, i.e., M xϕ(x,c).

    For each n∈, (Σ_n+1∧Π_n+1)⇔Σ_n+2.
(Σ_n+1∧Π_n+1)⊢Σ_n+2 follows from Lemma <ref>. For the other direction, given any countable model MΣ_n+2, there is a proper end extension M_,Σ_n+2K MΣ_n+1 by Theorem <ref>, and then M(Σ_n+1∧Π_n+1) by Proposition <ref>.

    In Hájek-Pudlák <cit.> it was shown that every Σ_0(Σ_n+1)-formula has the following normal form:
    
    1u_1v_1…ku_kv_kΨ(u_1… u_k,v_1… v_k,w_1… w_l).

    where k,l∈, each Q_k is either ∀ or ∃, Ψ is a Boolean combination of Σ_n+1-formulas and the variable sets {u_i}_i≤ k, {v_i}_i≤ k and {w_i}_i≤ l are pairwise disjoint.  

    Our proof of Proposition <ref> can be refined to show that Σ_n+2⊢ϕ, where ϕ(x,y)∈Σ_0(Σ_n+1), and if written in the normal form above, x does not appear in {v_i}_i≤ k, i.e., x is not permitted to appear in the bound of any bounded quantifiers. 
    
    In contrast, the instance ϕ(z,y) of Σ_0(Σ_n) we used to prove Σ_n+2 in Lemma <ref> starts with ∃ x<z explicitly.

Finally, we establish the characterization of countable models ofΣ_n+2as promised.

    Let M be a countable model of Δ_0. For each n∈, M satisfies Σ_n+2 if and only if M admits a proper Σ_n+2-elementary end extension K MΣ_n+1.

    The direction from left to right follows by Theorem <ref>. For the other direction, if M_,Σ_n+2K MΣ_n+1, then M(Σ_n+1∧Π_n+1) by Proposition <ref>, and thus MΣ_n+2 by Theorem <ref>. 


The main remaining problem now is to find a purely syntactic proof of Theorem <ref>. We conjecture that a more refined tree construction similar to the approach in Lemma <ref> would solve the problem.

   Give a direct proof of Σ_n+2⊢(Σ_n+1∧Π_n+1) (and also Σ_n+2⊢ϕ where ϕ(x,y)∈Σ_0(Σ_n+1) as described in the remark above) without using end extensions.


§ ACKNOWLEDGEMENT

The author's research was partially supported by the Singapore Ministry of Education Tier 2 grant AcRF MOE-000538-00 as well as by the NUS Tier 1 grants AcRF R146-000-337-114 and R252-000-C17-114. This work is contained in the author's Ph.D. thesis. I would like to thank my two supervisors Tin Lok Wong and Yue Yang for their guidance, encouragement and helpful discussions.

I am also indebted to Leszek A. Koł odziejczyk for carefully reading drafts of the paper and providing many helpful suggestions.

plain