Propositional Dynamic Logic has interpolation

Tomasz Kowalski JAIST-Hokuriku, 1–1 Asahidai, Tatsunokuchi, 923-1292 Ishikawa,

                       email: kowalski@jaist.ac.jp

9 January 2000

1 Prelude

Propositional Dynamic Logic (PDL) is the logic corresponding in a natural way to the variety D of dynamic algebras. Consult e.g., [5] for details on dynamic algebras. Precisely speaking, the correspondence holds between D and the so-called test-free PDL, but since it is proved in [2] that test-free PDL has interpolation iff full PDL does, we will systematically disregard the distinction between them. It is also conjectured in [2] that PDL indeed has interpolation.

2 Dynamic algebras

A dynamic algebra is an algebra A = ⟨A; ∨, ∧, ¬, 0, 1, π(π ∈ Π)⟩, such that:

1. ⟨A; ∨, ∧, ¬, 0, 1⟩ is a boolean algebra;

2. Π is the universe of the absolutely free algebra Π = ⟨Π; ∘, ∪, ∗⟩, of the type ⟨2, 2, 1⟩, countably generated by the set Ξ = {ξ_{n} : n ∈ ω}.

3. A satisfies:

(i) π0 = 0, (ii) π(x ∨ y) = πx ∨ πy, (iii) (π ∪ σ)x = πx ∨ σx, (iv) (πσ)x = π(σx),

(v) x ∨ ππ^{∗}x ≤ π^{∗}x ≤ x ∨ π^{∗}(¬x ∧ πx). An algebra A, of the type of dynamic algebras, is called ∗-continuous iff π^{∗}x = ⋁{π^{n} : n ∈ ω}, for all

π ∈ Π, with π^{n}x defined inductively by: π^{0}x = x, π^{n+1}x = ππ^{n}x. All ∗-continuous algebras are dynamic algebras. A class K of dynamic algebras is ∗-continuous iff if all its members are. Fact 1 All finite dynamic algebras are ∗-continuous. If a class K is ∗-continuous, then so is SP (K).

Recall, that an algebra is called residually finite iff it is a subdirect product of finite algebras. Fact 2 ([5] Theorem 5.4.) Free dynamic algebras are residually finite. Lemma 1 Free dynamic algebras are ∗-continuous.

3 Amalgamation and interpolation

A triple ⟨A_{0}, A_{1}, A_{2}⟩ of similar algebras, is called a V-formation iff there are embeddings i_{1} : A_{0} ⟶ A_{1} and i_{2} : A_{0} ⟶ A_{2}. In other words, in a V-formation, A_{1} and A_{2} share an isomorphic copy of A_{0} as a subalgebra. Thus, dealing with V-formations we will always tacitly assume i_{1} and i_{2} to be identity maps.

A V-formation ⟨A_{0}, A_{1}, A_{2}⟩, with A_{i} ∈ K, for i = 0, 1, 2 and K a class of similar algebras, can be amalgamated in K iff there is an algebra B ∈ K and embeddings e_{1} : A_{1} ⟶ B, e_{2} : A_{2} ⟶ B, such that e_{1} ∘ i_{1} = e_{2} ∘ i_{2} (or, by our convention, e_{1}|_{A_{0}} = e_{2}|_{A_{0}}).

A class K of similar algebras has the amalgamation property (AP) iff every V-formation from K can be amalgamated in K.

Assume that the universes of algebras in K are partially ordered. Then K is said to have the superamalgamation property (SupAP) iff for any V-formation ⟨A_{0}, A_{1}, A_{2}⟩, there is a B that amalgamates it, with the embeddings f_{1} : A_{1} ⟶ B and f_{2} : A_{2} ⟶ B, such that we have: for any x ∈ A_{k} and y ∈ A_{j}, if f_{k}(x) ≤ f_{j}(y), then there is a z ∈ A_{0} with x ≤ i_{k}(z), i_{j}(z) ≤ y, where {k, j} = {1, 2} (or, again, by our convention, simply x ≤ z, z ≤ y).

Clearly, SupAP is stronger than AP; thus, by obvious extensions of the definitions above we will speak of V-formations that superamalgamate, or of superamalgams of certain V-formations.

A (propositional) logic Λ, with a certain reasonable implication →, possesses Craig interpolation property iff for any formulas ϕ, ψ in the appropriate language, the following holds:

(†) if ⊢_{Λ} ϕ → ψ, then there is a formula χ, whose variables are a subset of those that ϕ and ψ have in common, and such that ⊢_{Λ} ϕ → χ and ⊢_{Λ} χ → ψ.

The next, crucial, proposition follows easily from Madarász’s generalisation of Maximova’s celebrated theorem (see [3] and [4]), and the folklore about dynamic algebras recalled above. Let F_{K}(Z) stand for the K-free algebra generated by Z. We say that free algebras from K superamalgamate iff every V-formation ⟨F_{K}(X ∩ Y), F_{K}(X), F_{K}(Y)⟩ (which implicitly assumes the existence of all the algebras involved) can be superamalgamated in the variety V(K). If the above holds for finite X and Y, we say that free finitely generated algebras from K superamalgamate.

Proposition 1 For the variety D of dynamic algebras the following are equivalent:

(i) D has SupAP,

(ii) free finitely generated algebras from D superamalgamate,

(iii) Λ(D) has Craig interpolation.

4 Boolean interlude

We will need two constructions well-known in the theory of boolean algebras (BAs). For lack of space we will not recall any definitions, instead, we refer the reader to [1]. The first construction is that of minimal completion.

Fact 3 For any BA A there is a unique complete BA C, such that A ⊆ C and C preserves all joins that exist in A.

The unique complete algebra C above is called the minimal completion of A. Let A ⊆ B be BAs, and C, D their respective minimal completions. We have:

Lemma 2 If B preserves all joins that exist in A, then the embedding i : A ⟶ B extends in a natural way to a complete embedding e : C ⟶ D.

Let F(X), F(Y) be BAs freely generated by X and Y, with Y ⊆ X and |Y | ≤ |X| = ω.

Lemma 3 The identity embedding i : F(Y) ⟶ F(X) preserves all joins that exist in F(Y).

Let ⟨B_{0}, B_{1}, B_{2}⟩ be a V-formation of BAs. The amalgamated free product B of B_{1}, B_{2} over B_{0} satisfies the following characterisation lemma (dual of [2] Corollary 11.22).

Fact 4 B is the amalgamated free product of B_{1}, B_{2} over B_{0}, with the embeddings e_{1}, e_{2} iff e_{1}(B_{1}) ∪ e_{2}(B_{2}) generates B and for any two elements b_{1} ∈ B_{1}, b_{2} ∈ B_{2} with e_{1}(b_{1}) ∨ e_{2}(b_{2}) = 1, there is a c ∈ B_{0} such that b_{1} ≥ ¬c and b_{2} ≥ c.

Under certain completeness assumptions amalgamated free products behave extremely well (cf.[1] Lemma 12.16).

Fact 5 If the algebras B_{0}, B_{1}, B_{2}, and the identity embeddings are all complete, then the amalgamated free product B of ⟨B_{0}, B_{1}, B_{2}⟩ preserves all joins from B_{i} (i = 1, 2).

5 Finale

First we extend the notion of minimal completion to dynamic algebras. Recall that, by Lemma 1, free dynamic algebras are ∗-continuous.

Lemma 4 Fact 3 and Lemma 2 remain valid for ∗-continuous algebras. Lemma 3 holds also for free dynamic algebras.

Then, take the V-formation ⟨F(X ∩ Y), F(X), F(Y)⟩. As D has constants, the free algebras involved always exist. Clearly, the boolean reducts of the algebras above also constitute a V-formation.

Since F(X ∩ Y), F(X), and F(Y) are all ∗-continuous, it follows by the lemma above that there are unique complete ∗-continuous algebras G_{X∩Y}, G_{X}, and G_{Y} with F(Z) ⊆ G_{Z}, for Z ∈ {X, Y, X ∩ Y } such that G_{Z} preserves all joins existing in F(Z). It also follows that for Z ∈ {X, Y }, G_{Z} preserves all joins existing in F(X ∩ Y). Consider the V-formation ⟨G_{X∩Y} , G_{X}, G_{Y} ⟩.

Fact 6 The identity embeddings in ⟨G_{X∩Y} , G_{X}, G_{Y} ⟩ are complete.

Let G be the amalgamated free product of the boolean reducts of G_{X} and G_{Y} over G_{X∩Y}. Let C be the minimal completion of G (as a BA).

Fact 7 C can be expanded to a ∗-continuous algebra D, with D = C. Moreover, D is a superamalgam of ⟨F(X ∩ Y), F(X), F(Y)⟩.

Corollary 1 Free finitely generated algebras from D superamalgamate.

By Proposition 1, we obtain:

Theorem 1 The variety D of dynamic algebras has SupAP. Full propositional dynamic logic has Craig interpolation property.

References

[1] S. Koppelberg, Handbook of Boolean Algebras. Volume 1 (edited by J.D. Monk with R. Bonnet), North Holland, 1989.

[2] M. Kracht, Tools and Techniques in Modal Logic, Elsevier Studies in Logic No. 142, 1999.

[3] J.X. Madarász, Interpolation and Amalgamation; Pushing the Limits. Part I, Studia Logica 61 (1998), 311–345. Part II, Studia Logica 62 (1999), 1–19.

[4] L.L. Maksimova, Interpolation theorems in modal logics and amalgamable varieties of topological boolean algebras, Algebra and Logic 18 (1979), 348–370

[5] V. Pratt, Dynamic Algebras: Examples, Constructions, Applications, Studia Logica 50 (1991), 571–601.