BRICS RS-94-23 S. Riis: Finitisation in Bounded Arithmetic

BRICS

Basic Research in Computer Science

Finitisation in Bounded Arithmetic

S�ren Riis

BRICS Report Series RS-94-23 ISSN 0909-0878 August 1994 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1994, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

Finitisation in Bounded Arithmetic

Søren Riis^{∗} ; BRICS^{†}

June 1994

Abstract

I prove various results concerning undecidability in weak fragments of Arithmetic. All results are concerned with S_{2}^{1} ⊆ T_{2}^{1} ⊆ S_{2}^{2} ⊆ T_{2}^{2} ⊆ .... a hierarchy of theories which have already been intensively studied in the literature. Ideally one would like to separate these systems. However this is generally expected to be a very deep problem, closely related to some of the most famous open problems in complexity theory.

In order to throw some light on the separation problems, I consider the case where the underlying language is enriched by extra relations and function symbols. The paper introduces a new type of results. These state that the first three levels in the hierarchy (i.e. S_{2}^{1}, T_{2}^{1} and S_{2}^{2}) are never able to distinguish (in a precise sense) the “finite” from the “infinite”. The fourth level (i.e. T_{2}^{2}) in some cases can make such a distinction. More precisely, elementary principles from finitistical combinatorics (when expressed solely by the extra relation and function symbols) are only provable on the first three levels if they are valid when considered as principles of general (infinitistical) combinatorics. I show that this does not hold for the fourth level.

All results are proved by forcing.

1 Bounded Arithmetic

The discovery of abstract set theory was like the discovery of the outer space. Set theory provides us with a telescope and has undoubtly affected the general view of the mathematical universe.

∗This work was initiated in Oxford University England.

†Basic Research in Computer Science, Centre of the Danish National Research Foundation.

I view Systems of Bounded Arithmetic as a promising framework of studying the mathematical microcosm. I suggest that questions in complexity theory reside outside the macro-world of ordinary mathematics. I belive that most deeper questions in complexity theory in a strong sense require refined “perception”. Many principles which reside deep down in most mathematical arguments, appear equivalent from the normal perspective. (Example: Many elementary counting principles, e.g. the different versions of the elementary pigeon-hole principle). Through a microscope things are perceived quite different. Certain powerful extensions of Bounded Arithmetic could provide such a microscope!

Consistency, not truth, is the right starting point when we consider universal problems. What matters must be deductive powerful viewpoints. Certain extensions of subsystems of Bounded Arithmetic seems to provide a very promising basis for this. This paper is the first in series of planed papers. In these my intension is to isolate more and more powerful, (but unsound) systems of Bounded Arithmetic. Notice that if a universal statement (or more generally a Δ_{0}-statement) ψ is proved from a collection of “false” (in the standard universe ℕ) axioms, which are consistent with Bounded Arithmetic, then we know a priori that ψ must actually be true. Because if ψ ware false this would be witnessed in the standard part of each model 𝕄 of Bounded Arithmetic, and so according to Gödels completeness theorem this would contradict the consistency assumption. This observation also seems to apply to the conjecture P ≠ NP. To see this recall that P ≠ NP is equivalent to the statement that “for all programs P, for all k ∈ ℕ, there exists an input x, such that (a) P uses less than | x |^{k}-steps, and either (b1) accept x but x does not satisfies 3-SAT or (b2) P does not accept x, but x is an instance of 3-SAT”. Now if the existential quantifier in “there exists an input x” is bounded by some term t, we obtain a Δ_{0}-formula Θ which implies P ≠ NP. According to the previous remark, if a (consistent) system of Bounded Arithmetic (however unsound) proves Θ, then actually P ≠ NP.

The idea of renouncing central and “obvious” axioms is certainly not new. We recall that there are models in which the self evident parallel postulate of Euclidian Geometry fails, and the wrong principle that each line has many parallel lines-hold true.

2 Making infinite structures finite

We are interested in constructing consistent (but unsound) systems of Bounded Arithmetic. In this paper I show that there are fragments of Bounded Arithmetic which have models 𝕄 in which any countable structure S (up to elementarily equivalence) can be elementarily embedded as a “finite” (in the sense of 𝕄!) structure.

In this section I will illustrate the basic method of this type of result. Consider the impossible ideal that any consistent theory Σ has always a \underline{finite} model. I show that there exists a world in which this ideal is realised. In this world the usual induction axioms only hold for purely existentially defined sets.

Construction: According to the completeness theorem, there is a countable structure 𝕄 non-isomorphic, but elementarily equivalent to ℕ, so the same set of Lexpressible sentences holds in the two structures. There must be an initial segment of 𝕄 isomorphic to (and identified with) ℕ. Usually the elements in ℕ are called standard numbers while the numbers in 𝕄 \ ℕ are the so-called “non-standard” numbers.

From an observers perspective outside 𝕄 (i.e. from our perspective) there exist “numbers” n ∈ 𝕄 which are infinitely large (i.e {1, 2, ...., n}) contains infinitely many numbers). However observers inside 𝕄 would either not be able to express this, or if we allow them to quantify over second order objects (definable in 𝕄) they would disagree. These observers of 𝕄 would believe that {1, 2, ..., n} was finite simply because it would be finite in their universe 𝕄, where they have fewer functions and therefore think more sets are finite! So far all have been folklore. Now the basic part of the argument runs along lines, similar to those in the proof of Theorem 21 in [12].

Suppose ψ states that there exists a bijection from some interval {1, 2, .., n} to the universe 𝕄. From our outside view {1, 2, ...., n} contains infinitely (countable) many numbers, and so our universe must contain a bijection f from {1, 2, ..., n} to 𝕄. Suppose now that we actually add a such a map f which maps {1, 2, ..., n} bijectively to 𝕄. Suppose also that we extend the language L with an extra function symbol f̄ referring to this f. Also assume that we add names for each of the countable many elements in 𝕄. Let us call this new language Lf̄. Clearly it is not possible for the model (𝕄, f) to satisfy the principle of induction. However if f is constructed carefully it turns out that we can force the model to satisfy some amount of induction!

In this example I want to show that one can ensure that (𝕄, f) satisfies induction for sets which can be existentially defined by Lf̄-formulas. First take an outside view. The model 𝕄 is countable so there are only countably many existentially defined sets S_{1}, S_{2}, .. defined by formulas ψ_{1}(x), ψ_{2}(x), .... of one free-variable. List these formulas such that each formula appears infinitely many times in the list. At the k^{th}-step in the construction consider the formula ψ_{k}(x), which as an example could be

∃u f̄(x + 13) = 2 · u.

Suppose that in the previous step f has already been defined on a finite set A ⊆ {1, 2, ..., n} with values in B ⊆ 𝕄.

We want the least number principle to be true for the formula ψ_{k}(x). This is done by “forcing” ψ_{k}(a) to be true for the smallest possible a, i.e. by letting f(a + 13) be even for the smallest value a where this is consistent with the fact that f is a 1-1 map. The conditions a has to satisfy can be expressed in the language L without reference to f̄. So in 𝕄 we are able to search for such an a by a simple search procedure, which only depends on how f has already been defined on A. From an outside view “<” does not well order 𝕄, so for a moment we take a look at things from inside 𝕄. From this perspective “<” is a well ordering (this is possible because there are fewer sets in 𝕄 than in the real universe). So the search procedure must terminate with some output a. Observers whether inside or outside 𝕄, always agree on first order properties, in this case, whether a actually is the smallest such element.

Now go back to the real world outside 𝕄 and proceed to the next step where the formula ψ_{k+1}(x) is considered. Again we force ψ_{k+1}(a) to be true for the smallest possible a. Alternatively if we cannot force ψ_{k+1}(a) to be true for any a we know it will never be true (even at doomsday when f is constructed for all formulas).

We must ensure that f eventually defines the required bijection. In the present construction this automatically happens. For instance, for each a ∈ {1, 2, ..., n} the formula ψ(x) := ∃y f̄(x) = y ∧ x = a eventually forces a to belong to {1, 2, ..., n} (if it does not already do so). The other properties follow for similar reasons.

Now let Σ be any consistent theory. According to Skolem-Löwenheims theorem, Σ has a countable model S. If this model is infinite we assume that ℕ is the underlying set. If we in the above construction start off by choosing a countable non-standard model (𝕄, S_{𝕄}) elementarily equivalent to (ℕ, S), we get a model of existential induction in which Σ has a finite (in the sense of 𝕄) model. Thus we have shown:

Proposition 2.0.1 Any consistent theory Σ has a model S, which is embedded as a finite (=bounded) set in some model 𝕄.

Actually suppose that L is a countable language which extend the language of arithmetic, and suppose that L contains undefined relation and function symbols for the language of Σ. Then the model 𝕄 can be chosen such that it satisfies the induction scheme for existential L-formulas.

This shows that any structure S, for example structures of strong systems like set theory, can be embedded as “finite” sets in some super-structure. It also shows that we can always assume that a given mathematical domain is “finite” given that our meta-theory (falsely) believes that all sets (and maps etc) in the universe are purely existentially defined.

As the pigeon-hole principle fails for infinite sets, as a corollary we obtain theorem 21 [12]:

Corollary 2.0.2 (A.Wilkie, J.Paris) The system I∃(f) does not prove that f satisfies the pigeon-hole principle.

The results in this paper resemble the ideas just described. However we need to be more careful.

It follows from the main results that countable structures can always be assumed to be (up to elementarily equivalence) finite in certain fragments of Bounded Arithmetic. As we have already indicated this phenomenon is closely related to the fact that the pigeon-hole principle fails heavily in these fragments. And it illustrates the microscope metaphor. One just has to look through the microscope from the right end!

3 Prelims

First let me recall some basic notations and facts, essentially all from [4]. Let BASIC denote a finite set of quantifier free formulas relating constants, functions and relations in the first order language L = L(0, 1, +, ·, | · |, ♯, ⌊\frac{x}{2}⌋, ≤, =). Here ♯ denotes the function given by a♯b = 2^{|a|·|b|} where |a| = ⌈log_{2}(a + 1)⌉. An example of a proper choice of BASIC (without coding functions) can be found in [4]. It is convenient to add other functions to the language. We will assume that a function (w)_{x} which takes the value of the x^{th} element in the sequence coded by w is part of the language. As long as additional functions are polynomially time computable, the results in this section can be stated with no change.

In the first order case atomic formulas are of the form t = s or t ≤ s where s, t are terms in L, while in the (monadic) second order case additionally, atomic formulas can be of the form t ∈ X or X =_{2} Y. (Where “=_{2}” denotes equality between second order variables.)

A first (second) order formula is bounded if all its quantifiers are of the form ....∀x ≤ t... or ....∃x ≤ t..... Second order quantifiers are not allowed in bounded formulas. Atomic formulas X =_{2} Y are not allowed because they smuggle in an unbounded first order quantifier (Extensionality axiom below). A first (second) order formula is sharply bounded if it is bounded and all quantifiers are of the form ....∀x ≤| t | ... or ....∃x ≤| t | ....

The class of bounded formulas can be stratified as follows: Let Σ_{0}^{b} = Π_{0}^{b} be the set of sharply bounded formulas (first or second order formulas depending on the context). Let Σ_{i+1}^{b} ( Π_{i+1}^{b} ) ; i ≥ 0 be the smallest class of formulas which contains Π_{i}^{b} ( Σ_{i}^{b} ) and is closed under ∧, ∨, sharply bounded quantification, and bounded existential quantification (bounded universal quantification). Notice that, except for minor syntactical changes, any bounded formula belongs to some Σ_{i}^{b} and to some Π_{i}^{b}.

Finally let strict-Σ_{i+1}^{b} ⊆ Σ_{i+1}^{b} denote the set of Σ_{i+1}^{b}-formulas which are of the form ∃y_{1} ≤ t_{1}∃y_{2} ≤ t_{2}...∃y_{r} ≤ t_{r} ϕ where ϕ ∈ Π_{i}^{b}. Similarly, let strict-Π_{i+1}^{b} ⊆ Π_{i+1}^{b} denote the set of Π_{i+1}^{b}-formulas which are of the form ∀y_{1} ≤ t_{1}∀y_{2} ≤ t_{2}...∀y_{r} ≤ t_{r} ϕ where ϕ ∈ Σ_{i}^{b}.

3.1 The first order theories

Let S_{2}^{i} denote the first order theory consisting of BASIC, together with the following “polynomial time” induction scheme, φ(0) ∧ ∀x(φ(⌊\frac{x}{2}⌋) ⇒ φ(x)) ⇒ ∀xφ(x)), where φ ∈ Σ_{i}^{b}. This scheme is usually denoted by Σ_{i}^{b}-PIND. Let T_{2}^{i} denote the first order theory consisting of BASIC together with the Σ_{i}^{b} induction scheme, φ(0) ∧ ∀x(φ(x) ⇒ φ(x + 1)) ⇒ ∀xφ(x), where φ ∈ Σ_{i}^{b}. This scheme is usually denoted by Σ_{i}^{b}-IND.

3.2 The second order theories

The (monadic) second order versions of these theories S_{2}^{i}(α) (T_{2}^{i}(α)) consist of BA-SIC, Σ_{i}^{b}-PIND (Σ_{i}^{b}-IND) together with the extensionality axiom

EXT : ∀X, Y (X =_{2} Y ⇔ ∀x(x ∈ X ⇔ x ∈ Y)).

We do not allow the full comprehension axiom, but follow [6] and equip S_{2}^{i}(α) (T_{2}^{i}(α)) with the following “NP ∩ co-NP”comprehension axiom-scheme: (Δ_{1}^{b}-comprehension)

∀x(φ(x, z⃗, Z⃗) ⇔ ¬η(x, z⃗, Z⃗)) ⇒ ∃X∀x (x ∈ X ⇔ φ(x, z⃗, Z⃗))

where φ, η ∈ Σ_{1}^{b}.

The underlying logic of these theories is second order predicate logic with second order equality =_{2}. It is easy to prove that no deductive strength is lost if X =_{2} Y is taken to be short-hand notation for ∀z(z ∈ X ↔ z ∈ Y), and if EXT and the equality axioms in the underlying logic are dropped.

3.3 Models of second order theories

A model of a second order theory T is a pair (𝕄, R̂), where R̂ ⊆ P (𝕄), the power set of 𝕄, and where 𝕄 is a model for the first order part of T. The satisfaction relation ⊧ is defined inductively such that second order variables are taken to be the subsets of 𝕄 which are in R̂. The well known main advantage of using this notion of a model, without requiring that R̂ = P (𝕄), is that the Compactness Theorem, the Completeness Theorem and Skolem-Löwenheims Theorems hold with minor changes. These facts follow easily (pointed out by A.J.Wilkie in Personal communication) from the natural isomorphism:

Observation 3.3.1 (Transitive collapse) Let 𝕄^{△} = 𝕄_{num}^{△} ∪ 𝕄_{set}^{△}be a first order model which contains two kinds of elements. One kind(x,y,z,...) denotes numbers and belongs to 𝕄_{num}^{△}, the other kind(X,Y,Z,...) denotes ”sets” and belongs to 𝕄_{set}^{△}. If ˜∈ is a binary relation on 𝕄^{△}, with domain 𝕄_{num}^{△} and range 𝕄_{set}^{△} such that

𝕄^{△} ⊧ (X = Y ⇔ ∀x(x˜∈X ⇔ x˜∈Y))

then the map ψ_{collapse} : X ⟶ {x ∈ 𝕄_{num}^{△} : 𝕄^{△} ⊧ ”x˜∈X”} maps 𝕄_{set}^{△} bijectively onto a class Ŝ of subsets of 𝕄_{num}^{△}. Furthermore (𝕄, Ŝ) :≡ (𝕄_{num}^{△}, ψ_{collapse}”𝕄_{set}^{△}) is isomorphic to 𝕄^{△}.

From this we get the following version of the Completeness Theorem.

Proposition 3.3.2 T ∪ EXT is consistent if and only if T has a model. T ∪ EXT ⊢ ϕ if and only if (𝕄, Ŝ) ⊧ ϕ for all models (𝕄, Ŝ) ⊧ T.

3.4 Some special results for S_{2}^{i}(α)

Now I prove that the second order theories S_{2}^{i}(α) are conservative over the corresponding first order theories, in the sense that any model 𝕄 ⊧ S_{2}^{i} has an expansion to a model (𝕄, S̃) ⊧ S_{2}^{i}(α). A similar result holds for the theories T_{2}^{i}. I prove a slightly more general result. Let Ψ be a set of formulas ψ(x), which might contain free second order variables and free first order variables other than x.

Definition 3.4.1 By a Ψ-substitution scheme Σ we will understand a first order formula θ_{Σ} with no second order variables, which contains meta-variables F_{1}, F_{2}, ..., F_{l}. To each meta-variable F_{j} is associated a term t_{j}. A substitution instance Σ(ψ(x)), ψ ∈ Ψ is obtained by replacing each F_{j} in θ_{Σ} with ψ(t_{j}). ♣

Example 3.4.2 Σ_{i}^{b}(α)-PIND and Σ_{i}^{b}(α)-IND are both Σ_{i}^{b}(α)-substitution schemes.

Definition 3.4.3 In the following let T (i) = Σ + BASIC + EXT, where Σ is a Σ_{i}^{b}- substitution scheme. In T (i), BASIC could be any set of first order formulas. ♣

Proposition 3.4.4 If (𝕄, R̂) ⊧ T (i) there is an expansion Ŝ ⊇ R̂ such that

(𝕄, Ŝ) ⊧ T (i) + Δ_{1}^{b} − comprehension.

Proof: Assume that (𝕄, R̂) ⊧ T (i) is a given model. Let

Ŝ = {S ⊆ 𝕄 : ∃ψ_{i}(= ψ_{i}(x, X_{1}, X_{2}, ..., X_{k})) ∈ Σ_{1}^{b}, i = 1, 2
∧∃R_{1}, R_{2}, ..., R_{k} ∈ R̂
(x ∈ S ⇔ ψ_{1}(x, R_{1}, R_{2}, ..., R_{k}) ⇔ ¬ψ_{2}(x, R_{1}, R_{2}, ..., R_{k}))}

I claim that (𝕄, Ŝ) ⊧ T (i) + Δ_{1}^{b}-comprehension. According to proposition 3.3.2 EXT holds in all second order models, in particular (𝕄, Ŝ). BASIC holds in (𝕄, Ŝ) because it is a set of first order formulas. It remains to be shown that (𝕄, Ŝ) ⊧ Σ and to show (𝕄, Ŝ) ⊧ Δ_{1}^{b}-comprehension. Sub claim 1: (𝕄, Ŝ) ⊧ Σ(ψ(x)) for all ψ ∈ Σ_{i}^{b}. Notice that if ψ(x, S_{1}, S_{2}, ..., S_{k}) is a Σ_{i}^{b}−formula with set parameters from Ŝ, there is a Σ_{i}^{b}−formula η(x, R_{1}, R_{2}, ..., R_{l}) with set parameters from R̂, such that for all c ∈ 𝕄

(𝕄, Ŝ) ⊧ ψ(c, S_{1}, S_{2}, ..., S_{k}) ⇔ η(c, R_{1}, R_{2}, ..., R_{l}).

Here η is obtained from ψ by the following. First, by replacing each appearance of S_{i} with either ψ_{1}(x, R_{1}, R_{2}, ..., R_{r}) or ¬ψ_{2}(x, R_{1}, R_{2}, ..., R_{r}) according to whether S_{i} appears positively or negatively. Second, by bringing it in a ”prenex like” form if convenient. Now sub claim 1 follows by noticing that

(𝕄, Ŝ) ⊧ Σ(ψ) ⇔ (𝕄, Ŝ) ⊧ Σ(η) ⇔ (𝕄, R̂) ⊧ Σ(η)

and that (𝕄, R̂) ⊧ Σ(η) is part of the assumption. Sub claim 2: (𝕄, Ŝ) ⊧ Δ_{1}^{b}−comprehension. Let ψ_{1}, ψ_{2} ∈ Σ_{1}^{b} be given and assume that for some given a ∈ 𝕄, (𝕄, Ŝ) ⊧ ∀x ≤ a(ψ_{1}(x) ⇔ ¬ψ_{2}(x)). Consider S = {x | ψ_{1}(x, S_{1}, S_{2}, ..., S_{k})} where S_{1}, S_{2}, ..., S_{k} ∈ Ŝ. As we have already noticed, there are Σ_{1}^{b}−formulas η_{1}(x, R⃗) and η_{2}(x, R⃗) equivalent to ψ_{1} and ψ_{2}, S = {x : η_{1}(x, R⃗)} = {x : ¬η_{2}(x, R⃗)} ∈ Ŝ. □

Corollary 3.4.5 Every model of first order S_{2}^{i}, i ≥ 1 has an expansion to a model of S_{2}^{i}(α).

More generally if U_{1}, U_{2}, ..., U_{r} are unary relation symbols added to L, then every model of S_{2}^{i}(U_{1}, U_{2}, ..., U_{r}), has an expansion to a model of S_{2}^{i}(α)

Proof: The first part of the corollary is just the special case where r = 0. If r > 0 let R_{i} := {x ∈ 𝕄 : 𝕄 ⊧ U_{i}(x)} and let R̂ := {R_{1}, R_{2}, ..., R_{r}}. Notice (𝕄, R̂) ⊧ S_{2}^{i}(α) − Δ_{1}^{b}-comprehension, and use proposition 3.4.4 with Σ as the Σ_{i}^{b}- substitution scheme Σ_{i}^{b}-PIND. □

Notice that Corollary 3.4.5 remains valid if the theories S_{2}^{i} are replaced by T_{2}^{i} for i ≥ 1.

3.5 Some conservation results

In [5] S.Buss gave a precise characterisation of the S_{2}^{i}-provable Σ_{i}^{b}-definable functions. Actually one of the major justification for dealing with S_{2}^{i} lies in this characterisation. Let me make an observation in this connection. According to a general argument by G.Kreisel the class of provable total recursive functions is always insensitive to the addition of extra universal axioms.

The same argument applies to the class of Σ_{i}^{b}-definable functions of a theory. The class is insensitive to addition of Π_{i}^{b}-axioms (as long they remain consistent with S_{2}^{i}). This is because for a theory T in general:

T + {∀xψ(x)} ⊢ ∀x∃yθ(x, y) ⇒ T ⊢ ∀x∃yθ(x, y) ∨ ¬ψ(y)

which does not produce any new provable total function if θ(x, y) ∨ ¬ψ(y) still is provable equivalent to a Σ_{i}^{b}-formula. Thus we have

Observation 3.5.1 The class of provable Σ_{i}^{b}-definable functions of a theory T is immune with respect to the underlying Π_{i}^{b}-theory.

The following immediately gives us the inclusions

S_{2}^{1}(α) ⊆ T_{2}^{1}(α) ⊆ S_{2}^{2}(α) ⊆ T_{2}^{2}(α) ⊆ .....

Proposition 3.5.2 (S.Buss) S_{2}^{i+1}(α) ⊢ T_{2}^{i}(α) for all i ≥ 0.

Proof: Fix an arbitrary (𝕄, Ŝ) ⊧ S_{2}^{i+1}(α). First notice that if X < b is a Σ_{i}^{b}- definable set in 𝕄 the convex closure Y = conv(X) := {x < b | ∃v ∈ X v ≤ x ∧ ∃u ∈ X x ≤ u} is also a Σ_{i}^{b}-definable set in 𝕄. Let “dist(Y, Y^{c}) ≤ d” be the Σ_{1}^{b}(Σ_{i}^{b})-formula ϕ_{b}(d) ≡ ∃x, y < b (y − x ≤ d ∧ y ∈ Y ∧ x ∉ Y). By considering the point ⌊\frac{x+y}{2}⌋obviously S_{2}^{i+1}(R) ⊢ ϕ_{b}(d(⌊\frac{1}{2}⌋)^{k}) ⇒ ϕ_{b}(d(⌊\frac{1}{2}⌋)^{k+1}) so by Σ_{i+1}^{b} - PIND “dist(Y, Y^{c}) ≤ b ′′ ⇒ “dist(Y, Y^{c}) ≤ b(⌊\frac{1}{2}⌋)^{|b|} ” and by modus ponens and the fact the S_{2}^{1}(α) ⊢ b(⌊\frac{1}{2}⌋)^{|b|} = 1 “dist(Y, Y^{c}) ≤ 1 ”. As Y is convex, Y has a smallest element in 𝕄, and then by definition X has a smallest element. As Σ_{i}^{b}-LNP ⇔ Σ_{i}^{b}-IND we are done. □

In some later examples I will use one of the deeper theorems in the subject:

Theorem 3.5.3 (S.Buss) For i ≥ 1, S_{2}^{i+1}(α) is ∀Σ_{i+1}^{b}-conservative over T_{2}^{i}(α).

Proof: Suppose that S_{2}^{i+1} ⊢ ∀x⃗∀X⃗∃z⃗ ≤ t(x⃗) ψ(x⃗, z⃗, X⃗) where ψ ∈ Π_{i}^{b}. It suffices to show that T_{2}^{i}(R⃗) ⊢ ∃z⃗ ≤ t(x⃗) ψ(x⃗, z⃗, R⃗), for ψ ∈ Π_{i}^{b}.

This follows again by relativising the proof of S.Buss’ theorem stating that for any i ≥ 0 S_{2}^{i+1} is ∀^{nd}Σ_{i+1}^{b}-conservative over T_{2}^{i}, [7] [5]. □

4 Some finitisation principles

One of our aims is to show that there is a fundamental difference between S_{2}^{2}(α) and levels in the hierarchy which are at least as strong as T_{2}^{2}(α). There is a general feeling amongst those working in Bounded Arithmetic that a proof of the non-finite axiomatisability of the first order theory S_{2} (= T_{2}) would be of great importance. An important step in that direction would be to separate T_{2}^{1}, S_{2}^{2} and T_{2}^{2}. These theories are only known to be different under an additional hypothesis from complexity theory.

In [9] T_{2}^{i} and S_{2}^{i+1}, i ≥ 1 were conditionally separated under the conjectural assumption that the polynomial hierarchy (in complexity theory) does not collapse on level i + 2. In [8] S_{2}^{2} and T_{2}^{2} were conditionally separated under the conjectural assumption Logspace^{Σ_{2}^{p}} ≠ Δ_{3}^{p}. However both these assumptions (generally believed to be true) are far beyond current techniques. They both imply P ≠ NP.

The relativised cases S_{2}^{2}(α) and T_{2}^{2}(α) were first separated in [8]. I present new proofs for these relativised cases. This is done by proving the following finitisation principle:

Theorem 4.0.4 If ψ has an infinite model (in the real world), there are structures of T_{2}^{1}(α) in which ψ has a finite (=bounded) model.

I also get the following principle.

Theorem 4.0.5 Suppose that θ := ∃A ψ(A, R) is a second order existential statement. Suppose also that θ is expressed solely by unspecified function and relation symbols. Suppose that θ has an infinite model (in the real world) where the existential quantifier is not witnessed by any finite set. Then there are structures of T_{2}^{1}(α), in which θ has a finite model {1, 2, ..., n} where the existential quantifier is not witnessed by any set A of size ≤ log(n).

Since an understanding of the relativised cases, seems to precede an understanding of the unrelativised cases these two results could perhaps be useful in separating T_{2}^{1} from T_{2}^{2} unconditionally.

Finally I prove a finitisation principle which can be used to separate the theories S_{2}^{1}(α) and T_{2}^{1}(α).

Theorem 4.0.6 Suppose that ψ(≺, R) is a first order statement which is expressed solely by unspecified function and relation symbols. Suppose that in the real world ψ(≺, R) holds in an infinite model, where ≺ defines a total linear ordering. Then there are structures of S_{2}^{1}(α) in which ψ(≺, R) holds in a finite (=bounded) model and where ≺ is the restriction of the order relation <.

These theorems show that when we pass from the real universe to an universe which only contains “feasible” sets, we have the heuristic translations, countable → finite, finite → poly-logarithmic.

4.1 Further definitions and assumptions

Let L_{2}(0, 1, +, ·, f_{fast}, f_{slow}, =, ≤) be a second order language where through some basic axioms f_{fast} and f_{slow} are ensured to define functions such that f_{fast} is fastgrowing, and that f_{slow} is slow growing. Further it is assumed that f_{slow} is slower than f_{fast} is fast (!). More precisely assume: (1 ) f_{slow}, f_{fast} are increasing. (2 ) f_{fast} ≥ x^{2}. (3 ) For any fixed k, for all sufficiently large n f_{slow}(f_{fast}^{(k)}(n)) ≤ n, where

f^{(k)} = \underbrace{f ∘ f ∘ ... ∘ f}_{k} .

Definition 4.1.1 A formula ψ ∈ L_{2} is sharply bounded if each quantifier appears in the context ∃x ≤ f_{slow}(t) or ∀x ≤ f_{slow}(t), where t ∈ Term_{L}. A formula ψ ∈ L_{2} is bounded if each quantifier appears in a context ∃x ≤ t or ∀x ≤ t, where t ∈ Term_{L}.

The class of Σ_{i}^{b} formulas and the class of Π_{i}^{b} formulas are defined similar to the earlier definition. ♣

Definition 4.1.2 T^{1}(α) denotes the second order theory consisting of a proper base theory Basic together with EXT + Δ_{1}^{b}−comprehension + Σ_{1}^{b}−IND. ♣

Given some additional relations R⃗ we define the first order theory T^{1}(R⃗) in the obvious way. \underline{Notice} that if f_{fast}(< x, y >) := x♯y and f_{slow}(x) := |x|, for a proper choice of BASIC T^{1}(α) becomes T_{2}^{1}(α). Furthermore notice that in this case

f_{fast}(n) ≤ f_{fast}(< n, n >) = 2^{(|n|^{2})}

and therefore | f_{slow}(f_{fast}^{(k)}(n)) | ≤ | f_{slow}(f_{fast}^{(k)}(< n, n >)) | = | n |^{2^{k}} . Clearly for any fixed k and non-standard n, | n |^{2^{k}}< n so the consideration below applies to the theory T_{2}^{1}(α).

Definition 4.1.3 Let < x_{1}, x_{2}, ..., x_{k} > be a natural code of the k-tuple. For each k we introduce quantifiers ∀^{k} and ∃^{k} such that Q^{k}x ψ(x) is shorthand notation for Qx_{1}Qx_{2}...Qx_{k} ψ(< x_{1}, ..., x_{k} >) where Q ≡ ∀ or Q ≡ ∃. ♣ Definition 4.1.4 Let Q^{k}x < t... be short-hand notation for Qx_{1} < t...Qx_{k} < t, when < x_{1}, x_{2}, ..., x_{k} >= x. Let θ(x⃗) be a formula in some relational language L(R_{1}, R_{2}, ..., R_{l}). For a relation symbol S, the formula θ_{S}(x⃗) denotes the formula which appears if each quantifier in θ is restricted to S. By θ_{<a}(x⃗) we understand the formula which appears by restricting each quantifier in θ to [0, a). ♣

4.2 A version of the completeness theorem

As I have already pointed out, in the real mathematical universe it is not true that any finite consistent set of first-order sentences has a \underline{finite} model. But there are T_{2}^{1}(α)-universes where such a strong form of the completeness theorem holds.

Theorem 4.2.1 (Finitisation principle) Let θ(R⃗) be a first order property expressed in some relational language L̃ = L(R⃗). Suppose that η(n) is an arithmetical first order property expressible in the language L of arithmetic and suppose that η(n) holds for arbitrary large n. If θ(R⃗) has a model then the theory T^{1}(R⃗) + ∃n η(n) ∧ θ_{<n}(R⃗) has a model.

First we shall make some preparation for the proof. Let L̃ and θ(R⃗) be given as in the theorem. We can assume that all relations are r-ary. θ(R⃗) is assumed to have an infinite model, so by Skolem-Löwenheims Theorem, we can assume θ(R⃗) has an infinite countable model S_{st} on a subset of the natural numbers. Furthermore, we can assume S_{st} is a model with an underlying co-countable set, and if convenient, that an extra unary relation symbol denoting membership of S_{st} is added to the language.

Let (𝕄, S) be a countable non-standard model for the language L̃(R) := L ∪ L̃ which is elementarily equivalent to the standard model (ℕ, S_{st}). Use overspill to pick a non-standard number n such that 𝕄 ⊧ η(n).

Fix a non-standard number b_{0} < n such that b_{0}^{k} < n for each standard number k, and such that f_{slow}(f_{fast}^{(k)}(n)) < b_{0} for every standard number k. Use overspill to pick c ∈ 𝕄 non-standard such that f_{slow}(c) < b_{0} and such that c > f_{fast}^{(k)}(n) for all standard numbers k.

Definition 4.2.2 Let P_{k}, k ∈ ω, be the set of all partial (1-1)-maps α which have dom(α) ⊆ {1, 2, ..., c} and ran(α) ⊆ 𝕄 such that | dom(α) |≤ b_{0}^{k}, and such that α maps points in [0, n) to S, and maps points in {n + 1, n + 2, ..., c} to 𝕄 \ S.

Let P = ∪_{k∈ω}P_{k} and let (P, ⊆) be P ordered under inclusion. ♣

4.3 Generic maps

Let us now make a few basic definitions:

Definition 4.3.1 D ⊆ P is called dense if ∀α ∈ P∃β ∈ D such that β ⊇ α.

A subset S ⊆ 𝕄 is quasi-definable in 𝕄 if there is θ(x) ∈ L(R_{ω}) such that S = {x ∈ M : (𝕄, ω) ⊧ θ(x)} where R_{w} is interpreted by ω. We allow θ to contain parameters from 𝕄. ♣

Notice that in [1] the similar notion (just called definable) is S = {x ∈ M | ∃n ∈ R_{w} θ(x, n)}, which would not work in our case because we cannot force formulas in general to be equivalent to existential formulas. It should also be noticed that any extension of the notion of quasi-definability which does not produce uncountably many quasi-definable dense subsets of P, would work.

Example 4.3.2 The set P is quasi-definable. The initial segment [0, b_{0}^{ω}) is quasidefinable.

Definition 4.3.3 G ⊆ P is a generic filter if

(1) ∀α, β ∈ G ∃γ ∈ G γ ⊇ α ∧ γ ⊇ β.

(2) ∀α ∈ G ∀β ∈ P α ⊇ β ⇒ β ∈ G.

(3)  G ∩ D ≠ ∅ for each quasi-definable dense set D ⊆ P.  ♣

Lemma 4.3.4 For every α_{0} ∈ P ∃G ⊆ P generic such that α_{0} ∈ G.

Proof: 𝕄 is assumed to be countable so that there is at most countably many quasidefinable sets D ⊆ P. List those as D_{1}, D_{2}, D_{3}, .... Pick α_{1} ⊇ α_{0} such that α_{1} ∈ D_{1}, pick α_{2} ⊇ α_{1} such that α_{2} ∈ D_{2}, etc. and let G := {β ∈ P | ∃j ∈ ω β ⊆ α_{j}}. It is straightforward to check that G is generic. □

Definition 4.3.5 α̃ ⊆ 𝕄 is generic if there is a generic G ⊆ P such that α̃ = ∪_{α∈G}α.

♣

4.4 Sketch of proof

Now let me sketch the proof. We are given a non-standard model (𝕄, S) ≡_{e} (ℕ, S_{st}) in which the “structure” S we want to miniaturise is a part. We can assume that the language contains the language of arithmetic together with extra relations, denoting the relations in S.

First, it is shown that some (actually any) generic α̃ is a bijection from [0, c) to 𝕄, mapping [0, n) onto S. At this stage we also have to show certain lemmas about the forcing relation in order to ensure it behaves well.

Second, it is shown that for some (actually any) generic map α̃, (𝕄, α̃) ⊧ ∃^{∗}−LNP, where ∃^{∗}-LNP denotes the least number principle for formulas in which all quantifiers are either existential (positive appearance) or are restricted to [0, b_{0}). This part of the argument is based on the same idea as the proof of theorem 21 in [12] (see also the introduction).

Third, it is noticed that the constants, relations and functions in the miniaturised structure S_{mini} := α̃^{−1}(S) are ∃ ∩ ∀-definable in the generic model (𝕄, α̃).

Fourth, it is shown that each formula expressing a Σ_{1}^{b}- property about the miniaturised model and numbers in [0, c), can be translated into an ∃^{∗}-formula. This ensures that LNP holds for Σ_{1}^{b}-formulas with parameters in [0, c).

Finally a concrete model 𝕄^{∗} is constructed as the smallest initial segment of [0, c) which contains [0, n) and is closed under f_{fast}.

4.5 The forcing relation

First we need to show some basic fact about generic maps. For simplicity we reduce logical constants. So suppose that ∀ :≡ ¬∃¬ and ∧ :≡ ¬ ∨ ¬. Extend the language with names for the elements in 𝕄. Also extend the language L̃(R) by an extra binary relation symbol ᾱ. For sentences in this language L̃(R⃗, ᾱ) we define the forcing relation inductively as follows:

α |⊢ ψ if ψ does not contain ᾱ, is atomic and true.

α |⊢ ᾱ(a, b) iff α(a) is defined and equals b.

α |⊢ ψ ∨ η iff α |⊢ ψ or α |⊢ η.

α |⊢ ∃x ψ(x) iff for \underline{some} a ∈ 𝕄 α |⊢ ψ(a).

The forcing relation for negation satisfies:

α |⊢ ¬ψ iff for no β ⊇ α, β ∈ P β |⊢ ψ.

4.6 Soundness of the forcing relation

We have to make sure that the forcing relation satisfies certain key properties. Except for lemma 4.6.4 below, the reader who is familiar with forcing techniques could ignore this section.

Definition 4.6.1 Let Σ(b_{0}) be the set of formulas where all quantifiers are restricted to [0, b_{0}). ♣

Notice f_{slow}(c) < b_{0} and therefore in the final model all sharply bounded quantifiers are restricted to [0, b_{0}).

Lemma 4.6.2 (Forcing lemma) The forcing relation has the following properties: Extension property: If α |⊢ ψ and β ⊇ α then β |⊢ ψ Consistency: For no α ∈ P and for no ψ, does both α |⊢ ψ and α |⊢ ¬ψ hold. Completeness: For each generic set G ⊆ P, and for each ψ there is α ∈ G such

that α |⊢ ψ or ψ |⊢ ¬ψ.

Soundness 1: If for a generic map α̃, (𝕄, α̃) ⊧ ψ, there is α ∈ G such that α |⊢ ψ. Soundness 2: If α |⊢ ψ then (𝕄, α̃) ⊧ ψ for \underline{any} generic α̃ ⊇ α.

Proof: Extension property: First notice that the claim holds for atomic formulas. Clearly the extension lemma holds if ψ ≡ ψ_{0} ∨ ψ_{1}, or if ψ ≡ ∃yψ_{0}(y). Suppose ψ ≡ ¬ψ_{0}, α |⊢ ψ, and β ⊇ α is given. By definition for no α′ ⊇ α, α′ ⊢ ψ_{0}. The ordering ⊇ of the forcing conditions P is transitive for no α′ ⊇ β, α′ |⊢ ψ_{0}. By definition β |⊢ ψ. Consistency: Direct by the inductive definition. Completeness: Let D := {α : α |⊢ ψ ∨ ¬ψ}. Notice D is quasi-definable and dense so there is α_{0} ∈ G ∩ D. By definition either α_{0} |⊢ ψ or α_{0} |⊢ ¬ψ. Soundness 1 + 2: Both claims are proved simultaneously using induction on the number of logical constants in ψ. The case where ψ is atomic is straightforward, and so is the case where ψ ≡ ψ_{0} ∨ ψ_{1} or ψ ≡ ∃y ψ_{0}(y).

If (𝕄, α̃) ⊧ ¬ψ, by induction there cannot be α ∈ G such that α |⊢ ψ. By completeness there is α ∈ G such that α |⊢ ¬ψ.

If α |⊢ ¬ψ but (𝕄, α̃) ⊧ ψ for some generic map α̃ ⊇ α, there is β ∈ G such that β |⊢ ψ. By definition α and β have a common extension in P. By use of the extension and the consistency property we get a contradiction. □

Corollary 4.6.3 Any generic α̃ is a bijection from [0, c) to 𝕄,which maps [0, n) onto S.

Proof: Let a ∈ [0, c] be an arbitrary element. Notice that D_{a} := {α : α(a) is defined} is both dense and quasi-definable. By definition there is α_{0} ∈ D ∩ G.

As α_{0} ⊆ α̃ this shows that α̃ has domain [0, c). The other properties are proved by a similar argument. □

Lemma 4.6.4 For each ψ(x⃗) ∈ Σ(b_{0}) there is k ∈ ω which does not depend on the parameters in ψ(x⃗) and 𝕄-definable maps x⃗ ↪ V D ; x⃗ and x⃗ ↪ V R ; x⃗ such that

(1)  Card(V D ; x⃗) ≤ b_{0}^{k}, Card(V R ; x⃗) ≤ b_{0}^{k}.
(2)  For all α ∈ P with Dom(α) ⊇ V D ; x⃗ and Ran(α) ⊇ V R ; x⃗.
α |⊢ ψ(x⃗) or α |⊢ ¬ψ(x⃗).
(3)  For all α ∈ P, α_{|V D ; x⃗∪V R ; x⃗} |⊢ ψ(x⃗) if α |⊢ ψ(x⃗).

Proof: If ψ(x) is atomic and is of the form α(u, v), α(x, v), α(u, x) or α(x_{1}, x_{2}) let V_{x}^{D} := {u}, V_{x}^{D} := {u}, V_{x}^{D} := {v} or V_{x_{1},x_{2}}^{D} := {x_{1}}, and similar let V_{x}^{R} := {v}, V_{x}^{R} := {v}, V_{x}^{R} := {v} and V_{x_{1},x_{2}}^{R} := {x_{2}}.

If ψ ≡ ψ_{0} ∨ ψ_{1} let V D ; x⃗ := V D,0 ; x⃗ ∪ V D,1 ; x⃗, and let V R ; x⃗ := V R,0 ; x⃗ ∪ V R,1 ; x⃗. If ψ ≡ ∃u ≤

b_{0} ψ_{0}(u, x⃗) let V D ; x⃗ := ⋃_{u≤b_{0}} V_{u,x⃗}^{D,0} and V R ; x⃗ := ⋃_{u≤b_{0}} V_{u,x⃗}^{R,0} and notice that Card(V D/R ; x⃗) ≤

b_{0} · b_{0}^{k} = b_{0}^{k+1} for some k ∈ ω. If ψ ≡ ¬ψ_{0} letV D/R ; x⃗ := V D/R,0 ; x⃗.

Now we prove (2) and (3) by induction on the number of logical constants in ψ(x⃗). If ψ(x⃗) is atomic it is easy to check (2) and (3). Suppose α |̸⊢ ∃x ≤ b_{0} ψ(x) where ψ ∈ Σ(b_{0}).

We need to show that α_{|V} |⊢ ¬∃x ≤ b_{0} ψ(x). Conversely suppose that for some β ⊇ α_{|V}, β |⊢ ∃x ≤ b_{0} ψ(x). By definition for some a ≤ b_{0}, β |⊢ ψ(a), and by induction β_{|V_{a}^{D}∪V_{a}^{R}} |⊢ ψ(a). Now as α_{|V_{a}^{D}∪V_{a}^{R}} = β_{|V_{a}^{D}∪V_{a}^{R}} α_{|V_{a}^{D}∪V_{a}^{R}} |⊢ ∃x ≤ b_{0} ψ(x) and then by the extension lemma α_{|V} |⊢ ∃x ≤ b_{0} ψ(x), which is in contradiction to the assumption α |̸⊢ ∃x ≤ b_{0} ψ(x) . □

4.7 Some properties of the generic objects

We have already defined ∃^{∗} to be the set of formulas in which all quantifiers are either existential which appear positively or are restricted to [0, b_{0}) (Sharply bounded quantifiers). According to our plan in order to prove the main theorem we have to prove that some (any) generic α̃ satisfies the ∃^{∗} -LNP scheme. Let ∃_{Strict}^{∗} be the set of formulas ∃x⃗ψ(x⃗), where ψ ∈ Σ(b_{0}) and where there are no restrictions on the parameters in ψ. First we prove that:

Lemma 4.7.1 For any generic map α̃, (𝕄, α̃) satisfies the ∃_{Strict}^{∗}-LNP scheme.

Proof: Let ψ(z) ≡ ∃x⃗ψ_{1}(x⃗, z) be given. (ψ_{1} ∈ Σ(b_{0})). Let α_{0} ∈ P_{k} be given such that α_{0} |⊢ ψ(a) for some a ∈ 𝕄. Let a_{0} ∈ 𝕄 be the smallest element such that for some β ⊇ α_{0} with β ∈ P_{k+r} (for suitable r), and some x⃗_{0}, β |⊢ ψ_{1}(x⃗_{0}, a_{0}). This definition makes sense because the forcing relation is definable for Σ(b_{0})-formulas. (By lemma 4.6.4). Let D be the set of β′ ∈ P which are either incompatible to α_{0} or extensions of a β with the property just mentioned above. D is quasi-definable and dense so there is α ∈ D ∩ G. Clearly α |⊢ ψ(a_{0}). All that remains is to check that if r is chosen properly (lemma 4.6.4) there is no a_{1} < a_{0} and α′ ⊃ α with α′ |⊢ ψ(a_{1}). □

4.8 A minor problem

Now we want to prove that for some (any) generic α̃, (𝕄, α̃) actually satisfies the ∃^{∗}-LNP scheme. It should be noticed that because of the presence of the generic object α̃ it is not entirely clear why any ∃^{∗}-formula should be equivalent to an ∃_{Strict}^{∗} formula.

Let ψ(z) be a given ∃^{∗}-formula. Let us try to follow the same strategy as in the proof of lemma 4.7.1 above. Without loss of generality we can assume that

ψ(z) ≡ ∃x_{0}∀u_{0} ≤ b_{0}∃x_{1}∀u_{1} ≤ b_{0}...∃x_{k}θ(x⃗, u⃗, z)

where θ ∈ Σ(b_{0}). Find smallest z_{0} such that there are a_{0},a_{1,0}, a_{1,1}, ..., a_{1,b}, and a_{2,0,0}, a_{2,0,1}, ...., a_{2,0,b_{0}} and a_{2,1,0}, a_{2,1,1}, a_{2,1,2}, ..., a_{2,1,b_{0}} ..., a_{2,b_{0},b_{0}}, ...

... \underbrace{a_{k,b_{0},b_{0},...b_{0}}}_{k b′_{0}s}

and β ⊇ α_{0} in P_{k+r} such that for any choice u_{0} ≤ b_{0}, u_{1} ≤ b_{0}, ... u_{k} ≤ b_{0}

β |⊢ θ(a_{0}, a_{1,u_{0}}, a_{2,u_{0},u_{1}}, ..., a_{k,u_{0},...,u_{k−1}}, u_{0}, u_{1}, ...u_{k−1}, z_{0})

Again if there is any z_{0} satisfying the condition, there is also a smallest such z_{0}. This holds for each choice of r ∈ ω. As a minor technical problem we need to show (what might be obvious to the reader) that if β is chosen as above, for no β′ ⊇ β we can have β′ |⊢ ψ(z_{1}) for some z_{1} < z_{0}. Now in general (𝕄, α̃) has \underline{more} definable functions on [0, b_{0}) than 𝕄. This is because for each formula θ(x, α) and each generic map α̃, α could be eliminated (i.e. there was a formula ψ(x) such that ∀x ∈ [0, b_{0}) θ(x, α) ⇔ ψ(x) in the case where f_{slow}(x) := log(x)), then induction would hold up to b_{0} ≥ log(c) and therefore up to c, which would be a contradiction. Essentially we have to check that ψ(z_{1}) can not have a sequence of witnesses which was not definable in 𝕄. In the case where ψ(x) was a ∃_{Strict}^{∗}-formula there was no such problem because the search in 𝕄 was only a search for standard finitely many witnesses. We have to show that there cannot be such a z_{1}. This is essentially done by showing that in the case of ∃^{∗}-formulas for any generic α̃ there is an 𝕄 definable sequence of witnesses.

For θ ∈ ∃^{∗} we make the following definition:

Definition 4.8.1 α |⊢^{D} ∀x ≤ b_{0} θ(x) iff ∀x ≤ b_{0} α |⊢^{D} θ(x).

α |⊢^{D} ∃xθ(x) iff ∃x α |⊢^{D} θ(x)

α |⊢^{D} ¬¬θ iff α |⊢^{D} θ. ♣

Notice that for θ ∈ ∃^{∗} if α |⊢^{D} θ for each extension (not necessarily a generic extension!) α̃ of α then (𝕄, α̃) ⊧ θ.

Observation 4.8.2 For each α_{0} ∈ P, each k ∈ ω and each ψ ∈ ∃^{∗} the set {< α, x >: α ⊇ α_{0} ∧ α ∈ P_{k} ∧ α |⊢^{D} ψ(x)} is definable in 𝕄.

The problem we are concerned with at this stage is whether it is possible for given α_{0} and θ ∈ Σ(b_{0}) to have α ⊇ α_{0} with α |⊢ ∀x ≤ b∃y θ(x, y) but for \underline{no} β ⊇ α_{0}, β ∈ P_{r} : β |⊢^{D} ∀x ≤ b∃y θ(x, y) ?

\underline{Assume} that there is α ⊇ α_{0} such that α |⊢ ∀x ≤ b_{0}∃y θ(x, y). Claim: There is an extension α_{1} ⊇ α such that ∀x ≤ b_{0}∃y α_{1} |⊢ θ(x, y). Pick for each j ≤ b_{0}, α^{j} such that α ⊆ α^{0} ⊆ α^{1} ⊆ ...α^{b_{0}} = α_{1} and such that α_{j} |⊢ ∃yθ(j, y). Furthermore by lemma 4.6.4 each extension can be chosen to be of size ≤ b_{0}^{l} for some \underline{fixed} l ∈ ω (l can be chosen to be the number of “∀x ≤ b_{0}” quantifiers in θ). So α_{1} is a ≤ b_{0}^{l+1} extension of α. By lemma 4.6.4 for each x ≤ b_{0} and witness y(x) there is a set V_{x,y(x)} with cardinality ≤ b_{0}^{l} for some \underline{fixed} standard l. Let V := ⋃_{x≤b_{0}} V_{x,y(x)}. Notice that Card(V) ≤ b_{0}^{l+1} and that ∀x ≤ b_{0}∃y α_{1,|V} |⊢ ψ(x, y). Let β = (α_{1})_{|V} and notice that β |⊢^{D} ∀x ≤ b_{0}∃y θ(x, y). We have just proved the first part of the next lemma:

Lemma 4.8.3 Let ψ(z) = ∀x ≤ b_{0}∃y θ(x, y, z) where θ ∈ Σ(b_{0}). There is r ∈ ω such that if β ⊇ α_{0} is the b_{0}^{r}-extension of α_{0} with the smallest z_{0} such that

β |⊢^{D} ∀x ≤ b_{0}∃y θ(x, y, z_{0})

then for \underline{any} generic model (𝕄, α̃) with α̃ ⊇ α_{0} (𝕄, α̃) ⊧ ψ(z_{0}) ∧ ∀z < z_{0} ¬ψ(z).

More generally Let ψ(z) = ∃x_{0}∀u_{0} ≤ b_{0}∃x_{1}∀u_{1} ≤ b_{0}....∃x_{k} θ(u⃗, x⃗, z) where θ ∈ Σ(b_{0}). Then there is a standard number r which does not depend on the parameters in ψ such that if β ⊇ α_{0} is the b_{0}^{r}-extension of α_{0} with the smallest z_{0} satisfying β |⊢^{D} ψ(z_{0}) then for \underline{any} generic model (𝕄, α̃) with α̃ ⊇ α_{0}

(𝕄, α̃) ⊧ ψ(z_{0}) ∧ ∀z < z_{0} ¬ψ(z).

Proof: Let α_{0} be given. \underline{Assume} that for some α ⊇ α_{0}

α |⊢ ∀x_{1} ≤ b_{0}∃y_{1}∀x_{2} ≤ b_{0}...∃x_{k} θ(x⃗, y⃗)

but that for \underline{no} β ⊇ α_{0}, β ∈ P_{r} β |⊢^{D} ∀x_{1} ≤ b_{0}∃y_{1}...θ(x⃗, y⃗). There is α′ ⊇ α such that ∀x_{1} ≤ b_{0}∃y_{1} α′ |⊢ ∀x_{2} ≤ b_{0}∃y_{2}....θ(x⃗, y⃗). By induction on k, we can assume that we have already proved that if for some fixed x_{1} and y_{1}, β ⊇ α, β |⊢ ∀x_{2} ≤ b_{0}∃y_{2}...θ(x⃗, y⃗), β can be chosen to be an b_{0}^{l+k−1}-extension, where l is the number of ∀-quantifiers in θ. There is α′′ ⊇ α′ (making b_{0}^{2} b_{0}^{k+l−2}-extensions of α′), such that

∀x_{1} ≤ b_{0}∃y_{1}∀x_{2} ≤ b_{0}∃y_{2} α′′ |⊢ ∀x_{3} ≤ b_{0}...θ(x⃗, y⃗)

Continuing like this, after k steps we obtain α^{∗} ⊇ α such that α^{∗} |⊢^{D} ψ. We can not use α^{∗} as β in the lemma, because α (and therefore α^{∗}) could be too large. But by lemma 4.6.4, there are b_{0}^{k} sets V_{x_{1},y(x_{1}),x_{2},y(x_{2}),...,x_{k},y(x_{k})} each with ≤ b_{0}^{l} elements where l can be taken to be the number of ∀-quantifiers in θ. Let

V := ⋃_{x_{1}≤b_{0}} ⋃_{x_{2}≤b_{0}} ... ⋃_{x_{k}≤b_{0}} V_{x_{1},y(x_{1}),...,x_{k},y(x_{k})}.

Notice that Card(V) ≤ b_{0}^{k+l}. Let β := α_{|V}^{∗} and notice that β |⊢^{D} ψ. This contradicts the assumption. □

Corollary 4.8.4 For \underline{any} generic map α̃ (𝕄, α̃) ⊧ ∃^{∗}−LNP

Proof: Let α̃ be an arbitrary generic map. We need to show that (𝕄, α̃) ⊧ ∃xψ(x) ⇒ ∃x_{0} ≤ x∀z < x_{0} ψ(x_{0}) ∧ ¬ψ(z). Suppose (𝕄, α̃) ⊧ ψ(a) for some a ∈ 𝕄 (otherwise there is nothing to prove). According to the completeness property there is α_{0} ⊆ α̃ such that α_{0} ∈ P and α_{0} |⊢ ψ(a). Assume α_{0} ∈ P_{k}. Consider D ⊆ P defined by D := {α | α ⊉ α_{0} ∨ (α ⊇ α_{0} ∧ ∃x α |⊢^{D} ψ(x) ∧ ∀y < x(∀α′ ⊇ α α′ |̸⊢^{D} ψ(y)))}. From what has already been proved it follows that D is well defined, dense and quasidefinable. For \underline{any} generic G ⊆ P there are α_{1} ∈ D ∩ G. By lemma 4.8.3 for any β̃ ⊇ α (in particular α̃ ) (𝕄, β̃) ⊧ ∃xψ(x) ⇒ ∃x_{0} ≤ x∀z < x_{0} ψ(x_{0}) ∧ ¬ψ(z). As α_{1} ⊆ α̃ we are done. □

4.9 Proof of the first finitisation principle

The previous section has given us a “generic model” (𝕄, α̃) which satisfies the ∃^{∗}-LNP scheme. Clearly α̃ induces a miniaturised version of S on [0, n). Constants, relations and functions on S correspond to constants, relations and functions on [0, n). Now I prove the important fact that all the miniaturised relations etc. are ∃ ∩ ∀-definable in (𝕄, α̃).

For each relation R ⊆ S^{r} (with quantifier-free definition in 𝕄), we define the corresponding miniaturised relation R_{mini} “existentially” by:

{(x_{1}, x_{2}, ..., x_{r}) | ∃z_{1}, z_{2}, ..., z_{r} ∧_{i=0}^{i=r} α̃(x_{i}, z_{i}) ∧ R(z_{1}, z_{2}, ..., z_{r})}.

Notice that R_{mini} also has a “universal” definition:

{(x_{1}, x_{2}, ..., x_{r}) | ∀z_{1}, z_{2}, ..., z_{r} ∧_{i=0}^{i=r} α̃(x_{i}, z_{i}) ⇒ R(z_{1}, z_{2}, ..., z_{r})}.

Add the miniaturised relations to the language. Consider the sub-language L_{mini} which contains L and names for the miniaturised constants, relations and functions.

Lemma 4.9.1 If ψ(x) ∈ L_{mini} is a Σ_{1}^{b}-formula with all quantifiers restricted to [0, c), there is a ∃^{∗}-formula ψ^{∗}(x) such that:

{x ≤ c : (𝕄, α̃) ⊧ ψ(x)} = {x ≤ c : (𝕄, α̃) ⊧ ψ^{∗}(x)}.

Proof: Let ψ(x) ∈ L_{mini} be a given Σ_{1}^{b} property. Replace each appearance of a ”miniaturised” relation R_{mini} by either the ∃-definition or the ∀-definition according to whether the R_{mini} appears positively or negatively in ψ(x). Notice that this gives an ∃^{∗}-formula ψ^{∗}(x) which satisfies the lemma. □

Now we are ready to construct a model of T_{2}^{1}(α) in which there is a bounded sub-structure S_{mini} on [0, n) where η(n) such that S_{mini} ⊧ θ_{<n}(R⃗). We have already got a countable model 𝕄 of true arithmetic in which a possibly unbounded model of θ(R⃗) is coded. We have n, b_{0}, c ∈ 𝕄 as above. Let α̃ be an arbitrary generic map, as described earlier. Let

𝕄∗ ; α̃ = {x ≤ c : ∃k ∈ ω x < f_{slow}^{(k)}(n)}.

Let R̂ be the set of all L_{mini}-definable relations on [0, n). It follows from what has already been proved that (𝕄, R̂) ⊧ Σ_{1}^{b}-IND scheme, hence because of corollary 3.4.5 there is an expansion of R̂ to Ŝ ⊇ R̂ such that (𝕄, Ŝ) ⊧ T^{1}(α). As second order existence statements are absolute with respect to expansions, we have proved the main theorem in the T^{1}(α)-case.

Corollary 4.9.2 Let S be a countable mathematical structure which can be encoded in a non-standard model 𝕄 which satisfies true arithmetic. There is a model of T_{2}^{1}(α) in which S appears as a bounded set.

Notice that our results hold in the special case where T^{1}(α) is the second order theory which consists of

1) Induction for existential formulas.

2) The ∀ ∩ ∃-comprehension axiom scheme.

5 Separating T_{2}^{1}(α) and S_{2}^{2}(α)

In the process as a by-product we have obtained a new proof of the separation of the theories T_{2}^{1}(α) and S_{2}^{2}(α).

Theorem 5.0.3 For \underline{any} generic map α̃ (𝕄∗ ; α̃, S̃α̃) ⊧ T_{2}^{1}(α).

If S defines two disjoint infinite sets, then for \underline{any} generic map α̃ (𝕄∗ ; α̃, S̃α̃) |̸= S_{2}^{2}(α).

Proof: The first part of the theorem has already been proven. It follows from the examples below that the second part holds at least for some constructions (i.e. for some S). To prove the second part let U(x) be a new unary predicate symbol which holds exactly in one component of S. Let U_{mini} denote the corresponding predicate in L_{mini}. Put f_{slow} :=| x | and f_{fast} := x^{|x|}. Consider the formula

A(z) := ∃u_{1} < u_{2} ≤ n u_{2} − u_{1} ≥ b^{z} ∀x ∈ [u_{1}, u_{2}) U_{mini}(x).

Clearly A(k) is valid for all standard k and hence, by overspill, A(z) holds for some non-standard z (and z ≤| n |). But this is a contradiction as for any given interval of length < b^{ω} the set of α ∈ P such that α maps an element of S \ U into it, is dense and quasi-definable.

According to [5] Σ_{2}^{b}-PIND is sufficient to ensure the validity of Σ_{2}^{b}-LMAX principle which in turn implies the validity of the Σ_{2}^{b}-overspill just used. □

Notice that if S is an infinite (co-countable) set with no additional structure then (𝕄∗ ; α̃, S̃α̃) ⊧ S_{2}(α). This shows that the second part of the theorem becomes false if there is no condition on S.

Corollary 5.0.4 T_{2}^{1}(α) ≠ S_{2}^{2}(α).

This is a new proof of the result which was first proved in [8].

6 Some examples

Example 6.0.5 Fix p ≥ 2. There is an infinite model A where “R defines a partition of A into disjoint p-subsets”. Let η(n) ≡ “n is not divisible by p’.

According to the first principle T^{1}(α) ⊬ Count(p).

In [2] and [16] it is shown that this holds for much stronger theories.

Example 6.0.6 According to the first principle:

(1) T^{1}(α) ⊬ ”every linear ordering R (of a finite set) has an isolated point”.

(2) T^{1}(α) ⊬ ”every linear ordering R (of a finite set) is discrete”.

(3) T^{1}(α) ⊬ ”every linear ordering R (of a finite set) is a well ordering”. By the results below in all cases T^{1}(α) can be replaced by S_{2}^{2}(α).

\underline{Notice} that example 6.0.6 shows (using T_{2}^{1}(α) ≡ WOA, Proposition 8.0.9) that the well ordering axiom for arbitrary linear orderings (WOA^{∗}) R does \underline{not} follow from WOA.

7 Another principle

The second finitisation principle says that for any given r ∈ ℕ if some second order existential relational property P̃ ≡ P (R⃗, X) is only witnessed by infinite sets (in the real universe), there are models of T_{2}^{1}(α) in which there is an n and relations R⃗ ⊆ [0, n) such that no subset X ⊆ [0, n) with size ≤ log_{2}^{r}(n) witness P (R⃗, X).

Theorem 7.0.7 (Finitisation principle) Let θ ≡ ∃Xψ(R⃗, X) be a second order existential formula where ψ is a first order formula in the language L(R⃗, X, =). Let k ∈ ℕ be a given natural number. In general (1) implies (2):

(1) There is a \underline{countable} model S of the language L(R⃗, =), such that for \underline{no finite} set X ⊆ S, S ⊧ ψ(R⃗, X).

(2) T^{1}(α) + “∃n∀X[0, n) Card(X) ≤ (log(n))^{k} ⇒ ¬ψ_{<n}(R⃗, X)” has a model.

This principle states that if a second order existential property has (in the real universe) a \underline{countable} model where the existential quantifier is not \underline{finitely} witnessed then it is consistent with T_{2}^{1}(α) (and by the results below S_{2}^{2}(α)) that there is a \underline{finite} model where the existential quantifiers is not “polylog”-witnessed.

Example 7.0.8 In the real world there is a binary tree with no finite branch. By the second finitisation principle T_{2}^{1} is consistent with the existence of a tree T ⊆ [0, n), which has no branch (coded by a number) of length ≤ log_{2}^{k}(n)”.

In the real word there is a vector space over Z_{2} with no finite basis, so by the second principle there exists a model of T_{2}^{1}(α) in which there exists a vector space V ⊆ [0, n) with no basic (coded by a number) of size ≤ log_{2}^{k}(n)”.

Proof: Proved by a construction very similar to the proof of the first finitisation principle. Pick S according to (1). Choose S as a countable model in the standard model on say the even numbers. Extend the standard model to an elementary equivalent countable non-standard model. Pick non-standard numbers b_{0} < n < c as above. Consider the same set of forcing conditions (P, ⊆) as above. The forcing conditions ensure that each generic α̃ maps small (i.e. ≤ b_{0}^{k} points) 𝕄-definable sets to “small” 𝕄-definable sets. The map α̃ induces a miniaturised structure S_{mini} with underlying set [0, n). For each 𝕄-definable subset B ⊆ [0, n), A := α̃^{−1}(B) can \underline{not} witness ψ(R⃗, A) because the set A has cardinality ≤ b_{0}^{k} which is finite \underline{in} the model 𝕄. As in the proof of the first principle without any complications we construct a model T_{2}^{1}(α) where ψ_{<n}(R⃗, X) is not witnessed by any set A of size ≤ b_{0}^{ω}. □

8 The well ordering axiom in S_{2}^{1}.

The well ordering axiom (WOA) is the principle:

WOA  ∀X(X ≠ ∅ ⇒ ∃y(y ∈ X ∧ ∀z < y z ∉ X))

WOA says that “<” well orders any set X, and should not be confused with the stronger principle WOA^{∗} stating that \underline{any} linear ordering of a bounded set is a well ordering.

Proposition 8.0.9 (Suggested by A.J.Wilkie) WOA is equivalent to T_{2}^{1}(α) in models of S_{2}^{1}(α)

Proof: T_{2}^{1}(α) ⇒ WOA: To reach a contradiction let (𝕄, Ŝ) ⊧ T_{2}^{1}(α) + ¬WOA. There is R ∈ Ŝ such that R ≠ ∅ and such that (𝕄, Ŝ) ⊧ ∀y(y ∈ R ⇒ ∃z < y z ∈ R). As R ≠ ∅ there is u_{0} ∈ R such that:

(∗)  (𝕄, Ŝ) ⊧ ∀y ≤ u_{0}(y ∈ R ⇒ ∃z < y ∈ R).

Let Y = {x ∈ 𝕄 : ∃z ∈ R z < x ∧ x ≤ u_{0}} ⊆ 𝕄. Notice that Y is Σ_{1}^{b}-definable in 𝕄 with set parameter R (Y is not required to belong to S̃). As Σ_{1}^{b}-LNP ⇔ Σ_{1}^{b}- IND, and as Y is non-empty, there is a minimal x_{0} ∈ Y. By definition of Y there is z < x_{0} such that z ∈ R. By (∗) this contradicts the minimality of x_{0}. WOA ⇒ T_{2}^{1}(α) : Let (𝕄, Ŝ) ⊧ S_{2}^{1}(α) + WOA be an arbitrary model. Let ψ ∈ Σ_{0}^{b} (= Π_{0}^{b}) be an arbitrary formula with possible set variables Z⃗ ∈ Ŝ. It is enough to prove that the Σ_{1}^{b}-definable set Y := {x ∈ 𝕄 : ∃z ≤ t(x) ψ(x, z, Z⃗)} ⊆ 𝕄 has a smallest element if it is not empty. Pick u_{0} ∈ Y. To this end consider

ϕ(w) :≡ ∃w_{1} ≤ u_{0}∃w_{2} ≤ u_{0} w = w_{1} · u_{0} + w_{2} ∧ ψ(w_{1}, w_{2}; Z⃗).

As ϕ ∈ Δ_{1}^{b} R_{b,u_{0}} :≡ {w ≤ b | ϕ(w)} ∈ Ŝ for any b, u ∈ M. Choose b such that for each pair (x, z) with z ≤ t(x) and x ≤ u_{0}, (x, z) ≤ b. According to WOA R_{b,u_{0}} has a smallest element w_{0}. Let y_{0} be the unique element with y_{0} · u_{0} ≤ w_{0} < (y_{0} + 1) · u_{0}, and notice that M ⊧ y_{0} = min(Y). We used the fact that strict-Σ_{1}^{b}-LNP is equivalent to Σ_{1}^{b}-IND over S_{2}^{1}(α) . So to prove Proposition 8.0.9 all that remains is to prove this, and the equivalence of Σ_{1}^{b}-IND and strict-Σ_{1}^{b}-LNP over S_{2}^{1}(α). Both these facts follow from [4],[7]. □

8.1 A finitisation principle for S_{2}^{1}(α)

As already proved T_{2}^{1}(α) is equivalent to the well ordering axiom WOA over the theory S_{2}^{1}(α). In this section I show that S_{2}^{1}(α) does not prove this axiom, and thus as a corollary we get a new proof of the separation result S_{2}^{1}(α) ≠ T_{2}^{1}(α). Parts of the argument are very similar to the proof of the two previous principles so I only emphasise the new ideas in the construction.

Theorem 8.1.1 (Finitisation principle for S_{2}^{1}(α)) Let ψ(≺, R) be a sentence in the first order language L(≺, R, =). Suppose that ψ(≺, R) has an infinite model S where ≺ defines a total linear ordering. Then ∃n∃U ⊆ [1, n] ψ_{U}(<, R) holds in some models of S_{2}^{1}(α).

Proof: I put the emphasis on the new ideas. Let (ℕ, S_{ℕ}, R_{ℕ}) be an expansion of the standard model ℕ to an infinite model of S, where R ⊆ S^{r}, and where ψ(≺, R) holds. Let (𝕄, S_{large}, R_{large}) be an elementary equivalent (in a language expanded by relation symbols for R_{large} and S_{large}) non-standard model. Let n ∈ 𝕄 be a nonstandard number, and let I^{∗} ⊆ 𝕄 be the initial sequent defined by

I^{∗} := {m ∈ 𝕄 : ∃t term m < t(n)}.

A Σ_{1}^{b}(I^{∗})-formula θ, is a Σ_{1}^{b}-formula where all parameters belong to I^{∗}. Notice that all quantifiers in such a θ also are restricted to I^{∗}. Choose b_{0} such that I^{∗} < 2^{b_{0}}, and such that b_{0}^{ω} < n. Notice that sharply bounded quantifiers in a Σ_{1}^{b}(I^{∗})-formula are bound by b_{0}.

We want to construct U ⊆ [1, n] and R ⊆ U^{r} such that ψ_{U}(<, R) is forced true, and such that the polynomial induction scheme

(θ(0) ∧ ∀x(θ(⌊\frac{x}{2}⌋) ⇒ θ(x))) ⇒ ∀xθ(x)

is forced true for all Σ_{1}^{b}(I^{∗})-formulas θ. Let < θ_{1}(x), a_{1} >, < θ_{2}, a_{2} >, .... be an enumeration of the countably many pairs < θ_{j}(x), a_{j} > where θ_{j}(x) is a Σ_{1}^{b}(I^{∗})- formula with one free variable (namely x), and where a_{j} ∈ I^{∗}.

Let U_{0} = W_{0} = R_{0} = ∅. Choose d_{0} < e_{0} ∈ 𝕄 with e_{0} − d_{0} > b_{0}^{ω}, and e_{0} < \frac{n}{b_{0}} . Let f_{0} = ∅.

In general after stage j we have constructed U_{j}, W_{j} ⊆ [1, n] and R_{j} ⊆ U_{j}^{r}, such that U_{j} ∩ W_{j} = ∅. The map f_{j} maps U_{j} bijectively onto a subset of S_{large}, such that < u_{1}, .., u_{r} >∈ R_{j} precisely when R_{large}(f(u_{1}), ..., f(u_{r})). Furthermore, we have | U_{j} |≤ j · b_{0}, | W_{j} |≤ j · b_{0}, and [d_{j}, e_{j}] such that e_{j} − d_{j} > b_{0}^{ω}. The points in U_{j} are very sparsely distributed in the sense that ∀u_{1} ≠ u_{2} ∈ U_{j} | u_{2} − u_{1} |≥ e_{j}.

Now consider < θ_{j+1}(x), a_{j+1} >. Our aim is to force

θ_{j+1}(0) ∧ ∀x(θ_{j+1}(⌊\frac{x}{2}⌋) ⇒ θ_{j+1}(x)) ⇒ θ_{j+1}(a_{j+1})

true. Let a_{j+1}^{1} := a_{j+1}, ...., a_{j+1}^{r+1} := ⌊\frac{a_{j+1}^{r}}{2} ⌋, ... for r ≤ ⌈log(a_{j+1})⌉. Now for each u ∈ [d_{j}, e_{j}] define the number l(u) ∈ 𝕄 as the largest number (≤ log(a_{j+1})) such that there are extensions U′_{j+1} ⊇ U_{j}, W′_{j+1} ⊇ W_{j}, and R′_{j+1} ⊇ R_{j}, such that

(1) (U′_{j+1}, R′_{j+1}) are isomorphic by an extension f′_{j+1} ⊇ f_{j} to a subset of S_{large}.

(2) The elements in U′_{j+1} has pairwise distance ≥ u

(3) | U′_{j+1} |≤ (j + 1) · b_{0}

(4) | W′_{j+1} |≤ (j + 1) · b_{0}.

(5) At least l(u) of the Σ_{1}^{b}(I^{∗})-formulas θ(a_{j+1}^{1}), ..., θ(a_{j+1}^{⌈log(a_{j+1})⌉}) are forced true. Now because l takes less than b_{0} values, there must be an interval [d_{j+1}, e_{j+1}] ⊆ [d_{j}, e_{j}] such that l is constant on this interval, and such that e_{j+1}−d_{j+1} > b_{0}^{ω}. Choose such an interval, and extend U_{j}, W_{j} and R_{j} by letting U_{j+1} := U′_{j+1}, W_{j+1} := W′_{j+1}, R_{j+1} := R′_{j+1}, and f_{j+1} := f′_{j+1} where these extensions correspond to the case where u = e_{j+1}. Proceed with the construction in this way:

Let U := ∪_{j∈ω} U_{j} and let R = ∪_{j∈ω} R_{j} and notice R ⊆ U^{r}. It is not hard to show that f = ∪_{j∈ω} f_{j} defines a bijection from the miniaturised model U on [1, n] to the large model S_{large}. This ensures that ψ_{U}(<, R) holds in the generic model.

The Σ_{1}^{b}(I^{∗}) polynomial induction schema is forced true. To see this suppose contrarily that for some k ∈ ω in the generic model we have

θ_{k}(0) ∧ ∀x(θ_{k}(⌊\frac{x}{2}⌋) ⇒ θ_{k}(x)) ∧ ¬θ_{k}(a_{k}).

In stage k in the construction we have forced a maximum number of the Σ_{1}^{b}(I^{∗})- formulas θ_{k}(a_{k}^{1}), θ_{k}(a_{k}^{2}), .., θ_{k}(a_{k}^{j}), .., θ_{k}(0) true. As obviously θ_{k}(a_{k}) cannot have been forced true, there must be j < ⌈log(a_{k})⌉ such that θ_{k}(a_{k}^{j+1}) is already forced true (after stage k) while θ_{k}(a_{k}^{j}) is not forced true at this stage (here we are using that the search procedure, for \underline{fixed} u ∈ [d_{k}, e_{k}], is 𝕄-definable). Could it be that θ_{k}(a_{k}^{j}) get forced true at a later stage k′ > k? No, because if this were the case for some u ∈ [d_{k}, e_{k}], l would take a larger value than l(e_{k}), which would be a contradiction.

□

Corollary 8.1.2 There are models of S_{2}^{1}(α) in which WOA fails.

Proof: Let ψ(≺) := ∀x∃y y ≺ x. This sentence holds in an infinite model (in the real world), so by theorem 8.1.1 the sentence ∀x ∈ U∃y ∈ U y < x holds in some models of S_{2}^{1}(α). □

This gives a new proof of the separation first proved in [10]

Corollary 8.1.3 S_{2}^{1}(α) ≠ T_{2}^{1}(α).

9 Lifting the finitisation principles

Now I show that both finitisation principles for T_{2}^{1}(α) hold for the theory S_{2}^{2}(α) but both fail to hold for T_{2}^{2}(α). This, in particular separates the theories S_{2}^{2}(α) and T_{2}^{2}(α). In this I rely heavily on a proof sketch ed by J.Krajicek (personal communication). The proof relies again strongly on S.Buss’ result [5], that S_{2}^{i+1}(α) is ∀Σ_{i+1}^{b}-conservative over T_{2}^{i}(α).

Theorem 9.0.4 The first finitisation principle holds if T^{1}(α) is replaced by S_{2}^{2}(α)

Proof: To get a contradiction assume that θ(R) ≡ ∀x_{1}∃y_{1}....∀x_{k}∃y_{k} θ̃(x⃗, y⃗; R) (θ̃ is quantifier free) does have an infinite model, but S_{2}^{2}(α) ⊢ ∀n (η(n) ⇒ ∀R < n ¬θ_{<n}(R)). Consider the skolemisation

θ̃(x_{1}, F_{1}(x_{1}), x_{2}, F_{2}(x_{1}, x_{2}), ..., x_{k}, F_{k}(x_{1}, x_{2}, ..., x_{k}); R)

of θ(R). By the first finitisation principle T_{2}^{1}(α) + ∃n (η(n) ∧ ∃R < n∃F_{1}, ..∃F_{k} < n ∀x⃗ ≤ n θ̃(x_{1}, F_{1}(x_{1})....; R)) is consistent.

Add an extra constant n̄, extra function symbols F̄_{1}, F̄_{2}, .., F̄_{k} and an extra relational symbol R̄ to the language. Call this language L̃_{2}. The first order theory T_{2}^{1}(n̄, F̄_{1}, ..., F̄_{k}, R̄) + ∀x ≤ n̄ θ̃(x_{1}, F̄_{1}(x_{1}), ..., F̄_{k}(x⃗); R̄) is consistent.

Now by theorem 3.5.3 S_{2}^{2}(n̄, F̄_{1}, ...., F̄_{k}, R̄) + ∀x ≤ n̄ θ̃(x_{1}, F̄_{1}(x_{1}), ..., F̄_{k}(x⃗); R̄) is consistent. As a skolemisation of θ implies θ (even in pure predicate logic) this contradicts our initial assumption about S_{2}^{2}(α). □

This give us the following:

Corollary 9.0.5 Let θ(R⃗) be any first order property in some relational language L̃ := L(R⃗). Then the following are equivalent:

(a)  Predicate logic ⊢ θ(R⃗)

(b)  T^{1}(α) ⊢ ∀n θ_{<n}(R⃗)
(c)  S_{2}^{2}(α) ⊢ ∀n θ_{<n}(R⃗).

Proof: Let T be T^{1}(α) or S_{2}^{2}(α). Assume that θ(R⃗). Assume that T does \underline{not} prove ∀n θ_{<n}(R⃗). There exists a non-standard model 𝕄^{∗} of T in which ¬θ_{<n}(R⃗) holds in some initial segment [0, n), so ([0, n), R⃗) ⊧ ¬θ(R⃗). But then by the completeness theorem θ(R⃗) is not provable in predicate logic.

Contrarily if predicate logic does not prove θ(R⃗) there is a model S of ¬θ(R⃗). If S is finite certainly ∀n θ_{<n}(R⃗) does not have a T -proof (because T is consistent). If S is infinite, by the finitisation principle ∃n ¬θ_{<n}(R⃗) is consistent with T. □

10 Separating S_{2}^{2}(α) and T_{2}^{2}(α)

Theorem 10.0.6 The statement “Every linear ordering of an interval has a smallest element” is provable in T_{2}^{2}(α), but \underline{not} provable in S_{2}^{2}(α).

The statement “There is no dense linear ordering of an interval of length ≥ 2” is provable in T_{2}^{2}(α) but not provable in S_{2}^{2}(α).

Proof: The second part of the claim follows from the finitisation principle for S_{2}^{2}(α). To prove the first part let (𝕄, Ŝ) ⊧ T_{2}^{2}(α) be an arbitrary model. Assume that R is an 𝕄-definable linear ordering of an interval [0, n) for some n ∈ M. Let

Y = {b ∈ [0, n) : ∃a_{0} ≤ b∀x ≤ b xRa_{0} ⇒ x = a_{0}}.

Notice that Y is Σ_{2}^{b}-definable and that 0 ∈ Y and b ∈ Y ⇒ b + 1 ∈ Y for b < n. As (𝕄, Ŝ) ⊧ Σ_{2}^{b} − IND, (n − 1) ∈ Y. By definition of Y, R has a smallest element. The second part follows from the first part. □

This gives us a new proof of

Corollary 10.0.7 S_{2}^{2}(α) ≠ T_{2}^{2}(α).

The following were proved in [10]. Above we have obtained a new proof of the second part of the theorem.

Theorem 10.0.8 The weak pigeon-hole principle (WPHP) is provable in T_{2}^{2}(α), but \underline{not} provable in S_{2}^{2}(α).

Proof: The second part of the theorem has already been proved. The first part follows from the fact that S_{2}^{3}(α) is ∀Σ_{3}^{b}-conservative over T_{2}^{2}(α), that WPHP is a ∀Σ_{2}^{b}-formula and from the following sub claim:

Lemma 10.0.9 WPHP is provable in S_{2}^{3}(α).

Proof: A careful analysis of the S_{2}-proof in [12] (see also [8]) of WPHP shows that the proof is actually a S_{2}^{3}(R)-proof. □

11 Lifting the second principle

For the sake of completeness let me sketch how the second finitisation principle can be lifted to S_{2}^{2}(α).

Theorem 11.0.10 Let θ ≡ ∃X ψ(R⃗, X) be a second order existential formula where ψ can be any first order formula in the relational language L(R⃗, =). Let k ∈ ℕ be a given natural number. In general (1) implies (2):

(1) There is a \underline{countable} model S of the language L(R⃗, =), such that for \underline{no finite} set X ⊆ S, S ⊧ θ(R⃗, X).

(2) S_{2}^{2}(α) + “∃n∀X ⊆ [0, n) Card(X) ≤ (log(n))^{k} → ¬θ_{<n}(R⃗, X)” has a model.

Proof:(sketch) Essentially we lift the result as we did for the first finitisation principle. Suppose that S_{2}^{2}(α) ⊢ ∀n∀R⃗ ⊆ [0, n)∃b ψ_{<n}(R⃗, Seq(b)) where ψ_{<n} ≡ ∀x_{1} < n∃x_{2} < n...∃x_{2r} < n θ̃(x⃗, n, R⃗, Seq(b)) with θ̃ quantifier free.

We have already proved the theorem in the T_{2}^{1}(α)-case, so

T_{2}^{1}(α) + ∀x⃗ < n∀b¬θ̃(x_{1}, F̄_{1}(x_{1}), x_{3}, ...., F̄_{r}, n, R⃗, Seq(b))

is consistent, where the language is extended by extra relation symbols n̄, R⃗, F̄_{1}, ..., F̄_{r}. By S.Buss’ conservation result, (theorem 3.5.3), which also works in this case where we have added extra function symbols to the language

S_{2}^{2}(α) + ∀x⃗ < n̄∀b ¬θ̃(x_{1}, F̄_{1}(x_{1}), ...., n̄, R⃗, Seq(b))

is consistent in this extended language. Clearly this contradicts our initial assumption.

□

Notice the following phenomenon:

Corollary 11.0.11 If

∃X ⊆ [0, n) Card(X) ≤ (log(n))^{k_{1}} ∧ θ_{<n}(R⃗, X)

holds in the real world for some constant k_{1} but does not hold for some other constant k_{2} < k_{1}, S_{2}^{2}(α) does not prove the formula for any constant k.

12 Some applications

By use of the second finitisation principle we get the following theorem. The last case (3) shows that the theorem is not entirely a curiosity.

Theorem 12.0.12 If k is a natural number, then S_{2}^{2}(α) does not prove any of the following statements:

(1) “Every vector space V ⊆ [0, n) over Z_{2} has a basis of size ≤ log^{k}(n)”.

(2) “Every binary tree T ⊆ [0, n) has a branch of length ≤ log^{k}(n)”.

(3) “Every total irreflexively oriented graph on [0, n) has a dominating set of size ≤ log^{k}(n)”.

On the other hand T_{2}^{2}(α) proves (1)-(2).

At present, it is not known whether T_{2}^{2}(α) ⊢ (3). A proof of even S_{2}(α) ⊢ (3) would have interesting consequences. (See [13] and [10] for more details). Proof: The first part of the theorem follows from the second finitisation principle (in case (1) from a slightly modified version of the principle) and the facts:

There is an (infinite) vector space with \underline{no} finite basic.

There is an (infinite) binary tree with \underline{no} finite branch.

There is an (infinite) irreflexively oriented graph with \underline{no} finite dominating set. To prove the last part of the theorem, assume V is a vector space on [0, n) with

no coded basic. Pick independent vectors v_{1}, v_{2}, ..., v_{⌊log(2n)⌋+1} and get a Δ_{1}^{b}-definable injective map from [0, 2n) to [0, n). This violates WPHP which are provable in T_{2}^{2}(α) by [4] (or [8]).

Finally T_{2}^{2}(α) proves that every tree T ⊆ [0, n) has a coded branch. Let T^{∗} := {x ∈ T : ∃b b codes a path of length ≤ ⌊log(n)⌋+1 from the root to x}. Notice that T^{∗} also have the Π_{1}^{b}-definition: T^{∗} := {x ∈ T : ∀b b codes a path from the root to x and the length of the path is ≤ ⌊log(n)⌋ + 1}. Define a Δ_{1}^{b}-relation by F (x) = y iff ∀b b codes a path x_{1}, x_{2}, ..., x_{r} from the root to x, and bit(y, j) = 1 ↔ x_{j} is a right son. Again we get a contradiction to the WPHP in [11]. □

References

[1] M.Ajtai; On the complexity of the pigeonhole principle. 29^{th} Annual symp. on Found. Comp.Sci.(1988),pp 340-355.

[2] M.Ajtai; Parity and the pigeon-hole principle, in Feasible Mathematics Birkhauser, (1990), pp 1-24.

[3] A.Berrarducci, B.Intrigila; Combinatorial principles in elementary number theory, Annals of Pure and Applied Logic 55 (1991) pp 35-50.

[4] S.Buss; Bounded Arithmetic. Ph.D. dissertation, Princeton University, (1985). As book, Bibliopolis, Napoli (1986).

[5] S.Buss; Axiomatization and conservative results for fragments of Bounded Arithmetic, Proc. Workshop in Logic and Computation (1987), Contemporary Mathematics AMS, vol.106 (1990), pp 57-84

[6] F.Ferreira; Polynomial Time Computable Arithmetic and Conservative extensions. Ph.D dissertation, Pennsylvania State University, (1988).

[7] P.Hajek, P.Pudlak; Metamathematics of first order arithmetic, to app. in Springer-Verlag.

[8] J.Krajicek; No counter-example interpretation and interactive computation. To appear in: Logic in Computer science, ed. 287-293.

[9] J.Krajicek; Fragments of Bounded Arithmetic and bounded query classes. To appear in the Transactions of AMS.

[10] J.Krajicek, P.Pudlak, and G.Takeuti; Bounded Arithmetic and the polynomial hierarchy, Annals of Pure and Applied Logic 52 (1991), pp 143-153.

[11] J.Paris, A.Wilkie, A.Woods; Provability of the pigeonhole principle and the existence of infinitely many primes. Journal of Symbolic Logic 53, (1988), pp 1231-1244.

[12] J.Paris, A.Wilkie; Counting problems in Bounded Arithmetic, in: Methods in Mathematical Logic, LNM 1130, Springer (1985), pp 317-340.

[13] P.Pudlak; Ramsey’s theorem in Bounded Arithmetic. To appear.

[14] P.Pudlak; Some relations between subsystems of arithmetic and complexity of computations. In: Logic in Comp. Science, ed.

[15] S.M.Riis; Making infinite structures finite in models of Second Order Bounded Arithmetic, in: Arithmetic, Proof theory and computorial complexity, Oxford university press (1993) pp 289-319.

[16] S.M.Riis; Independence in Bounded Arithmetic; DPhil dissertation, Oxford University (1993)

[17] S.M.Riis; Count(q) does not imply Count(p); Submitted.

[18] A.Wilkie; A model-theoretical proof of Buss’s characterisation of the polynomial time computable functions. Notes. (1985).

Recent Publications in the BRICS Report Series

RS-94-23 S�ren Riis. Finitisation in Bounded Arithmetic. August 1994, 31 pp.

RS-94-22 Torben Bra� uner. A General Adequacy Result for a Linear Functional Language. August 1994, 39 pp. Presented at MFPS ’94.

RS-94-21 S�ren Riis. Count(q) does not imply Count(p). July 1994, 55 pp.

RS-94-20 Peter D. Mosses and Mart��n Musicante. An Action Semantics for ML Concurrency Primitives. July 1994, 21 pp. To appear in Proc. FME ’94 (Formal Methods Europe, Symposium on Industrial Bene�t of Formal Methods), LNCS, 1994.

RS-94-19 Jens Chr. Godskesen, Kim G. Larsen, and Arne Skou. Automatic Veri�cation of Real�Timed Systems Using Epsilon. June 1994, 8 pp. Appears in: Protocols, Speci�- cation, Testing and Veri�cation PSTV ’94.

RS-94-18 Sten Agerholm. LCF Examples in HOL. June 1994, 16 pp. To appear in: Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications, LNCS, 1994.

RS-94-17 Allan Cheng. Local Model Checking and Traces. June 1994, 30 pp.

RS-94-16 Lars Arge. External-Storage Data Structures for Plane-Sweep Algorithms. June 1994, 37 pp.

RS-94-15 Mogens Nielsen and Glynn Winskel. Petri Nets and Bisimulations. May 1994, 36 pp.

RS-94-14 Nils Klarlund. The Limit View of In�nite Computations. May 1994, 16 pp. To appear in the LNCS proceedings of Concur ’94, LNCS, 1994.

RS-94-13 Glynn Winskel. Stable Bistructure Models of PCF. May 1994, 26 pp. Preliminary draft. Invited lecture for MFCS ’94. To appear in the proceedings of MFCS ’94, LNCS, 1994.