The Modal Completeness of ILW

Dick de Jongh Frank Veltman

Abstract

This paper contains a completeness proof for the system ILW, a rather bewildering axiom system belonging to the family of interpretability logics. We have treasured this little proof for a considerable time, keeping it just for ourselves. Johan’s fiftieth birthday appears to be the right occasion to get it out of our wine cellar.

Contents

1 Introduction 2

2 Semantics 3

3 Modal completeness 3

1 Introduction

In interpretability logic the logical properties of the notion of interpretability are studied in much the same way as the logical properties of the notion of provability are studied in provability logic. In the latter a one-place operator □ is added to the language of propositional logic. The intended meaning in the context of an arithmetical theory T of a formula □A is ‘A is provable in T ’ (where A represents an arithmethic formula). In the former, a binary operator ⊳ is added to the language of propositional logic. Here the intended meaning of A ⊳ B (read ‘A interprets B’) in an arithmetical theory T is: ‘T + B is interpretable in T + A’.

Interpretability logic extends provability logic: □ is definable in terms of ⊳ via the equation □A =_{def} ¬A ⊳ ⊥. Thus, in principle, interpretability logic can disclose at least as much about the underlying arithmetical theory T as provability logic can. Actually, it does disclose more. Provability is a stable notion, interpretability is not. All extensions of IΔ_{0} + EXP have the same provability logic. But as it turns out, the interpretability logic ILM of Peano Arithmetic differs widely from the interpretability logic ILP of ACA_{0} (the arithmetical counterpart of Gödel-Bernays set theory).

All interpretability logics studied so far are extensions of the core system IL, which is given by the derivation rules Modus Ponens and Necessitation and the axioms □A → □□A and □(□A → A) → □A (Löb’s Axiom) of the provability system L, plus the axioms:

(J1) □(A → B) → (A ⊳ B)

(J2) (A ⊳ B) ∧ (B ⊳ C) → (A ⊳ C)

(J3) (A ⊳ C) ∧ (B ⊳ C) → (A ∨ B ⊳ C)

(J4) (A ⊳ B) → (♢A → ♢B)

(J5) ♢A ⊳ A

(With respect to priority of parentheses ⊳ is treated as →.)

By adding the scheme (A ⊳ B) → (A ∧ □C ⊳ B ∧ □C) one gets the system ILM mentioned above. ILP is given by IL plus the scheme (A ⊳ B) → □(A ⊳ B). Central in this paper is a third extension of IL, the system ILW described e.g. in Visser [7]. ILW = IL + W, where W is the axiom scheme

(A ⊳ B) → (A ⊳ B ∧ □¬A)

The system ILW is contained in both ILM and ILP (see de Jongh-Veltman [2], or Visser [6]), and was at some point conjectured to embody the principles common to all “reasonable” arithmetics. In the meantime, however, Albert Visser discovered two new general principles, M_{0}: A ⊳ B → (♢A ∧ □C ⊳ B ∧ □C) (see Visser [7]), and P_{0}: A ⊳ ♢B → □(A ⊳ B) (see Joosten [5]).

¿From a purely modal point of view, it seems wise to first take a proper look at ILW, before trying to get to grips with a system like ILWM_{0}P_{0}. Indeed, as the completeness proof presented below will show, ILW already poses so many problems that the predicate ‘bewildering’ comes to mind.

2 Semantics

It is a well-known fact that the modal logic L is complete with respect to the L-frames ⟨W, R⟩, which consist of a set of worlds W together with a transitive conversely well-founded relation R.

Definition 1 If ⟨W, R⟩ is a partially ordered set and w^{∈} W, then wR = {w′^{∈} W | wR w′}.

Definition 2 An IL-frame is a L-frame ⟨W, R⟩ with an additional relation S_{w} for each w^{∈} W, which has the following properties:

(i) S_{w} is a relation on w R, (ii) S_{w} is reflexive and transitive, (iii) if w′, w′′^{∈} w R and w′ R w′′, then w′S_{w}w′′.

We will often write S for {S_{w} | w^{∈} W }.

Definition 3 An IL-model is given by an IL-frame ⟨W, R, S⟩ combined with a forcing relation with the clauses:

(i) u^{||−}□A iff ∀v(uRv ⇒ v^{||−}A),

(ii) u^{||−}A ⊳ B iff ∀v(u R v and v^{||−}A ⇒ ∃w(vS_{u}w and w^{||−}B)).

Definition 4

(a) For F = ⟨W, R, S⟩, we write F ^{||−}A iff w^{||−}A for every ^{||−} on F and every w^{∈} W.

(b) If K is a class of frames, we write K^{||−}A iff F ^{||−}A for each F ^{∈} K .

(c) K_{W} is the class of IL-frames with the additional property (iv) for any w, the converse of R ∘ S_{w} is well-founded.

The next lemma states that the scheme W characterizes the class of frames K_{W}.

Lemma 5 (a) For each A, if ⊢_{IL} A, then F ^{||−}A.

(b) F ^{||−}ILW iff F ^{∈} K_{W} (ILW characterizes K_{W}). Proof. Straightforward. ⊣

3 Modal completeness

The usual method in modal logic for obtaining completeness proofs is to construct directly or indirectly the necessary countermodels by taking maximal consistent sets of the logic under consideration as the worlds of the model. There are three problems with this approach here. First, there is a problem deriving from the modal logic L which is the basis of our system. This logic is not compact: some infinite syntactically consistent sets of formulae are semantically incoherent. A solution is to restrict the maximal consistent sets to subsets of some finite set of formulae. Such a so-called adequate set has to be rich enough to prove the analogon of the valuation lemma which states that a formula A belonging to the adequate set is forced in a world w iff A^{∈} w. Therefore it has to be closed under forming of subformulae and single negations. Furthermore, for each particular logic, additional requirements on the adequate set will be needed to be able to apply the axioms.

It turns out that for ILW we need the following.

Definition 6 An adequate set of formulae is a set Φ which fulfills the following conditions:

(i) Φ is closed under the taking of subformulae, (ii) if B^{∈} Φ, and B is not a negation, then ¬B^{∈} Φ, (iii) ⊥ ⊳ ⊥^{∈} Φ, (iv) if B as well as C are the antecedent or consequent of some ⊳ -formula

in Φ, then B ⊳ C^{∈} Φ.

It is not difficult to see that each finite set Γ of formulae is contained in a finite adequate set Φ.

In this connection, we consider ♢A to be shorthand for ¬(A ⊳ ⊥), and □A short for ¬A ⊳ ⊥ (unless A is ¬B; then □A stands for B ⊳ ⊥), so that we can ignore □- and ♢-formulas in inductions. Note that in this way we can be sure that, if B ⊳ C is a member of an adequate set, then so are ♢B and ♢C.

As usual, we define Γ ≺ Δ ⇔ (i) for each □A^{∈} Γ, it holds that □A, A^{∈} Δ, and (ii) for some □A^{/ ∈} Γ, it holds that □A^{∈} Δ. Whenever Γ ≺ Δ, we say that Δ is a successor of Γ. The following lemma transfers from L to IL and its extensions.

Lemma 7 Let Γ_{0} be a maximal ILW-consistent subset of some finite adequate Φ, and let W_{Γ_{0}} be the smallest set such that (i) Γ_{0}^{∈} W (ii) if Δ^{∈} W and Δ′ is a maximal ILW-consistent subset of Φ such that Δ ≺ Δ′, then Δ′^{∈} W. Then

(i) ≺ is transitive and irreflexive on W_{Γ_{0}}, (ii) for each Γ^{∈} W_{Γ_{0}}, □A^{∈} Γ ⇔ A^{∈} Δ for every Δ such that Γ ≺ Δ.

The model supplied by this lemma works fine in a completeness proof for L, but it is much too small for IL and its extensions. It is not always possible endow ⟨W_{Γ_{0}}, ≺ ⟩ with relations S_{Γ} for every Γ^{∈} W_{Γ_{0}} in such a way that (i) S has all the properties required, and (ii) the valuation lemma can be proved for ⊳ - formulas. We can no longer identify a world with the set of formulas true in it. In the eventual model it will often occur that different worlds are described by the same maximal consistent ILW-consistent subset of Φ. Serious duplication of worlds is necessary already in the case of IL. (See de Jongh-Veltman [2] or Japaridze-de Jongh [3] for more explanation on this point.)

To overcome this second problem we need some more machinery.

Definition 8 Let Γ and Δ be maximal consistent subsets of Φ and let C^{∈} Φ.

(a) Δ is a C-critical successor of Γ iff (i) Γ ≺ Δ,

(ii) ¬B, □¬B^{∈} Δ for each B such that B ⊳ C^{∈} Γ.

(b) C admits B with respect to Γ iff B occurs in some C-critical successor of Γ.

It is easily seen that successors of C-critical successors of Γ are C-critical successors of Γ.

In the model that we are going to build every world w is associated with a maximal ILW-consistent subset Γ of some adequate Φ. This set Γ is supposed to give a partial description of w. To ensure that a formula of the form ¬(B ⊳ C)^{∈} Γ is indeed true in w, the model has to provide a world w′ associated with a C-critical successor of Γ containing B. Moreover, all the worlds accessible from w′ by the relation S_{w} should be associated with C-critical successors, too.

Is this feasible? The next two lemmata say it is.

Lemma 9 Let Γ be maximal ILW-consistent in Φ, and suppose (B ⊳ C)^{∈} Φ. Then ¬(B ⊳ C)^{∈} Γ iff C admits B with respect to Γ.

Proof. From right to left: this follows almost immediately from the definition. ¿From left to right: the proof of lemma 3.6 in de Jongh-Veltman [2] (or lemma 13.12 of Japaridze-de Jongh [3]) applies to ILW. ⊣

Lemma 10 Let Γ be maximal ILW-consistent in Φ and suppose (A ⊳ D)^{∈} Γ. If C admits A with respect to Γ, then C admits D, too.

Proof. Almost directly from the previous lemma. ⊣

The lemmata just mentioned enable us to construct an IL-countermodel to A for every A such that ⊬_{ILW} A. They allow us to connect a so-called C-critical cone above w with every world w introduced in the model and with every C such that some ¬(B ⊳ C) should be true in w. The worlds in this C-critical cone are all associated with a C-critical successor of the set of formulas associated with w. By duplicating we get non-overlapping cones for different C’s. In doing so we can ensure that the S_{w} relation will never ‘exit from’ a given C-critical cone.

However, for the completeness of ILW we don’t need an IL-countermodel, we need an ILW-countermodel. The third and most difficult problem we have to deal with is in the extra condition that ILW imposes on the models: R ∘ S_{w} is to be conversely well-founded.

In the following definition, we isolate a special kind of critical successors. Unfortunately, at this point it is rather difficult to explain what makes them so special.

Definition 11 Let Γ be a maximal ILW-consistent subset of Φ and suppsose E^{∈} Φ.

The set Δ is an E-critical solution for C_{i} with respect to B_{1} ⊳ C_{1}, …, B_{n} ⊳ C_{n} iff Δ is an E-critical successor of Γ such that C_{i} and □¬B_{1}, ..., □¬B_{n} all occur together in Δ.

The following lemma, which strengthens Lemma 10 above, will help us to construct the S_{w}-relation on a given E-critical cone in a step-by-step construction. We say that a maximal consistent set Δ blocks a set of formulas Ψ if Δ contains ¬B for all B in Ψ.

Lemma 12 Let Γ be a maximal consistent subset of Φ and E^{∈} Φ. Suppose B_{1} ⊳ C_{1}, …, B_{n} ⊳ C_{n} are ⊳-formulae in Γ such that E admits each B_{i}.

There is a non-empty subset X of {1, …, n} such that, for each i^{∈} X, there exists an E-critical solution for C_{i} with regard to B_{1} ⊳ C_{1}, …, B_{n} ⊳ C_{n} which blocks {B_{j} | j^{∈} {1, …, n}\X}. Proof. Suppose no such subset X of {1, …, n} exists. Then, in the first place, the whole set {1, …, n} does not function as an X with the required properties: There exists i such that no E-critical solution for C_{i} with regard to B_{1} ⊳ C_{1}, …, B_{n} ⊳ C_{n} can be found. Without loss of generality we may assume that i = n.

Formally this means that there are A_{1}, …, A_{m} with □A_{1}, …, □A_{m}^{∈} Γ and F_{1}, …, F_{k} with F_{1} ⊳ E, …, F_{k} ⊳ E^{∈} Γ such that,

A_{1}, …, A_{m}, □A_{1}, …, □A_{m}, ¬F_{1}, …, ¬F_{k}, □¬F_{1}, …, □¬F_{k} ⊢

C_{n} → ♢B_{1} ∨ … ∨ ♢B_{n}.

In other words,

A_{1}, …, A_{m}, □A_{1}, …, □A_{m} ⊢

C_{n} → ♢(B_{1} ∨ … ∨ B_{n}) ∨ (F_{1} ∨ … ∨ F_{k}) ∨ ♢(F_{1} ∨ … ∨ F_{k}),

which gives

□A_{1}, …, □A_{m} ⊢

□(C_{n} → ♢(B_{1} ∨ … ∨ B_{n}) ∨ (F_{1} ∨ … ∨ F_{k}) ∨ ♢(F_{1} ∨ … ∨ F_{k})).

This means that:

□A_{1}, …, □A_{m} ⊢ C_{n} ⊳ ♢(B_{1} ∨ … ∨ B_{n}) ∨ (F_{1} ∨ … ∨ F_{k}) ∨ ♢(F_{1} ∨ … ∨ F_{k}).

In view of (J5) this can be simplified to

□A_{1}, …, □A_{m} ⊢ C_{n} ⊳ ♢(B_{1} ∨ … ∨ B_{n}) ∨ (F_{1} ∨ … ∨ F_{k}).

Since B_{n} ⊳ C_{n}^{∈} Γ, we see, by applying several axioms, that:

Γ ⊢ B_{n} ⊳ ♢(B_{1} ∨ … ∨ B_{n}) ∨ (F_{1} ∨ … ∨ F_{k}).

At this point the axiom W plays its crucial role; we obtain:

Γ ⊢ B_{n} ⊳ (♢(B_{1} ∨ … ∨ B_{n}) ∨ (F_{1} ∨ … ∨ F_{k})) ∧ ¬□B_{n}, which simplifies to

Γ ⊢ B_{n} ⊳ ♢(B_{1} ∨ … ∨ B_{n−1}) ∨ (F_{1} ∨ … ∨ F_{k}). Since each F_{i} ⊳ E is a member of Γ this leads, by some applications of (J3) and (J2), to:

Γ ⊢ B_{n} ⊳ ♢(B_{1} ∨ … ∨ B_{n−1}) ∨ E. (*) This concludes our use of the assumption that the whole set {1, …, n} is not an X with the required properties.

Next, in the second place, the set {1, …, n − 1} does not function as such an X. There exists i, say n − 1, such that no E-critical solution for C_{i} with regard to B_{1} ⊳ C_{1}, …, B_{n} ⊳ C_{n} blocking {B_{n}} exists. This means that there are A_{1}, …, A_{m} with □A_{1}, …, □A_{m}^{∈} Γ and F_{1}, …, F_{k} with F_{1} ⊳ E, …, F_{k} ⊳ E^{∈} Γ, such that

A_{1}, …, A_{m}, □A_{1}, …, □A_{m}, ¬F_{1}, …, ¬F_{k}, □¬F_{1}, …, □¬F_{k} ⊢

C_{n−1} → ♢(B_{1} ∨ … ∨ B_{n−1} ∨ B_{n}) ∨ B_{n}. Reasoning as before gives

Γ ⊢ B_{n−1} ⊳ ♢(B_{1} ∨ … ∨ B_{n−1}) ∨ (♢B_{n} ∨ B_{n}) ∨ E, and hence, applying (*):

Γ ⊢ B_{n−1} ⊳ ♢(B_{1} ∨ … ∨ B_{n−1}) ∨ E, and thus, by W,

Γ ⊢ B_{n−1} ⊳ ♢(B_{1} ∨ … ∨ B_{n−2}) ∨ E. Continuing like this, in stage p we have

Γ ⊢ B_{n−p + 1} ⊳ ♢(B_{1} ∨ … ∨ B_{n−p}) ∨ E. Now suppose the set {1, …, n − p} does not function as such an X: There exists i, say n − p, such that there are A_{1}, …, A_{m} with □A_{1}, …, □A_{m}^{∈} Γ and F_{1}, …, F_{k} with F_{1} ⊳ E, …, F_{k} ⊳ E^{∈} Γ, such that

A_{1}, …, A_{m}, □A_{1}, …, □A_{m}, ¬F_{1}, …, ¬F_{k}, □¬F_{1}, …, □¬F_{k} ⊢

C_{n−p} → ♢(B_{1} ∨ … ∨ B_{n}) ∨ B_{n−p+1} ∨ … ∨ B_{n} or in other words,

A_{1}, …, A_{m}, □A_{1}, …, □A_{m}, ¬F_{1}, …, ¬F_{k}, □¬F_{1}, …, □¬F_{k} ⊢

C_{n−p} → ♢(B_{1} ∨ … ∨ B_{n−p}) ∨ (♢B_{n−p+1} ∨ B_{n−p+1}) ∨ … ∨ (♢B_{n} ∨ B_{n}) Reasoning as before and applying the results reached for B_{n}, …, B_{n−p + 1}, we find

Γ ⊢ B_{n−p} ⊳ ♢(B_{1} ∨ … ∨ B_{n−p−1}) ∨ E.

Continuing like this, we finally get, in the n-th stage,

Γ ⊢ B_{1} ⊳ E,

but this is a contradiction, since B_{1} ⊳ E cannot be a member of Γ. ⊣

Theorem 13 (Completeness and decidability of ILW). If ⊬_{ILW} A, then there is a finite ILW-model ⟨W, R, S, ^{||−}⟩ such that w^{|̸|−}A for some w^{∈} W. Proof. We show that, for abitrary Φ, Γ with Φ adequate and Γ maximal consistent in Φ, there is a model with root w_{0} such that, for all ϕ^{∈} Φ, w_{0}^{||−}ϕ iff ϕ^{∈} Γ. Then for completeness it is sufficient to take some finite adequate set Φ containing ¬A and let Γ be a maximal consistent subset of Φ containing ¬A.

Every world in the model will be a sequence of pairs ⟨⟨Δ_{1}, σ_{1}⟩, …, ⟨Δ_{k}, σ_{k}⟩⟩. In this sequence each Δ_{i} is a maximal consistent subset of Φ and each σ_{i} is either empty or a pair consisting of a formula in Φ and a number j (1 ≤ j ≤ n), where n is the number of ⊳-formulas in Φ. If w is such a world, Δ_{k} will be the set of the formulas true in the world, and so we will write Δ(w) for Δ_{k}. The sequence that codes the world encrypts the sequence of all its predecessors as its initial segments. The formula E, if any, in σ_{k} signals that w is in the E-critical cone of its immediate predecessor w′. The natural number accompanying E is used to fix the S_{w′}-relation inside this E-critical cone.

More precisely, the set of worlds W of the model is given by the following inductive definition.

(i) w_{0} = ⟨⟨Γ, ∅⟩⟩^{∈} W,

(ii) If τ ∗ ⟨Δ, σ⟩^{∈} W, the following procedure is applied for each E that occurs as a consequent in some ⊳-formula in Φ. Taking the set Y = {B_{1} ⊳ C_{1}, …, B_{n} ⊳ C_{n}} of all ⊳-formulas in Δ with antecedents admitted by E as our starting point, we repeatedly apply lemma 12 with respect to Δ and E in Φ. Eventually we obtain a sequence X_{1}, …, X_{m} (obtained in that order) of disjoint subsets of Y the union of which is Y.

The set X_{1} is the outcome of applying lemma 12 to Δ, E and Y. Choose for each j^{∈} X_{1} an E-critical solution Δ_{j} for C_{j} with respect to Y blocking {B_{j} | j^{∈} Y \X_{1}}. Then extend W with τ ∗ ⟨Δ, σ⟩ ∗ ⟨Δ_{j}, ⟨E, 1⟩⟩.

In a similar manner X_{i+1} is determined: X_{i+1} is the set obtained by applying lemma 12 to Y \(X_{1} ∪ … ∪ X_{i}). Choose for each j^{∈} X_{i+1} an E-critical solution Δ_{j} for C_{j} with respect to Y \(X_{1} ∪ … ∪ X_{i}) containing ¬B_{m} for all m^{∈} Y \(X_{1} ∪ … ∪ X_{i+1}). Then extend W with τ ∗ ⟨Δ, σ⟩ ∗ ⟨Δ_{j}, ⟨E, i + 1⟩⟩.

W is finite for the usual reasons: each newly constructed world ‘contains’ more □-formulas than its immediate predecessor.

Define R and S_{w} on W as follows:

(i) w R w′ iff w is a proper initial segment of w′.

(ii) u S_{w}v iff u = w ∗ ⟨Δ, ⟨E, i⟩⟩ ∗ σ and v = w ∗ ⟨Δ′, ⟨E, j⟩⟩ ∗ τ and (either j < i, or j = i and σ is empty), or u = v or u R v.

Note that {u | u = w ∗ ⟨Δ, ⟨E, i⟩⟩ ∗ σ for some Δ, i, σ} plays the role of the E-critical cone above w. For each i, we call the set {u | u = w ∗ ⟨Δ, ⟨E, i⟩⟩ ∗ σ} the i-th section of this cone.

Given its definition, it is obvious that R is transitive and conversely wellfounded. Likewise, S_{w} is easily seen to be reflexive and transitive. For the converse well-foundedness of R ∘ S_{w} it is sufficient to note that, if u R ∘ S_{w} v, then, either u R v or v’s ‘index’ (i.e. the number accompanying the last element of v) is lower than the index of u.

Finally, it remains to prove that for all B^{∈} Φ, w^{∈} W_{Γ}, w^{||−}B iff B^{∈} Δ(w). The induction is trivial except for the two ⊳-cases.

First assume ¬(C ⊳ D)^{∈} Δ(w). This is easy: D admits C, so some Dcritical successor with C in it exists, because C will occur as C_{i} in one of the X_{j}’s, and its D-critical solution will be produced in the D-critical cone above w. By the definition above the S_{w}-relation does not exit from the D-critical cone.

Next assume C ⊳ D^{∈} Δ(w). We have to show that, if C occurs in the Ecritical cone above w, then so does D in such a way that the occurrence of D can be reached from the occurrence of C by S_{w}. Since C ⊳ D^{∈} Δ(w), C ⊳ D is one of the B_{i} ⊳ C_{i} in Y. This number i is an element of X_{j} for some j while an E-critical solution for C_{i} is produced as the formula set of a world v in the j-th section of the E critical cone above w, in fact as one of the R-minimal elements of that section. For all k ≤ j, □¬B_{i} is present in the R-minimal elements of the k-sections of the E-critical cone above w. This is so because ‘before’ X_{j}, B_{i} ⊳ C_{i} is each time a member of the set of formulas under discussion. This implies that, in these k-sections, B_{i} does not occur in the nonminimal elements. Moreover, for k < j, B_{i} does not occur among the minimal elements of the ksection either. Therefore, if B_{i} occurs in the E-critical cone at all, it will be either in a world u belonging to a k-section with k > j, or in a world u that is a minimal element of the j-section. In both cases u S_{w} v holds, so C ⊳ D is forced in w. ⊣

References

[1] A. Berarducci, The Interpretability Logic of Peano Arithmetic, Journal of Symbolic Logic, 56, 1059-1089, 1990.

[2] D.H.J. De Jongh and F. Veltman, Provability Logics for Relative Interpretability, in: Petkov ed., Mathematical Logic, Proceedings of the Heyting 1988 Summer School in Varna, Bulgaria, pp. 31-42, Plenum Press, Boston, 1990.

[3] G. Japaridze and D.H.J. De Jongh, The Logic of Provability , in: S.R. Buss ed., Handbook of Proof Theory, pp. 476–546, Elsevier Science, Amsterdam, 1998.

[4] C. Smoryński, Self-Reference and Modal Logic, Springer Verlag, 1985.

[5] J. Joosten, The interpretability logic of all reasonable artithmetic theories, master’s thesis, ILLC, University of Amsterdam, 1998.

[6] A. Visser, Interpretability Logic, in: Petkov, ed., Mathematical Logic, Proceedings of the Heyting 1988 Summer School in Varna, Bulgaria, pp. 175-209, Plenum Press, Boston, 1990.

[7] A. Visser, An overview of interpretability logic, in: M. Kracht, M. de Rijke and H. Wansing, eds., Advances in modal logic ’96, pp. 307-359, CSLI Publications, Stanford, CA, 1997.