PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 63 (77), 1998, 1–8

CONSTRUCTING KRIPKE MODELS OF CERTAIN FRAGMENTS OF HEYTING’S ARITHMETIC

Kai F. Wehmeier

Communicated by Žarko Mijajlović

Abstract. We present nontrivial methods of constructing Kripke models for the fragments of HA obtained by restricting the induction schema to instances with Π_{1}- and Π_{2}-induction formulae respectively. The model construction for Π_{1}- induction was applied in [W96a] and [W97] to investigate the provably recursive functions of this theory. The construction of Π_{2}-induction models is a modification of Smoryński’s collection operation introduced in [S73].

1. Introduction

A Kripke structure K for a first-order language L is a pair

K = ((K, ≤), (A_{α})_{α∈K})

such that (K, ≤) is a (nonempty) reflexive partial order (the frame of K) and for each α ∈ K, A_{α} is a classical L-structure A_{α} = (A_{α}, =_{α}, (R_{α})_{R∈L}, (f_{α})_{f∈L}) (not necessarily normal, i.e., =_{α} need not be true equality on A_{α}), with the proviso that the following ‘monotonicity conditions’ be fulfilled:

Whenever α ≤ β, then

1. A_{α} is a subset of A_{β};

2. for every relation symbol R of L (including equality =): R_{α} ⊆ R_{β};

3. for every n-ary function symbol f of L: f_{α} is the function f_{β} restricted to A_{α}^{n}. The forcing relation ⊩_{K}, ⊩ for short, is defined as usual. K ⊧ ϕ means that for

all α ∈ K, α ⊩ ϕ. We also use ⊧ for the classical satisfaction relation, sometimes writing α ⊧ ϕ instead of A_{α} ⊧ ϕ. We consider here the usual arithmetical language L_{ar} given by 0, S, +, · and <. iΔ_{0} is the intuitionistic L_{ar}-theory axiomatized by the usual axioms for PA^{−} (cf. [K91]) together with the axiom schema of induction for Δ_{0}-formulae. IΔ_{0} is the classical version of iΔ_{0}, i.e., iΔ_{0} augmented by classical logic. Σ_{1} is the class of L_{ar}-formulae of the form ∃ȳφ(x̄, ȳ), Π_{1} the class of L_{ar}- formulae ∀ȳφ(x̄, ȳ) with, in both cases, φ in Δ_{0}. Given a formula class Γ, iΓ is iΔ_{0} plus induction over all formulae in Γ (IΓ being the corresponding classical theory). HA is iΔ_{0} together with the axiom schema of induction for arbitrary formulae of L_{ar}, its classical counterpart is PA. Note that in iΔ_{0}, Δ_{0}-formulae are decidable.

AMS Subject Classification (1991): Primary 03F50, 03F55, 03F30 The contents of this article were part of a talk given in the Mathematical Logic Seminar of the Mathematical Institute in Belgrade on June 20, 1997. The present paper draws on results of my doctoral dissertation.

As a consequence, we have the following

1.1 Lemma. Let K = ((K, ≤), (A_{α})_{α∈K}) be any Kripke structure for L_{ar}. The following are equivalent:

1. K ⊧ iΔ_{0}, i.e., for each α ∈ K, α ⊩ iΔ_{0}.

2. For each α ∈ K, A_{α} is a classical model of IΔ_{0} (i.e., α ⊧ IΔ_{0}) and whenever α ≤ β in K, A_{α} ≺_{Δ_{0}} A_{β}. Under these conditions, we have for each α ∈ K, each Δ_{0}-formula ϕ(x̄) and

each ā ∈ A_{α}:

α ⊩ ϕ(ā) ⟺ α ⊧ ϕ(ā). □

For a proof, see [W96a]. If atomic formulae (and hence quantifier-free formulae, cf. [M84]) are decidable in K (as will be the case for K ⊧ iΔ_{0}), we may assume without loss of generality that every A_{α} is a normal structure and that, whenever α ≤ β in K, A_{α} is a substructure of A_{β} (such K will be called normal Kripke structures):

1.2 Lemma. Let K = ((K, ≤), (A_{α})_{α∈K}) be a Kripke structure for a language L such that K ⊧ ∀x̄(P x̄ ∨ ¬P x̄) for each atomic formula P x̄ of L. Then there is a Kripke structure K^{+} = ((K, ≤), (B_{α})_{α∈K}) for L such that every B_{α} is a normal structure and whenever α ≤ β in K, B_{α} is a substructure of B_{β}, and such that K ⊧ ϕ ⟺ K^{+} ⊧ ϕ for each L-sentence ϕ. □

This fact was already pointed out by Smoryński in [S73]; however, there are two pitfalls in proving it. Smoryński notes that one cannot just divide out =_{α} locally, since the equivalence classes may grow when passing from α to some β ≥ α, and so one will not obtain actual inclusion of domains. His proposal is to divide out globally as follows (note that he does not consider function symbols):

Let D := ⋃_{α∈K} A_{α}. For c, d ∈ D define c ∼ d : ⟺ ∃α ∈ K c =_{α} d. Put B_{α} := {[c] : c ∈ A_{α}}, where [c] is the equivalence class of c under ∼, let R_{B_{α}}([c_{1}], ..., [c_{n}]) : ⟺ R_{A_{α}}(d_{1}, ..., d_{n}) for some elements d_{1},…, d_{n} ∈ A_{α} such that d_{i} ∈ [c_{i}].

But there is a problem here: ‘By accident’, one and the same object may exist in worlds of incomparable nodes of the frame, and with incompatible properties in the respective worlds. Thus, let α, β and γ be nodes such that α < β, α < γ, but β ≰ γ and γ ≰ β. Assume that A_{α} does not contain the object c, whereas a ∈ A_{α}.

Then it is possible that a =_{β} c and a≠_{γ}c. Clearly, this makes it impossible to identify a and c.

Instead, it is necessary to proceed as follows: In a first step, divide out the equality relations =_{α} locally. In a second step, for α ≤ β, identify two equivalence classes [a]_{=_{α}} and [b]_{=_{β}} if [a]_{=_{α}} ⊆ [b]_{=_{β}}, then take the transitive closure. The easy but tedious verification is left to the reader.

Given some set of axioms T, a Kripke structure K = ((K, ≤), (A_{α})_{α∈K}) for the language of T is called T -normal or locally T if for each α ∈ K, the structure A_{α} is a classical model of T, A_{α} ⊧ T. The interplay of sets of axioms being forced at α and those being classically true in A_{α} is intriguing, see e.g. [W96].

2. Smorynski’s collection operation

In his [S73], Smoryński introduced a powerful collection operation on Kripke structures which he used to prove a large number of results on intuitionistic logic and arithmetic. The idea behind his operation (∑ )′ is this:

Let some family F = {K^{i} : i ∈ I} of Kripke structures

K^{i} = ((K^{i}, ≤^{i}), (A_{α}^{i})_{α∈K^{i}})

for some version L of the arithmetical language (containing a closed term for each natural number n) be given. We may assume without loss of generality that for i ≠ j in I, K^{i} ∩ K^{j} = ∅.

We obtain a new Kripke structure by forming the disjoint union ΣF = K = ((K, ≤), (A_{α})_{α∈K}) of F, putting

• K = ⋃_{i∈I} K^{i};

• for α, β ∈ K, α ≤ β : ⟺ for some i ∈ I, α ≤^{i} β;

• for α ∈ K, A_{α} := A_{α}^{i}, where i ∈ I is such that α ∈ K^{i}.

Observing that for each α ∈ K^{i}, K_{α}^{i} = K_{α}, we see that if each K^{i} ⊧ T for some theory T, then K = ΣF ⊧ T. The operation of disjoint union becomes interesting only in conjunction with a second operation K ↦ K′ which consists in attaching a (new) root to K:

Given a normal Kripke structure K, K′ is obtained from K by adding a new node α_{0} to K (i.e., K′ := K ⊎ {α_{0}}), stipulating that α_{0} be minimal in K′ (i.e., ≤′:=≤ ∪{(α_{0}, β) : β ∈ K′}) and letting A_{α_{0}} be the standard model of arithmetic ℕ.

Note that the restriction to normal models, or at least an assumption that all worlds are normal in their ‘standard part’ given by the numerals, is important here: The interpretations f_{α} of function symbols f are actual functions, compatible with =_{α} but not multi-valued. Thus e.g. in the standard model A_{α_{0}}, we certainly have S_{α}(0) = 1 (true equality!), whereas at some node β from K, only S_{β}(0) =_{β} 1 is required, and we may actually have S_{β}(0) = c for some c ∈ A_{β} such that c ≠ 1 (but of course c =_{β} 1). This would collide with the requirement that S_{α_{0}} be the restriction of S_{β} to A_{α_{0}}. But this cannot happen if we exclude non-normal models from the start (which, by Lemma 1.2, is no real restriction).

It is now easy to see that K′ is again a Kripke structure; more difficult is the question which theories T are preserved under this operation, i.e., for which theories T is K′ a model of T, provided that K ⊧ T?

Smoryński has shown that HA and some of its extensions are preserved under the ′ operation. We briefly go through his proof, pointing out the punch line and in fact showing that every fragment iΓ of HA is preserved.

2.1 Theorem (Smoryński). Let K ⊧ iΓ. Then K′ ⊧ iΓ too.

Proof . Clearly it is sufficient to show that α_{0} ⊩′ iΓ (writing ⊩′ for ⊩_{K}_{′}). The crucial axioms to check are the induction axioms. So let φ(x, z̄) ∈ Γ; we must show that

α_{0} ⊩′ ∀z̄[φ(0, z̄) ∧ ∀x(φ(x, z̄) → φ(Sx, z̄)) → ∀x φ(x, z̄)].

Assume the contrary. Then for some β ≥′ α_{0} and b̄ ∈ A_{β},

β ⊮′ φ(0, b̄) ∧ ∀x(φ(x, b̄) → φ(Sx, b̄)) → ∀x φ(x, b̄).

The assumption that β > α_{0} leads to a contradiction, since at such β, ⊩ and ⊩′ coincide, and so β ⊩′ iΓ.

Hence β = α_{0} and b̄ ∈ A_{α_{0}} = ℕ. We thus have (now suppressing parameters from A_{α_{0}}):

α_{0} ⊮′ φ(0) ∧ ∀x(φ(x) → φ(Sx)) → ∀x φ(x),

i.e., for some β ≥′ α_{0},

β ⊩′ φ(0) ∧ ∀x(φ(x) → φ(Sx))

but β ⊮′ ∀x φ(x). Again β > α_{0} is impossible since then β ⊩′ iΓ. So we have (i) α_{0} ⊩′ φ(0) ∧ ∀x(φ(x) → φ(Sx)) and (ii) α_{0} ⊮′ ∀x φ(x).

By (i) and the fact that for β > α_{0} we have β ⊩′ iΓ we conclude that for all β > α_{0}, β ⊩′ ∀x φ(x). Hence we may infer from (ii) that for some n ∈ A_{α_{0}} = ℕ, α_{0} ⊮ φ(n). Here’s the punch line: Let m be the least number n such that α_{0} ⊮′ φ(n). Such a minimal counterexample exists since we are in the standard model ℕ. (If A_{α_{0}} were nonstandard, we would have to know that the forcing relation at α_{0} is suitably definable in A_{α_{0}}.) Now since α_{0} ⊩′ φ(0), we have m ≠ 0, so m = Sk for some k ∈ ℕ. By minimality of m, α_{0} ⊩′ φ(k), so by α_{0} ⊩′ ∀x(φ(x) → φ(Sx)) we obtain α_{0} ⊩′ φ(m), contradiction. □

2.2 Corollary. Every theory of the form iΓ has the explicit definability property (ED) and the disjunction property (DP), i.e., whenever iΓ proves a sentence ∃x φ(x), then for some n ∈ ℕ, iΓ ⊢ φ(n), and whenever iΓ proves a sentence ψ∨χ, then either iΓ ⊢ ψ or iΓ ⊢ χ.

Proof. We consider only (ED). Suppose that iΓ ⊬ φ(n) for each n ∈ ℕ. By the completeness theorem, for each n there is a Kripke model K_{n} ⊧ iΓ with K_{n} |̸= φ(n). Now consider (∑_{n∈ℕ} K_{n})′ =: K′ which is a model of iΓ by theorem 2.1. Obviously, α_{0} ⊮′ ∃x φ(x), since this would imply α_{0} ⊩′ φ(n) for some n ∈ A_{α_{0}} = ℕ, which is impossible by K_{n} |̸= φ(n). By the soundness theorem, iΓ ⊬ ∃x φ(x). □

Smoryński’s idea obviously yields a construction method for Kripke models that can be summarized as follows:

2.3 Theorem. Let (K, ≤) be any conversely wellfounded tree. Attach arbitrary models of IΓ to terminal nodes of (K, ≤) and the standard model ℕ of arithmetic to each internal node of (K, ≤). The resulting Kripke structure is then a model of iΓ.

3. Constructing models of Π_{1}-induction

Sam Buss has shown in [B93] that there is an easy way to construct Kripke models of iΣ_{1} over arbitrary frames: Every IΣ_{1}-normal Kripke structure is a Kripke model of iΣ_{1}. But he also illustrates, by way of counterexample, that it is not as trivial to construct models of iΠ_{1}. However, models of iΠ_{1} over conversely wellfounded frames are not too difficult to build:

3.1 Lemma. Let K = ((K, ≤), (A_{α})_{α∈K}) be a Kripke structure such that for each β ∈ K there is a terminal node α ≥ β in K (this is always the case when (K, ≤) is conversely wellfounded). Suppose further that for all terminal nodes α ∈ K, A_{α} ⊧ IΣ_{1} and that for all internal nodes β ∈ K, A_{β} ⊧ IΔ_{0}. Assume that whenever α ≤ β in K, A_{β} is a Δ_{0}-elementary extension of A_{α}. Then K ⊧ iΠ_{1}.

Proof. We proceed by brute force (see [W96a] for an alternative proof). Take any α ∈ K and let ψ(x, ȳ, z̄) be a Δ_{0}-formula. We have to prove that α forces

∀z̄(∀ȳψ(0, ȳ, z̄) ∧ ∀x(∀ȳψ(x, ȳ, z̄) → ∀ȳψ(Sx, ȳ, z̄)) → ∀x∀ȳψ(x, ȳ, z̄)).

So let β ≥ α, b̄ ∈ A_{β} and suppose that

β ⊩ ∀ȳψ(0, ȳ, b̄) ∧ ∀x(∀ȳψ(x, ȳ, b̄) → ∀ȳψ(Sx, ȳ, b̄)).

Thus every terminal node above β classically satisfies this last sentence. Since all terminal nodes are classical models of IΣ_{1} (≡ IΠ_{1}), every such node also satisfies ∀x∀ȳψ(x, ȳ, b̄)). This sentence is Π_{1} and thus downwards preserved in Δ_{0}- elementary extensions. In particular, it is classically true in every γ ≥ β. But we want to show that β ⊩ ∀x∀ȳψ(x, ȳ, b̄). However, this just means that for all γ ≥ β and all c, d̄ ∈ A_{γ}, γ ⊩ ψ(c, d̄, b̄), i.e., by 1.1 that γ ⊧ ∀x∀ȳψ(x, ȳ, b̄), which, as we have just seen, is indeed the case. □

3.2 Remark. This result shows that Buss’ counterexample is not just accidentally not conversely wellfounded: Every PA-normal Kripke structure on conversely wellfounded frames validates iΠ_{1}.

4. Some general Kripke model theory

In the next section, we will use a modification of Smoryński’s (∑ )′ operation to construct models of iΠ_{2} from arbitrary classical models of IΣ_{2}. The present section develops a little theorem in general Kripke model theory as a preparation for that result.

4.1 Definition. A formula φ of some language L is positive if it is built up from atomic formulae using only ∧, ∨ and ∃.

4.2 Remark. For all Kripke structures K, α ∈ K, ā ∈ A_{α} and every positive formula φ(x̄) we have: α ⊩ φ(ā) ⟺ α ⊧ φ(ā). (In fact this property characterizes the positive formulae: If always α ⊩ φ(ā) ⟺ α ⊧ φ(ā), then φ is intuitionistically equivalent to a positive formula; cf. [M83].) If in the respective Kripke model Δ_{0}-formulae are decidable, we may, by 1.1, relax the definition of positivity by replacing ‘atomic’ with ‘Δ_{0}’, and the property will continue to hold.

4.3 Definition. Let Γ be the smallest class of formulae containing the positive formulae, closed under application of ∀ and ∧ and under the following rule: If φ is positive and ψ ∈ Γ, then φ → ψ is in Γ.

4.4 Remark. Under classical logic, Γ is the class of ∀∃-formulae. This is also true in intuitionistic theories within which atomic formulae are decidable.

4.5 Lemma. Let φ(z̄) ∈ Γ, let K be a Kripke structure, α ∈ K, ā ∈ A_{α} and suppose that for all β > α we have β ⊩ φ(ā). Then:

α ⊩ φ(ā) ⟺ α ⊧ φ(ā).

Proof. We proceed by induction on the definition of φ ∈ Γ.

If φ(z̄) is positive, then the claim follows from our remark above. Using the induction hypothesis, the case of conjunction is trivial.

So suppose that φ(z̄) is of the form ∀y ψ(y, z̄) with ψ(y, z̄) ∈ Γ. By assumption for all β > α, β ⊩ ∀y ψ(y, ā). (We will from now on suppress mention of the parameters ā and just write ∀y ψ(y).) First suppose that α ⊩ ∀y ψ(y). In particular, for all c ∈ A_{α}, α ⊩ ψ(c), and so by persistence of forcing, for all c ∈ A_{α} and all β ≥ α β ⊩ ψ(c). By the induction hypothesis then for all c ∈ A_{α} α ⊧ ψ(c), i.e., α ⊧ ∀y ψ(y).

Now suppose that α ⊮ ∀y ψ(y). By definition, for some β ≥ α and some c ∈ A_{β}, β ⊮ ψ(c). But since all β > α force ∀y ψ(y), we must have α ⊮ ψ(c) for some c ∈ A_{α}. But for all β > α β ⊩ ψ(c) and so by induction hypothesis α |̸= ψ(c) and thus α |̸= ∀y ψ(y).

For the case of implication, suppose φ is of the form ψ → χ, where ψ is positive and χ ∈ Γ. (We are again suppressing parameters from A_{α}.) Assume that for all β > α, β ⊩ ψ → χ.

First let α ⊩ ψ → χ. We consider two cases. For the first case, suppose that α ⊩ ψ. Then for all β ≥ α β ⊩ ψ and thus for all β ≥ α β ⊩ χ. By induction hypothesis then α ⊧ χ and of course α ⊧ ψ → χ. In the second case α ⊮ ψ. Since ψ is positive, we then have α |̸= ψ and so vacuously α ⊧ ψ → χ.

For the other direction, assume that α ⊮ ψ → χ. Then for some β ≥ α β ⊩ ψ and β ⊮ χ. Since by assumption for all β > α β ⊩ ψ → χ, we must in fact have α ⊩ ψ and α ⊮ χ. Since α ⊩ ψ, for all β > α β ⊩ χ. Hence by induction hypothesis α |̸= χ. α ⊩ ψ and ψ is positive, so α ⊧ ψ. Together we get α |̸= ψ → χ. □

4.6 Question. Does the property exhibited in Lemma 4.5 characterize the class Γ?

4.7 Remark. If Δ_{0}-formulae are decidable in the model under consideration, the theorem remains true if we use the relaxed definition of positivity indicated in remark 4.2 in the definition of Γ (cf. lemma 1.1), so that we are then talking about Π_{2}-formulae.

5. Constructing models of Π_{2}-induction

In the variant indicated at the end of the previous section, we can use our result 4.5 to construct certain models of the intuitionistic version iΠ_{2} of IΠ_{2}:

5.1 Theorem. Let K be an IΣ_{2}-normal Kripke structure over a conversely wellfounded frame. Then K is a model of iΠ_{2}, i.e., for each α ∈ K, ā ∈ A_{α} and every Π_{2}-formula φ(x, ȳ) we have

α ⊩ φ(0, ā) ∧ ∀x(φ(x, ā) → φ(Sx, ā)) → ∀x φ(x, ā).

Proof. Note that in IΣ_{2}-normal Kripke structures all extensions are Δ_{0}- elementary (since the MRDP theorem can be proved in IΣ_{2}, cf. [HP93]), and so K ⊧ iΔ_{0} by 1.1.

We proceed by bar induction on α. For terminal α there is nothing to show since IΠ_{2} ≡ IΣ_{2}.

So let α be an internal node and suppose that

α ⊮ φ(0, ā) ∧ ∀x(φ(x, ā) → φ(Sx, ā)) → ∀x φ(x, ā).

Then for some β ≥ α we have β ⊩ φ(0, ā), β ⊩ ∀x(φ(x, ā) → φ(Sx, ā)) and β ⊮ ∀x φ(x, ā). But by induction hypothesis, we must have β = α, so α ⊩ φ(0, ā), α ⊩ ∀x(φ(x, ā) → φ(Sx, ā)) and α ⊮ ∀x φ(x, ā).

By persistence of ⊩ we obtain for each β > α that β ⊩ φ(0, ā), β ⊩ ∀x(φ(x, ā) → φ(Sx, ā)) and hence by induction hypothesis that β ⊩ ∀x φ(x, ā). So it follows from α ⊮ ∀x φ(x, ā) that already for some b ∈ A_{α}, α ⊮ φ(b, ā); however, for each β > α we have β ⊩ φ(b, ā) and φ is Π_{2}, so by 4.5 α |̸= φ(b, ā). Now let c be the least element e of A_{α} such that α |̸= φ(e, ā). (This is possible since α ⊧ IΠ_{2}.)

Then the following obtain:

1. α ⊮ φ(c, ā) (by 4.5, since α |̸= φ(c, ā) and for all β > α we have β ⊩ φ(c, ā));

2. for each d <_{α} c, α ⊩ φ(d, ā) (again by 4.5, since for d <_{α} c α ⊧ φ(d, ā) and for each β > α β ⊩ φ(d, ā)). But now c is not 0, since α ⊩ φ(0, ā) and α ⊮ φ(c, ā). Hence c = Sd for

some d ∈ A_{α}. But by 2. α ⊩ φ(d, ā), so by α ⊩ ∀x(φ(x, ā) → φ(Sx, ā)) we get α ⊩ φ(Sd, ā), i.e., α ⊩ φ(c, ā), contradicting 1. □

5.2 Remark. It is clear by Theorem 5.1 that every PA-normal Kripke structure over a wellfounded frame is a model of iΠ_{2}. This result is in some sense optimal: Zambella and Visser show in a forthcoming paper that there are PA-normal Kripke structures over two-element frames, the respective PA-models an end-extension, which are not models of iΣ_{2}.

References

[B93] S. Buss, Intuitionistic validity in T-normal Kripke structures, Ann. Pure Appl. Logic 59 (1993), 159–173

[HP93] P. Hajek and P. Pudlak, Metamathematics of First-Order Arithmetic, Springer-Verlag, Berlin, Heidelberg, New York, 1993

[K91] R. Kaye, Models of Peano Arithmetic, Oxford University Press, Oxford, 1991

[M83] Z. Marković, Some preservation results for classical and intuitionistic satisfiability in Kripke models, Notre Dame J. Formal Logic 24 (1983), 395–398

[M84] Z. Marković, Kripke models for intuitionistic theories with decidable atomic formulas, Publ. Inst. Math. (Beograd)(N.S.) 36 (50) (1984), 3–7

[M93] Z. Marković, On the structure of Kripke models of Heyting arithmetic, Math Logic Quart. 39 (1993), 531–538

[S73] C. Smorynski, Applications of Kripke Models, in: [T73], 324–391

[T73] A. S. Troelstra (ed.), Metamathematical Investigations of Intuitionistic Arithmetic and Analysis, Springer-Verlag, Berlin, Heidelberg, New York, 1973

[W96] K. F. Wehmeier, Classical and intuitionistic models of arithmetic, Notre Dame J. Formal Logic 37 (1996), 452–461

[W96a] K. F. Wehmeier, Semantical Investigations in Intuitionistic First-order Arithmetic, Dissertation, Münster, 1996

[W97] K. F. Wehmeier, Fragments of HA based on Σ_{1}-induction, Arch. Math. Logic 37 (1997), 37–49

Institut für Mathematische Logik (Received 08 10 1997) und Grundlagenforschung Einsteinstr. 62 D-48149 Münster, Germany