Herbrand Consistency and Bounded Arithmetic

Zofia Adamowicz Math.Institute of the Polish Academy of Sciences Sniadeckich 8, 00-950 Warszawa, e-mail zosiaa@impan.gov.pl

Abstract

We prove that the Gödel incompleteness theorem holds for a weak arithmetic T_{m} = IΔ_{0} + Ω_{m}, for m ≥ 2, in the form

T_{m} ⊬ HCons(T_{m}),

where HCons_{m}(T_{m}) is an arithmetic formula expressing the consistency of T_{m} with respect to the Herbrand notion of provability.

Moreover, we prove

T_{m} ⊬ HCons^{I_{m}}(T_{m}),

where HCons^{I_{m}} is HCons relativised to the definable cut I_{m} of m − 2-times iterated logarithms.

The proof is model theoretic.

We also prove a certain non-conservation result for T_{m}.

In [PW] Paris and Wilkie asked the following question: does IΔ_{0} prove the cut free consistency of IΔ_{0}? Here we solve (negatively) an analogous question with IΔ_{0} + Ω_{m}, m ≥ 2 in place of IΔ_{0}. The theory IΔ_{0} + Ω_{m} can be considered as another version of bounded arithmetic and Herbrand provabiltity is a version of cut free provability (it is defined and formalized in secion 2).

Pudlak in [P] and Hajek-Pudlak in [HP] proved Gödel’s Incompleteness Theorem for weak arithmetic with the ordinary (Hilbert) notion of provability.

As Herbrand consistency of a theory is a weaker statement than its ordinary consistency, proving its unprovability in some theory is more difficult.

In [P] Pudlak also proves that theories of the form IΔ_{0} + Ω_{m} do prove their own Herbrand consistency relativised to a certain definable cut J_{m}. Here we show that they do not prove their own Herbrand consistency relativised to I_{m}. It follows that consistently J_{m} ⊊ I_{m}.

Pudlak in [P] (see also Hajek and Pudlak [HP]) in his proof uses a provability predicate P rov and its restriction P rov^{∗} to a definable initial segment and show that P rov and P rov^{∗} satisfy some derivability conditions from which the main result is obtained in a routine way.

Our result for the case of IΔ_{0} + Ω_{2} (m=2) has been proved in [AZ]. There we applied an idea similar to that of [P] and [HP].

In this paper we give a different proof, much more model theoretic than the former one.

The Paris-Wilkie problem has also been considered by Willard in [W].

We use standard notation throughout. In particular, Δ_{0} denotes the class of bounded arithmetical formulas and IΔ_{0} is the system of weak arithmetic with induction scheme for Δ_{0} formulas only. Addition and multiplication are regarded as relations.

Let ω_{0}(x) = x^{2} and ω_{m+1}(x) = 2^{ω_{m}(log x)} (arithmetical log x denotes the integral part [log x] of the logarithm). Axioms Ω_{m} state the totality of the function ω_{m}. The axiom exp states the totality of the exponential function y = 2^{x}.

Generally formulas are always defined as elements of ℕ or of a model M under consideration. In other words we identify formulas with their Gödel numbers.

Let Sat be a universal formula for Δ_{0}. Thus Sat is Σ_{1} and

M ⊧ Sat(φ) iff M ⊧ φ,

for φ ∈ Δ_{0}, in every model M of IΔ_{0} + exp.

For each n ∈ ℕ let

log^{n} M = {a ∈ M : ∃b ∈ M(M ⊧ (b = exp^{n}(a))}.

Of course every log^{n} M is a definable initial segment of M (“y = exp(x)” can be expressed by a Δ_{0} formula – see [HP]). Thus we have I_{m}^{M} = log^{m−2} M.

Sec.1

We shall express (in Sec.2) the Herbrand consistency by a Π_{1} formula HCons_{m}(φ), (φ is Herbrand consistent with T_{m}). We shall use also an auxiliary Π_{1} formula HCons_{m}^{I_{m}}(φ), obtained from HCons_{m} by restriction of the initial quantifier to a definable segment I_{m}, (thus, in the standard model I_{m} is ℕ). The formula HCons_{m}^{I_{m}} will have the following property

(∗)

For a bounded θ if

T_{m} + ∃x̄ ∈ log^{m+1} θ(x̄) + HCons_{m}^{I_{m}}(“0 = 0”) is consistent then

T_{m} + ∃x̄ ∈ log^{m+2} θ(x̄)

is consistent.

Note that HCons_{m}(“0 = 0”) expresses “T_{m} is Herbrand consistent”.

Now with HCons_{m} and HCons_{m}^{I_{m}} as above we can prove the announced result,

T_{m} ⊬ HCons_{m}^{I_{m}}(“0 = 0”).

We need the following theorem:

1.1. Theorem

For m, n ∈ ℕ there is a bounded formula θ(x̄) (where x̄ is a finite string of variables) such that

IΔ_{0} + Ω_{n} + ∃x̄ ∈ log^{m} θ(x̄)

is consistent and

IΔ_{0} + Ω_{n} + ∃x̄ ∈ log^{m+1} θ(x̄)

is inconsistent.

In particular, for m ∈ ℕ there is a bounded formula θ_{m}(x̄) such that

IΔ_{0} + Ω_{m} + ∃x̄ ∈ log^{m+1} θ_{m}(x̄)

is consistent and

IΔ_{0} + Ω_{m} + ∃x̄ ∈ log^{m+2} θ_{m}(x̄)

is inconsistent.

The theorem can be considered as a certain non-conservation result and may be interesting in its own right. We prove this theorem later in this section.

Now the proof of the main result is as follows. Let θ_{m} be given by theorem 1.1. We shall show that

T_{m} + ∃x̄ ∈ log^{m+1} θ_{m}(x̄) + HCons_{m}^{I_{m}}(“0 = 0”)

is inconsistent.

Suppose that this theory is consistent. Then, by (∗),

T_{m} + ∃x̄ ∈ log^{m+2} θ_{m}(x̄)

is consistent. But this violates the choice of θ_{m}. Hence

T_{m} + ∃x̄ ∈ log^{m+1} θ_{m}(x̄) + HCons_{m}^{I_{m}}(“0 = 0”)

is inconsistent. Thus, in view of the consistency of

T_{m} + ∃x̄ ∈ log^{m+1} θ_{m}(x̄),

T_{m} ⊬ HCons_{m}^{I_{m}}(0 = 0),

which completes the proof.

We have shown that to prove our main result it is sufficient to construct formulas HCons, HCons^{I_{m}} with the properties stated above. This will be done in subsequent sections.

Now let us prove theorem 1.1.

Let m, n ∈ ℕ. Suppose that for every bounded formula θ such that IΔ_{0} + Ω_{n} + ∃x̄ ∈ log^{m} θ(x̄) is consistent, IΔ_{0} + Ω_{n} + ∃x̄ ∈ log^{m+1} θ(x̄) is consistent. Fix a bounded formula θ_{0} such that

IΔ_{0} + Ω_{n} + ∃x̄ ∈ log^{m} θ_{0}(x̄)

is consistent, x̄ = x_{1}, …, x_{k}. Hence

IΔ_{0} + Ω_{n} + ∃x̄ ∈ log^{m+1} θ_{0}(x̄)

is consistent.

Hence

IΔ_{0} + Ω_{n} + ∃y ∈ log^{m} ∃x̄ ≤ y( ⋀_{i=1,...,k} y ≥ 2^{x_{i}} ∧ θ_{0}(x̄))

is consistent.

Let θ_{1}(y) be ∃x̄ ≤ y( ⋀_{i=1,...,k} y ≥ 2^{x_{i}} ∧ θ_{0}(x̄)).

Applying our supposition to θ_{1} we infer

IΔ_{0} + Ω_{n} + ∃y ∈ log^{m+1} ∃x̄ ≤ y( ⋀_{i=1,...,k} y ≥ 2^{x_{i}} ∧ θ_{0}(x̄))

is consistent.

Hence

IΔ_{0} + Ω_{n} + ∃x̄ ∈ log^{m+2} θ_{0}(x̄)

is consistent.

Continuing we infer that

IΔ_{0} + Ω_{n} + ∃x̄ ∈ log^{m+n′} θ_{0}(x̄)

is consistent, for n′ ∈ ℕ. Thus there is a model M of IΔ_{0} and an ā ∈ M such that M ⊧ θ_{0}(ā) and M ⊧ ( exp^{n′}(max ā) exists), for n′ ∈ ℕ. Consider the initial segment M′ of M determined be elements exp^{n′}(max ā) for n′ ∈ ℕ. Then M′ ⊧ IΔ_{0} + exp and M′ ⊧ θ_{0}(ā). It follows that the theory IΔ_{0} + exp +∃x̄θ_{0}(x̄) is consistent.

Thus, for every bounded θ, if IΔ_{0} + Ω_{n} + ∃x̄ ∈ log^{m} θ(x̄) is consistent then IΔ_{0} + exp +∃x̄θ(x̄) is consistent.

Also, for any bounded θ_{1}, …, θ_{l}, if

IΔ_{0} + Ω_{n} + ⋀_{i=1,...,l} ∃x̄ ∈ log^{m} θ_{i}(x̄)

is consistent then

IΔ_{0} + exp + ⋀_{i=1,...,l} ∃x̄θ_{i}(x̄)

is consistent. For, the sentence

⋀_{i=1,...,l} ∃x̄θ_{i}(x̄)

can be presented as

∃x̄_{1}, …, x̄_{l} ⋀_{i=1,...,l} θ_{i}(x̄_{i}).

Let now Σ_{1}^{∗} denote the collection of all sentences of the form ∃x̄ ∈ log^{m} θ(x̄), where θ is bounded.

Let T^{∗} ⊆ Σ_{1}^{∗} be maximal (with respect to Σ_{1}^{∗}) consistent with IΔ_{0} + Ω_{n}.

It follows that IΔ_{0} + exp +T^{∗} is consistent.

Let T^{∗∗} ⊆ Σ_{1} consist of those Σ_{1} sentences ϕ of the form ∃x̄θ(x̄), where θ is bounded, for which the sentence “∃x̄ ∈ log^{m} θ(x̄)” is in T^{∗}.

We shall show that T^{∗∗} is maximal consisting of Σ_{1} sentences consistent with IΔ_{0} + exp.

Let ϕ ∈ Σ_{1} of the form ∃x̄θ(x̄) be such that IΔ_{0} + exp +T^{∗∗} + ϕ is consistent. Then

IΔ_{0} + exp +T^{∗∗} + ∃x̄ ∈ log^{m} θ(x̄)

is consistent. Hence

IΔ_{0} + Ω_{n} + T^{∗} + ∃x̄ ∈ log^{m} θ(x̄)

is consitent. Hence, by the maximality of T^{∗}, the sentence “∃x̄ ∈ log^{m} θ(x̄)” is in T^{∗}, whence ϕ ∈ T^{∗∗}. It follows that T^{∗∗} is maximal consisting of Σ_{1} sentences consistent with IΔ_{0} + exp.

Let M ⊧ IΔ_{0} + exp +T^{∗∗} + BΣ_{1} be such that Σ_{1}(M) (the set of Σ_{1} sentences true in M) is not coded in M. Such a model M exists – see [WP2], the proof of theorem 9. Note that by the maximality of T^{∗∗}, Σ_{1}(M) = T^{∗∗}.

By another result of [WP2] (theorem 5 (2)), M has a proper end extension to a model M′ of IΔ_{0} + Ω_{n+1}.

By the maximality of T^{∗} w.r.t IΔ_{0} + Ω_{n} and Σ_{1}^{∗}, we have

M′ ⊧ ϕ ⇔ M ⊧ ϕ,

for every ϕ ∈ Σ_{1}^{∗}.

Let a ∈ M′ \ M. We have thus

M ⊧ ϕ ⇔ M′ ⊧ ϕ^{a},

for every ϕ ∈ Σ_{1}^{∗}.

Since every ϕ ∈ Σ_{1} is equivalent in M (and so in M′) in a canonical way to an ∃Σ_{1}^{b} sentence (via the Matiasevitch theorem) and M′ ⊧ Ω_{1}, we may use the universal formula for ∃Σ_{1}^{b} formulas available in M′ and infer that

{ϕ ∈ Σ_{1}^{∗} : M′ ⊧ ϕ^{a}}

is coded in M′.

Here Σ_{1}^{b} denotes Buss’s class – see [B], [HP] – and ∃Σ_{1}^{b} denotes the class of formulas of the form ∃x̄θ(x̄), where θ is Σ_{1}^{b}. The required universal formula can be built using the formula μ_{1} from theorem 4.18 of [HP] (see also the appendix of [A]). The notation ϕ^{a} denotes the formula obtained from ϕ by bounding its unbounded existential quantifiers to a.

But hence T^{∗} is coded in M′ and consequently T^{∗∗} is coded and so Σ_{1}(M) is coded in M′, whence it is coded in M, contradiction.

Thus the theorem has been proved.

Sec.2

Let us recall what we mean by Herbrand type provability of a sentence. Let φ be a sentence of the form

2.1  ∃x_{1}∀y_{1} … ∃x_{m}∀y_{m}φ̄(x_{1}, y_{1}, …, x_{m}, y_{m}),

where φ̄ is open.

Extend the language by new function symbols f_{1}, …, f_{m} such that f_{k} is of arity k. The symbol f_{k} can be treated as a symbol for a Skolem function for the kth existential quantifier in ¬φ. Let T be the set of terms of the extended language. We call φ̃(t_{1}, …, t_{m}) a Herbrand variant of φ if φ̃ is of the form

φ̄(t_{1}, f_{1}(t_{1}), …, t_{m}, f_{m}(t_{1}, …, t_{m})),

for some t_{1}, …, t_{m} ∈ T .

We say that φ is Herbrand provable (in logic) iff there is a finite T′ ⊆ T such that

⋁_{t_{1},...,t_{m}∈T ′} φ̃(t_{1}, …, t_{m})

is a propositional tautology.

Assume now that T = {ϕ_{1}, ϕ_{2}, …} is a fragment of arithmetic and +, · are treated as relations. Assume that ϕ_{j} is of the form

∀x_{1}∃y_{1} … ∀x_{m}∃y_{m}ϕ̄_{j}(x_{1}, y_{1}, …, x_{m}, y_{m}),

where ϕ̄ is open. We may assume that m ≤ j.

We are aiming at formulating Herbrand type consistency of T. To this end we need to extend the language by some function symbols s_{k}^{j} such that s_{k}^{j} is of arity k. The symbol s_{k}^{j} is a symbol for a Skolem function for the kth existential quantifier in ϕ_{j}. We have k ≤ j. Let the language so obtained be denoted by L̃. Then, by the above definition, a Herbrand variant of ¬ϕ_{j} is a formula ¬ϕ̃_{j}(t_{1}, …, t_{k}) of the form

¬ϕ̄_{j}(t_{1}, s_{1}^{j}(t_{1}), …, t_{k}, s_{k}^{j}(t_{1}, …, t_{k})),

where t_{1}, …, t_{k} are terms of L̃.

Then T is Herbrand-inconsistent if a finite disjunction of some Herbrand variants

¬ϕ̃_{j}(t_{1}, …, t_{k})

is provable in the propositional calculus.

Hence, T is Herbrand consistent if every finite conjunction of some ϕ̃_{j}(t_{1}, …, t_{k}) is consistent with the propositional calculus.

To formalize the property “T is Herbrand-consistent” in arithmetic we have to encode the language L̃ in arithmetic. So we enumerate all terms of L̃ in the following natural order. Let the constants 0, 1 be terms of rank 0 and let the terms of rank at most i + 1 consist all terms of rank at most i and of all terms of the form s_{k}^{j}(t_{1}, …, t_{k}) for j ≤ i + 1 − (k − 1), t_{1}, t_{2}, …, t_{k} of ranks i − (k − 1), i − (k − 2), …, i respectively. We enumerate terms of rank 0, then of rank 1 etc. by consecutive natural numbers leaving some numbers not used. Let the left aside numbers serve to enumerate logical symbols of the language L̃. The exact form of our enumeration is given below in this section. Then terms of rank at most i are enumerated by numbers less than l_{i}, for some recursive function i ⟶ l_{i}.

As a matter of fact in our enumeration every term has a lot of numbers. If t_{1}, …, t_{k} are of rank i_{0} then they are also of rank at most i for every i ≥ i_{0} and so, the term s_{k}^{j}(t_{1}, …, t_{k}) is a term of rank at most i + 1 for every i ≥ i_{0}.

There are recursive uniformly definable functions S_{k}^{i,j} such that S_{k}^{i,j} : [0, l_{i−(k−1)}) × [0, l_{i−(k−2)}) × … × [0, l_{i}) ⟶ [0, l_{i+1}) and the following holds: if the terms t_{1}, …, t_{k} are enumerated by a_{1}, … a_{k} then the term s_{k}^{j}(t_{1}, …, t_{k}) as a term of rank i + 1 is enumerated by S_{k}^{i,j}(a_{1}, …, a_{k}).

Let the encoded language be denoted by L^{∗}.

Let E_{i} denote the collection of encoded atomic and negated atomic formulas on terms of rank at most i.

We shall call a function p : E_{i} ⟶ {0, 1} a T-evaluation of rank i if p(¬φ) = 1−p(φ), for φ ∈ E_{i}. Each such p extends uniquely (in a routine way) to open sentences of L^{∗} with terms < l_{i}. We assume further that p(φ) = 1 for every axiom of equality φ and that p makes

ϕ̄_{j}(t_{1}, s_{1}^{j}(t_{1}), …, t_{k}, s_{k}^{j}(t_{1}, …, t_{k}))

true for every Herbrand variant of ϕ_{j} with terms of rank at most i + 1, i.e. p takes value 1 at the formula

ϕ̄_{j}(a_{1}, S_{1}^{i,j}(a_{1}), …, a_{k}, S_{k}^{i,j}(a_{1}, …, a_{k}))

of L^{∗}, for a_{1} < l_{i−(k−1)}, a_{2} < l_{i−(k−2)}, …, a_{k} < l_{i}.

Note that every T -evaluation of rank i + 1 makes true every conjunction of some ϕ̃_{j}(t_{1}, …, t_{k}) with t_{1}, …, t_{k} of ranks at most i − (k − 1), i − (k − 2), …, i respectively.

Thus, T is Herbrand-consistent if for every i there is a T -evaluation of rank i.

To be able to define all the required notions at stage i we need exp^{3} i to exist. This is because the number l_{i} and E_{i} are roughly of size exp^{2} i and any T -evaluation of rank i is roughly of size exp^{3} i.

The whole formalization is available in IΔ_{0} +Ω_{m}. In particular we have a Δ_{1} formula V^{T} (p, i) expressing the meaning “p is a T -evaluation of rank i”. Then we may formulate Hcons(T) as

∀i ∈ log^{3} ∃p V^{T} (p, i).

This may be considered a weak from of Herbrand consistency, however it makes our negative results even stronger.

Here we give the exact definition of our coding.

Let M be a model of T_{m}. Let us define

l_{0} = 2

and

l_{i+1} = l_{i} + (i + 1)l_{i} + il_{i}l_{i−1} + … + l_{i} · . . . · l_{0}.

We have,

2.2  l_{i} ≤ 2^{2^{i}}

for each i ∈ log^{3}.

For,

l_{i+1} = l_{i}(1 + (i + 1) + il_{i−1} + … + l_{i−1} · . . . · l_{0}) = l_{i}(1 + (i + 1) + l_{i} − l_{i−1})

and hence, assuming 2.2 for a given i > 0, we obtain

l_{i+1} ≤ 2^{2^{i}}(1 + (i + 1) + 2^{2^{i}} − l_{i−1}) = (2^{2^{i}})^{2} + 2^{2^{i}}(1 + (i + 1) − l_{i−1}) ≤ 2^{2^{i+1}}

since, obviously, l_{j} ≥ 1 + (j + 2) for each j ≥ 1.

The graph of the function l (as a function of i) is definable in T_{m} (with the help of an ordinary technique, see e.g. [WP1] or [HP]), so that the domain of l is an initial segment. From 2.2 it follows that l is defined at least on log^{3}. An easy estimation shows that

log^{m−1} M = ⋃_{i∈log^{m+1} M}[l_{i}, l_{i+1})

(where [a, b) is the interval {x : a ≤ x < b}), but we do not use this fact. Let us define also (letters i, j will denote elements of log^{m} throughout)

2.3  \begin{matrix}S_{k}^{i,j}(a_{1}, …, a_{k}) = l_{i} + (i + 1)l_{i} + i · l_{i}l_{i−1} + … + ((i + 1) − (k − 2))l_{i} · . . . · \\ l_{i−(k−2)} + j · l_{i} · . . . · l_{i−(k−1)} + (a_{1}, …, a_{k})_{i}, for k ≥ 2, \\ S_{1}^{i,j}(a_{1}) = l_{i} + jl_{i} + (a_{1})_{i} \end{matrix}

for 1 ≤ k ≤ i, j ≤ i and a_{1} < l_{i−(k−1)}, …, a_{k} < l_{i} (otherwise assume S_{k}^{i,j} = 0; also assume S_{1}^{0,0}(0) = 2 and S_{1}^{0,0}(1) = 3). Here (a_{1}, …, a_{k})_{i} denotes the position (a number

≤ l_{i} · . . . · l_{i−(k−1)})

of (a_{1}, …, a_{k}) in the lexicographical ordering of the product

[0, l_{i−(k−1)}) × … × [0, l_{i}).

The graph of S_{k}^{i,j} is (uniformly in i, j, k) definable in T_{m}. The values S_{k}^{i,j}(a_{1}, …, a_{k}) as in 2.3 fill the interval [l_{i}, l_{i+1}), for each i ∈ log^{3} M. Thus, 2.3 constitutes an enumeration of log M (except 0 and 1).

The inner language L^{∗}, encoded in T_{m} in a usual way, is obtained from the ordinary arithmetical language L (in which addition and multiplication are treated as relations) by adding elements a ∈ log as terms (except the S_{k}^{i,j}(a_{1}, …, a_{k})’s with j = 0, which may serve to define other primitive notions and formulas of L^{∗}).

Let T be a set of sentences of L^{∗}. An evaluation p on E_{i} is a T -evaluation if p satisfies the following condition (denoted shortly p ⊩^{∗} φ):

2.4 for each axiom φ of T in its prenex form, ∀x_{1}∃y_{1} … ∀x_{m}∃y_{m}φ̄, if φ has index j ≥ 1 (in a fixed enumeration of T), then for all i_{1} < … < i_{m} < i (φ < i_{1}) and arbitrary a_{1} < l_{i_{1}}, …, a_{m} < l_{i_{m}},

p assumes the value 1 at φ̄(a_{1}, S_{1}^{i_{1},j}(a_{1}), …, a_{m}, S_{m}^{i_{m},j}(a_{1}, …, a_{m})).

It is understood here that all terms occurring in the axioms of T are less than l_{i}. Notice that, roughly, we have p ≤ 2^{l_{i}}, for each evaluation p on E_{i}.

The condition 2.4 generalizes in a natural way as follows. For an evaluation p on E_{i} and a sentence φ of L^{∗} as in 2.1, which contains parameters c̄ and is of the form ψ(c̄), where ψ ∈ ℕ and c̄ < l_{j}, write p ⊩ φ, if

∀i_{1} ∈ [j + 1, i)∀a_{1} < l_{i_{1}}∃b_{1} < l_{i_{1}+1} … ∀i_{m} ∈ [i_{m−1} + 1, i)∀a_{m} < l_{i_{m}}∃b_{m} < l_{i_{m}+1}

such that p is 1 at

φ̄(a_{1}, b_{1}, …, a_{m}, b_{m}).

For open φ we assume that p ⊩ φ, if p(φ) = 1. Thus, we have p ⊩ φ for each standard axiom φ of T and each T -evaluation p.

All quantifiers in the above definition are bounded by l_{i} ∈ log (i.e. exp(l_{i}) exists). Hence, using the universal formula Sat we can find a Δ_{0} formula F with an additional parameter b (bounding the unrestricted quantifier in Sat) such that

p ⊩ φ iff F (p, i, φ, b)

for arbitrary evaluation p on E_{i}, standard φ with terms < l_{i} and any b such that b ≥ 2^{l_{i}^{φ}}, (cf Lessan [L], theorem 2 of [DP]). It follows that

2.5  p ⊩ φ iff ∀b(b ≥ 2^{l_{i}^{φ}} ⇒ F (p, i, φ, b))

for arbitrary evaluation p on E_{i} and a standard sentences φ with terms < l_{i}. Assume that T is Δ_{0} definable in T_{m}. We construct a Π_{1} formula V^{T} such that

2.6  p is a T -evaluation on E_{i} iff V^{T} (p, i)

iff ∀b(b ≥ 2^{ω_{1}(l_{i})} ⇒ V_{0}^{T} (p, i, b)) with bounded V_{0}^{T}.

Let M be a (non standard) model of T_{m} and let i′ = i + j ∈ log^{3} M, where j > ℕ. Every T -evaluation p ∈ M on E_{i+j}^{M} determines a model M(p, i) as follows. Put

a =_{p} b ≡ p(“a = b”) = 1

for a, b < l_{i+ℕ}. Clearly, =_{p} is an equivalence relation on the initial segment [0, l_{i+ℕ}) of M. Let

M(p, i) = {[a]; a < l_{i+ℕ}}

consist of equivalence classes and define

[a] + [b] = [c] iff p(“a + b = c”) = 1

and similarly for the multiplication and ordering.

It follows immediately that

M(p, i) ⊧ φ iff p(φ) = 1

for arbitrary open φ with parameters < l_{i+ℕ}.

Also, directly from the above definition, we obtain the following

2.7  If p ⊩ φ(c_{1}, …, c_{n}), then M(p, i) ⊧ φ([c_{1}], …, [c_{n}])

for arbitrary standard φ with parameters c_{1}, …, c_{n} < l_{i+ℕ}. In particular, M(p, i) is a model of T ∩ ℕ for every T -evaluation p and i > ℕ. The converse of 2.7 is in general not true.

Therefore the formula HCons_{m}(φ), expressing the Herbrand consistency of φ with T_{m} can be assumed to have the form

∀i ∈ log^{3} ∃p V^{T_{m}+φ}(p, i).

More precisely, HCons_{m}(φ) looks like

2.8  ∀y∀i ≤ y[i ≤ log^{3} y ∧ y ≥ 2^{ω_{1}(l_{i})} ⇒ ∃p ≤ y V_{0}^{T_{m}+φ}(p, i, y)].

Finally, HCons(T_{m}) is HCons_{m}(“0 = 0”).

Sec.3

In order to prove that HCons_{m} and HCons_{m}^{I_{m}} have the required properties we need some auxiliary lemmas.

Lemma 3.2 and corollary 3.3 show that models M(p, i) are end-extensions of the intitial segment ≤^{M} i of M. Theorem 3.4 is the main step for proving (∗) of the introduction. It shows that M(p, i) is a stretching of M in the sense that an element i of log^{m+1} M gets an additional exponent in M(p, i) (falls into log^{m+2} M(p, i)). Finally we prove (∗) of the introduction.

3.1 Definition Let M ⊧ T_{m} be given, i_{0} ∈ log^{3} M. Let p be a T_{m}-evaluation on E_{i_{0}}. For i < i_{0} we define a numeral \underline{i} determined by p. The sentence ∀x∃y(y = x + 1) is an axiom of T_{m} and we may assume that this is the

first axiom in a fixed enumeration of T_{m}. It follows that

∀a < l_{i}∃b < l_{i+1} p ⊩ (b = a + 1)

for all i < i_{0}.

Hence there exists a sequence of names ⟨c_{i} : i < i_{0}⟩ such that

p ⊩ (c_{0} = 0) and p ⊩ (c_{i+1} = c_{i} + 1) for all i < i_{0}.

Let \underline{i} = c_{i} for i < i_{0}.

In the next lemma and corollary we shall show that \underline{i} is a name of the ith integer in models M(p, j) with j < i_{0} − ℕ, in the case where i_{0} is non standard.

3.2 Lemma.

Let p, i_{0} be as before. If, for some name a, p ⊩ (a ≤ \underline{i}), than there is a j ≤ i such that p ⊩ (a = \underline{j}). Moreover,

(∗)  φ(i_{1}, …, i_{n}), where i_{1}, …, i_{n} < i_{0}, implies p ⊩ φ(\underline{i}_{1}, …, \underline{i}_{n}),

for open φ with all terms indicated.

Proof.

Induction on i < i_{0}. For i = 0 we have p ⊩ (a ≤ \underline{i}), whence p ⊩ (a ≤ 0). Since the sentence ∀x(x ≤ 0 ⇒ x = 0) can be assumed to be an axiom of T_{m}, we get p ⊩ (a = 0), whence p ⊩ (a = \underline{0}). In the inductive step we apply, in a similar way, an axiom

∀x, y, z(y = z + 1 ∧ x ≤ y ⇒ x = y ∨ x ≤ z)

to p ⊩ (a ≤ \underline{i + 1}), i.e. to p ⊩ (a = \underline{i} + 1) and obtain p ⊩ (a = \underline{i + 1}) or p ⊩ (a ≤ \underline{i}). In the latter case we use the inductive assumption to infer p ⊩ (a = \underline{j}), for some j ≤ i.

For the second assertion of the lemma we prove first p ⊩ (\underline{i} + \underline{j} = \underline{i + j}) for all i, j such that i + j < i_{0}. We apply induction on j. Since p evaluates \underline{i} + \underline{0} as \underline{i} + 0, the axiom ∀x(x + 0 = x) yields immediately p ⊩ (\underline{i} + \underline{0} = \underline{i}). At the inductive step notice that p evaluates \underline{i} + \underline{j + 1} as \underline{i} + \underline{j} + 1 and hence as \underline{i + j} + 1, by the inductive assumption. On the other hand p ⊩ (\underline{i + j} + 1 = \underline{i + j + 1}), by definition of the numerals, which yields the required result. In a similar way we prove p ⊩ (\underline{i}·\underline{j} = \underline{i · j}) for all i, j such that i, j < i_{0} and also p ⊩ (\underline{i} < \underline{j}), whenever i ≤ j. This shows that (∗) holds for all atomic (and therefore also for all open) sentences φ, which finishes the proof of the lemma.

We have the following immediate corollary

3.3 Corollary

Let M be a model of T_{m}, i_{0} ∈ log^{3} M and p ∈ M a T_{m}-evaluation on E_{i_{0}+j}, where j > ℕ. Then the initial segment ≤ i_{0} of M is isomorphically embeddable into M(p, i_{0}) as an initial segment. Consequently, if a_{1}, …, a_{k} ∈ M, a_{1}, …, a_{k} ≤ i_{0}, φ(x_{1}, …, x_{k}) is bounded (with + and · treated as relations) and

M ⊧ φ(a_{1}, …, a_{k}),

then M(p, i_{0}) ⊧ φ([\underline{a}_{1}], …, [\underline{a}_{k}]).

Recall that I_{m} = log^{m−2} M.

Note that in the presence of Ω_{m}, the segment log^{m+1} M is closed under addition. For, we have

exp^{m+1}(2a) = exp^{m} 2^{2a} = exp^{m}(2^{a})^{2} = exp^{m}(ω_{0}(exp a)) = exp^{m−1}(ω_{1}(exp^{2} a))
= exp^{m−2}(ω_{2}(exp^{3} a)) = … = ω_{m}(exp^{m+1} a).

So, if exp^{m+1}(a) exists in a model of IΔ_{0} +Ω_{m}, then (in view of Ω_{m}), ω_{m}(exp^{m+1}(a)) exists, and thus exp^{m+1}(2a) exists. To see that exp^{m+1}(a + b) exists provided exp^{m+1}(a) and exp^{m+1}(b) exist, we show that exp^{m+1}(2 max a, b) exists, and then using the Δ_{0} minimum principle we infer the existence of exp^{m+1}(a + b).

It follows that I_{m} is closed under ω_{2}.

The following theorem implies the property (∗) of sec.1.

3.4 Theorem

Let M be a model of T_{m}, i_{0} ∈ log^{m+1} M, i_{0} > ℕ. Let p ∈ M be a T_{m}-evaluation on E_{2i_{0}}. Then the model M(p, i_{0}) satisfies

T_{m} + [\underline{i}_{0}] ∈ log^{m+2} .

Proof.

Since Ω_{m} is an axiom of T_{m} we have p ⊩ (∀x∃y y = ω_{m}(x)) and hence

∀a < l_{i}∃b < l_{i+1} p ⊩ (b = ω_{m}(a))

for each i < i_{0}. From 2.5 it follows that, for a fixed φ, the relation p ⊩ φ is Δ_{0} over M. Thus, there is a (code of) sequence of names ⟨w_{i} : i ≤ i_{0}⟩ ∈ M satisfying

∀i < i_{0} p ⊩ (w_{i+1} = ω_{m}(w_{i})) and p ⊩ (w_{0} = exp^{m} 2).

Clearly there is a standard n_{0} (depending on the position of Ω_{m} in the enumeration of axioms) such that w_{i} < l_{i+n_{0}} for each i ≤ i_{0}.

A simple checking shows (the superscript k denotes the kth iteration) that provably in T_{m},

3.6  exp^{m+2}(k) = ω_{m}^{k}(exp^{m} 2)

for each k ∈ log^{m+2}.

This can be proved in T_{m} by straightforward induction on l ≤ k applied to the formula exp^{m+2}(l) = ω_{m}^{l}(exp^{m} 2) which can be bounded by ω_{m}(exp^{m+2}(k)).

In fact the right hand side of 3.6, i.e. y = ω_{m}^{k}(exp^{m} 2) can be defined by an arithmetical formula with the help of the Gödel β-function: let ψ(x, y, a, b) be

β(a, b, 0) = exp^{m} 2 ∧ β(a, b, x) = y ∧ ∀i < xβ(a, b, i + 1) = ω_{m}(β(a, b, i))

where β(a, b, i) = r stands for

∃q(a = q · (b(i + 1) + 1) + r ∧ r < b(i + 1) + 1).

Now, y = ω_{m}^{x}(exp^{m} 2) can be defined by the formula ∃a, bψ(x, y, a, b).

In order to find a small enough name for a sequence corresponding to the w_{i}s, let 𝔐 be the model M(p, i_{0}) determined by p over M and consider the sequence s of iterations

s = ⟨exp^{m} 2, ω_{m}(exp^{m} 2), …, ω_{m}^{[\underline{k}]}(exp^{m} 2)⟩

of ω_{m} in 𝔐, where [\underline{k}] is the maximal j with the property ω_{m}^{j}(exp^{m} 2) ≤ [w_{i_{0}}] in 𝔐. Since the length and terms of s are relatively small, a standard reasoning shows that s has a β-code (a, b) in 𝔐, i.e.

∀i ≤ [\underline{k}] β(a, b, i) = ω_{m}^{i}(exp^{m} 2)

in 𝔐. Since 𝔐 = M(p, i_{0}), the elements a, b have names A and B, respectively, with A, B < l_{i_{0}+n_{1}} (for some standard n_{1} ∈ ℕ).

Moreover, there are names q_{i}, r_{i} < l_{i_{0}+n_{i}} for an n_{i} ∈ ℕ such that

3.7  p ⊩ (A = q_{i}(B(i + 1) + 1) + r_{i} ∧ r_{i} < B(i + 1) + 1),

for each i ≤ k.

We shall show that there is a sequence ⟨q_{i}, r_{i} : i ≤ k⟩ in M such that q_{i}, r_{i} < l_{i_{0}+n_{i}} for an n_{i} ∈ ℕ and 3.7 holds.

For, we have in M

∀i ≤ k∃q_{i}, r_{i} p ⊩ (A = q_{i}(B(i + 1) + 1) + r_{i} ∧ r_{i} < B(i + 1) + 1).

Choose now q_{i}, r_{i} in M, for i ≤ k, so that q_{i}, r_{i} satisfy 3.7 and the least j such that q_{i}, r_{i} < l_{i_{0}+j} is the least possible. Then j ∈ ℕ and the sequence ⟨q_{i}, r_{i} : i ≤ k⟩ is Δ_{0} definable in M, so it is in M.

An easy induction in M shows that

3.8  p ⊩ (r_{i} = w_{i})

for each i ≤ k. For, assume 3.8 for a given i < k. Thus

𝔐 ⊧ [r_{i}] = [w_{i}].

By construction of the w’s, p ⊩ (w_{i+1} = ω_{m}(w_{i})). Hence [w_{i+1}] = ω_{m}([r_{i}]) = [r_{i+1}] in 𝔐, which proves 3.8.

In particular we have

[r_{k}] = [w_{k}].

Suppose k < i_{0}. Then, p ⊩ (w_{k+1} = ω_{m}(w_{k})), whence in 𝔐

ω_{m}^{[\underline{k+1}]}(exp^{m} 2) = ω_{m}(ω_{m}^{[\underline{k}]}(exp^{m} 2)) = ω_{m}([r_{k}]) = ω_{m}([w_{k}]) = [w_{k+1}] ≤ [w_{i_{0}}],

which contradicts the maximality of k. Hence k = i_{0}, and therefore 3.8 holds for each i ≤ i_{0}.

Note that

𝔐 ⊧ [r_{i}] = ω_{m}^{[\underline{i}]}(exp^{m} 2),

by the choice of a, b and A, B.

Hence

𝔐 ⊧ [w_{i_{0}}] = ω_{m}^{[\underline{i}_{0}]}(exp^{m} 2) = exp^{m+2}[\underline{i}_{0}].

Thus the proof of the theorem has been completed.

Now we shall show (∗) of section 1. Consider first a model M of

T_{m} + ∃x̄ ∈ log^{m+1} φ(x̄) + HCons^{I_{m}}(“0 = 0”).

Let ā ∈ log^{m+1} M, ā = a_{1}, …, a_{k} be such that M ⊧ φ(ā). Let i_{0} = max ā. By the fact that log^{m+1} M is closed under addition we infer

M ⊧ ∃p V^{T_{m}}(p, 2i_{0}).

Fix p. By corollary 3.3, M(p, i_{0}) ⊧ φ([\underline{a}_{1}], …, [\underline{a}_{k}]). By theorem 3.4,

M(p, i_{0}) ⊧ T_{m} + φ([\underline{a}_{1}], …, [\underline{a}_{k}]) + [\underline{a}_{1}], …, [\underline{a}_{k}] ∈ log^{m+2} .

Hence the theory

T_{m} + ∃x̄ ∈ log^{m+2} φ(x̄)

is consistent and (∗) follows.

References

[A] Z. Adamowicz, A contribution to the end-extension problem and the Π_{1} conservativeness problem, Annals of Pure and applied Logic 61(1993) 3-48

[AZ] Z. Adamowicz, P. Zbierski , On Herbrand type consistency in weak theories, Archive for Mathematical Logic, to appear

[B] S.R. Buss, Bounded Arithmetic, Bibliopolis, 1986

[DP] K. Dimitrakopoulos, J. Paris, Truth definitions for Δ_{0} formulae, Logic and Algorithmic, Monographie No. 30 de l’Enseignement Mathématique, Genève 1982, 319-329

[HP] P.Hajek, P.Pudlak, Metamathematics of first order arithmetic, Berlin 1993, Springer-Verlag 8 XIV 460 Perspectives in mathematical Logic

[L] H.Lessan, Models of arithmetic, Dissertation, Mancheter.

[PW] J. Paris and A. Wilkie, Δ_{0} sets and induction, Proceedings of the Jadwisin Logic Conference, Poland, Leeds University Press, 1981, 237-248

[P] P. Pudlak, Cuts, consistency statements and interpretations, Journal of Symbolic Logic Vol. 50, Number 2, June 1985

[W] D. Willard, The semantic Tableau version of the second incompleteness theorem extends almost to Robinson’s arithmetic Q, circulating manuscript

[WP1] A.Wilkie and J.Paris, On the scheme of induction for bounded arithmetic formulas, Annals of Pure and applied Logic 35(1987) 261-302

[WP2] A.Wilkie and J.Paris, On the existence of end-extensions of models of bounded induction” Proceedings of the International Congress of Logic, Philosophy and Methodology of Science, Moscow 1987