Bisimulation and Propositional Intuitionistic Logic

Anna Patterson

Computer Science Department, Stanford University Stanford CA 94305, Email annap@cs.stanford.edu

Abstract. The Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic suggests that p ⊃ q can be interpreted as a computation that given a proof of p constructs a proof of q. Dually, we show that every finite canonical model of q contains a finite canonical model of p. If q and p are interderivable, their canonical models contain each other. Using this insight, we are able to characterize validity in a Kripke structure in terms of bisimilarity.

Theorem 1 Let K be a finite Kripke structure for propositional intuitionistic logic, then two worlds in K are bisimilar if and only if they satisfy the same set of formulas.

This theorem lifts to structures in the following manner.

Theorem 2 Two finite Kripke structures K and K′ are bisimilar if and only if they have the same set of valid formulas.

We then generalize these results to a variety of infinite structures; finite principal filter structures and saturated structures.

1 Background

The standard model theory for intuitionistic logic (Heyting 1966) was introduced by Kripke (1965). This model theory was originally introduced as a characterization of modal logics (Kripke 1963). A natural question that arises for any model theory is characterizing when two models satisfy the same set of formulas. A partial answer to this for modal logics was given by van Benthem, who showed that for well behaved modal structures the notion of bisimulation was appropriate.

We now apply the same techniques to intuitionistic logic. Although intuitionistic logic is not a traditional modal logic we can use the relationship between S4 and topology to provide a bridge.

The algebra of S4 (Lewis and Langford 1932) is a topological Boolean algebra (McKinsey and Tarski 1944) where the modality □ can be taken to be an interior operation and the modality ◇ is taken to be a closure operation (McKinsey 1941, Rasiowa and Sikorski 1963). It is well known (Birkhoff 1948) that the open subsets of a topological Boolean algebra form a relatively pseudocomplemented lattice. However, a relatively pseudo-complemented lattice with a bottom is a pseudo-complemented lattice, that is a Heyting algebra and hence an algebra of intuitionistic logic.

We prove that finite Kripke structures for intuitionistic logic are bisimilar exactly when they entail the same set of intuitionistic formulas. This means that two transitive monotonic modal models are bisimilar if and only if their associated finitely axiomatizable sets of valid intuitionistic formulas are equal. This can be interpreted as saying that all functions between open sets, the □- formulas, are definable in intuitionistic logic (McKinsey and Tarski 1946). Since functions between open sets are continuous and all operators in intuitionistic logic are computable, this result is perhaps better known in computer science as: continuous functions are computable (Scott 1972).

2 Intuitionistic Logic

We present a model theory for intuitionistic logic due to Kripke. For a nice overview of this model theory see Fitting (1969).

Definition 1. A Kripke structure for propositional intuitionistic logic over a set P of propositional atoms is a triple ⟨W, R, V ⟩ where W is a non-empty set (the set of worlds), R is a binary reflexive and transitive relation on W and V is a function assigning to every world a set of propositional atoms from P where the assignment V satisfies, for every world w, wRw′ → V (w) ⊆ V (w′).

Thus, V is monotonic on propositional atoms.

Definition 2. The satisfaction relation ⊧_{K} on a Kripke structure K = ⟨W, R, V ⟩ over a set of propositional atoms P is a relation between worlds and propositional formulas. We define this relation inductively over the structure of a formula. Thus, for any w ∈ W,

w ⊧_{K} p  ≡  p ∈ V (w)
w ⊧_{K} φ ∧ ψ ≡  w ⊧_{K} φ and w ⊧_{K} ψ
w ⊧_{K} φ ∨ ψ ≡  w ⊧_{K} φ or w ⊧_{K} ψ
w ⊧_{K} φ ⊃ ψ ≡ ∀w′ ∈ W such that w R w′, w′ ⊧_{K} φ implies w′ ⊧_{K} ψ
w ⊧_{K} ∼ φ ≡  ∀w′ ∈ W such that w R w′, w′ |̸=_{K} φ

Lemma 3. Monotonicity Let K = ⟨W, R, V ⟩ be a Kripke model. We have for all w ∈ W, and for all formula φ, if w ⊧_{K} φ, and wRw′, then w′ ⊧_{K} φ.

Therefore, the satisfaction relation is monotonic for arbitrary formulas.

Definition 4. Let K = ⟨W, R, V ⟩ be a Kripke structure, then a formula φ is satisfied in K if and only if ∃w ∈ W. w ⊧_{K} φ. A formula φ is valid in K if and only if ∀w ∈ W. w ⊧_{K} φ. A formula φ is valid if and only if φ is valid in all Kripke structures.

A formula φ is refuted at a world, w, in K if and only if w |̸=_{K} φ. A formula φ is refuted in K if and only if ∃w ∈ W. w |̸=_{K} φ.

Definition 5. – A set of formulas Θ is a propositional intuitionistic theory if

it is closed under the intuitionistic inference rules.

– A theory Θ is consistent if Θ does not include a contradiction.

– A set of formulas Θ has the disjunction property if φ ∨ ψ ∈ Θ implies φ ∈ Θ or ψ ∈ Θ.

– The theory of a world w in a Kripke structure is the set of formulas satisfied at w in K, i.e. T h(w) = {φ | w ⊧_{K} φ}.

– Two worlds w, w′ are theory equivalent, denoted w ≈ w′, if T h(w) = T h(w′).

– The theory of a structure K is the set of formulas valid in K.

We say that a Kripke structure is finite if the cardinality of W is finite. Studying finite Kripke structures is not particularly restrictive because it is well known that an intuitionistic formula is valid if and only if it is valid in all finite Kripke structures.

Theorem 6. Let K = ⟨W, R, V ⟩ be a finite Kripke structure over P and let Θ be a consistent intuitionistic theory satisfying the disjunction property whose propositional atoms are in P. Let w be a world in W.

T h(w) ⊆ Θ if and only if ∃w′ ∈ W such that (wRw′ and T h(w′) = Θ).

Proof. The direction from right to left is a restatement of monotonicity (Lemma 3).

Now from left to right, we need a world above w with exactly the theory Θ.

1. We are going to define a formula γ as the conjunction of some subset of Θ which in K implies every other formula in Θ. Let W_{<} be the set of worlds in K that do not satisfy all of Θ. For each world w_{<} in W_{<}, pick some formula ϕ_{w_{<}} in Θ such that w_{<} |̸=_{K} ϕ_{w_{<}}. As W_{<} is finite, we can define γ as the finite conjunction ⋀_{w_{<}∈W_{<}} ϕ_{w_{<}}. In K, by construction, every world which satisfies γ satisfies Θ. The theory Θ contains γ, hence w |̸=_{K}∼ γ. Otherwise ∼ γ would be in Θ contrary to the consistency of Θ. Therefore there is a world accessible from w that satisfies all of Θ.

2. We are going to define a formula δ as the disjunction of some subset of the complement of Θ and use the formula γ ⊃ δ to force the satisfaction of only the formulas in Θ. Let W_{>} be the set of worlds in K that satisfy a formula not in Θ. For each world w_{>} in W_{>}, pick some formula ψ_{w_{>}} which is not in Θ such that w_{>} ⊧_{K} ψ_{w_{>}}. As W_{>} is finite, let δ be the finite disjunction ⋁_{w_{>}∈W_{>}} ψ_{w_{>}}. In K, by construction, in every world where δ is refuted, only formulas in Θ could be satisfied. Now we have w |̸=_{K} γ ⊃ δ. Otherwise the formula γ ⊃ δ would be in Θ. Since Θ is a theory satisfying the disjunction property, we would have δ and one ψ_{w_{>}} in Θ — contrary to the construction. Therefore there is a world accessible from w that satisfies γ and refutes δ. This means that there is a world w′ accessible from w which satisfies exactly Θ.

By a simplification of the above proof we obtain the following theorem.

Theorem 7. Let K = ⟨W, R, V ⟩ be a finite Kripke structure over P and let Θ be a consistent intuitionistic theory satisfying the disjunction property whose propositional atoms are in P.

T h(K) ⊆ Θ if and only if ∃w ∈ W such that T h(w) = Θ.

Definition 8. A Kripke structure K is a canonical model for a theory Θ if every formula in Θ is valid in K and every formula not in Θ is refuted in K.

Definition 9. Let K = ⟨W, R, V ⟩ be a Kripke structure, and let w be an element of W, then K ↑ w is the structure, ⟨↑ (w), R^{\}_{↑(w)}, V ^{\}_{↑(w)}⟩, where the principal filter of w is ↑ (w) = {w′ | wRw′}.

This is simply the restriction of K to the worlds above w. Technically we should prove that K ↑ w is a Kripke structure, but this is immediate. Likewise, for any X ⊆ W, we can construct a sub-Kripke structure K ↑ X from the upwards closed elements generated from X, ↑ (X) = ⋃_{w∈X} ↑ (w).

Theorem 10. If K is a finite canonical model for a theory Φ and Φ is included in some consistent theory Θ and Φ and Θ have the same set of propositional atoms, then a finite canonical model for Θ is a sub-structure of K.

Proof. Let Δ = {Ψ | Ψ a consistent theory extending Θ satisfying the disjunction property}. By Theorem 7, for all theories Ψ in Δ, there exists a world w_{Ψ} in K satisfying exactly Ψ. Let X be the union of such worlds i.e. X = ⋃_{Ψ∈Δ} w_{Ψ}, then K ↑ X is the required sub-structure.

3 Bisimulation within a structure

Bisimulation was introduced by Milner (1980) as a way of defining an equivalence notion for a process algebra. There bisimulation characterized equivalences between labeled transition systems. Earlier, van Benthem showed the close connection between bisimulation (or more precisely p-morphisms) and definability in modal logics (1976). Using the classical transformation of modal formulas to first order formulas, he showed that a first order formula is preserved under bisimulation exactly when it is equivalent to the translation of a modal formula. Bisimulation has been used in a variety of other ways; Aczel (1988) for instance showed that bisimulation provided a natural identity condition for non-well-founded sets.

Bisimulation is usually defined over labeled transition systems. In structures for intuitionistic logic, we do not really have labels on transitions. Therefore, we consider labeled transition systems with just one label; in addition, the states of these labeled transition systems are decorated with the set of propositional atoms “true” at that world.

The following is the definition of bisimulation in such a structure.

Definition 11. Let K = ⟨W, R, V ⟩ be a Kripke structure, then we say that two worlds w, w′ ∈ W are bisimilar, denoted w \underline{↔} w′, in K if there exists a relation B ⊆ W × W (a bisimulation) such that

wBw′  and
xBy ⇒ V (x) = V (y)  and
xBy ⇒ ∀x′. (x R x′ → ∃y′. y R y′ and x′ B y′) and
xBy ⇒ ∀y′. (y R y′ → ∃x′. x R x′ and x′ B y′)

Note that bisimilarity is the largest such bisimulation relation. The set of equivalence classes under \underline{↔} is denoted W/ \underline{↔} and the equivalence class of w is denoted [w].

We can make a smaller structure using this equivalence relation on worlds.

Definition 12. Let K = ⟨W, R, V ⟩ be a Kripke structure, then K/\underline{↔} = ⟨W/\underline{↔} , R/\underline{↔} , V/\underline{↔} ⟩ is a Kripke structure where V/\underline{↔} ([w]) = V (w) and

[w]R/\underline{↔} [w′] ≡ ∃w_{1} ∈ [w], ∃w′_{1} ∈ [w′] such that w_{1} R w′_{1}.

Technically, we have to show that K/\underline{↔} is a Kripke structure. To this end one should notice that V/\underline{↔} is monotonic with respect to propositional atoms.

3.1 Bisimulation and Finite Kripke Models

The following theorem states that bisimulation is truth preserving and does not strengthen the structure to prove any extra formulas. This is a result also found in modal logics (Benthem 1976). The forward direction of this theorem for intuitionistic logic appears as a lemma in Rodenburg’s thesis (1986). The backward direction is an easy exercise in structural induction.

Theorem 13. Let K = ⟨W, R, V ⟩ be a Kripke structure, then ∀w ∈ W,

w ⊧_{K} α if and only if [w] ⊧_{K/\underline{↔}} α.

Next we show that if two worlds in a finite Kripke structure are theory equivalent, then they are bisimilar. This result also holds for modal logics (Benthem 1976).

Theorem 14. Let K = ⟨W, R, V ⟩ be a finite Kripke structure, then ∀w_{1}, w_{2} ∈ W. w_{1} ≈ w_{2} implies that w_{1} \underline{↔} w_{2}.

Proof. It suffices to show that ≈ is a bisimulation. By definition, V (w_{1}) = V (w_{2}). Since ≈ is symmetric, we only need to show one more clause of the bisimulation definition; for all w′_{1} ∈ W such that w_{1} R w′_{1} there is a w′_{2} ∈ W such that w_{2} R w′_{2} and w′_{1} ≈ w′_{2}.

Let Θ be the set of formulas satisfied at w′_{1}. By monotonicity and theory equivalence, Θ is a superset of formulas satisfied at w_{2}. Thus T h(w_{2}) ⊆ T h(w′_{1}) and we apply Theorem 6 to find a w′_{2} such that w′_{2} ≈ w′_{1}.

Corollary 15. Let K = ⟨W, R, V ⟩ be a finite Kripke structure, then for all w, w′ ∈ W.

w \underline{↔} w′ if and only if w ≈ w′

Proof. This follows from Theorems 13 and 14.

3.2 Extending Beyond the Finite

We extend this study beyond finite Kripke structures because we wish to study structures which correspond to intuitionistic theories, not simply structures which correspond to an intuitionistic formula.

We define two extensions and prove theorems that are tailored to intuitionistic Kripke models. There are similarities and differences with the modal case. In the modal case the non-finite Kripke structures where a correspondence between bisimilarity and theory equivalence has been discovered are the image-finite and the saturated Kripke structures. The definitions of those concepts are specific to Kripke models for modal logic. In this section, we examine similar conditions for Kripke models for intuitionistic logic.

Finite Principal Filter Structures Finite principal filter structures are a candidate for an intuitionistic version of image-finite Kripke structures for modal logic. But as we shall see, there are other candidates as well.

Definition 16. Let K = ⟨W, R, V ⟩ be a Kripke structure. K has finite principal filters when ∀w ∈ W the principal filter, ↑ (w), is finite.

Insisting that the set of worlds accessible from any world be a finite set seems like a quite restrictive condition. However, this condition does not imply that the entire structure is finite, for there could exist an infinite set of incomparable worlds. Finite principal filter structures have the advantage over finite structures in that they can describe a canonical model for any intuitionistic theory over a finite number of propositional atoms.

It follows from the work of Riger and Nishimura (1957, 1960) that there are no finite canonical Kripke models for the entire theory of propositional intuitionistic logic even if the cardinality of the set of propositional atoms is only 1. However, there is a canonical Kripke model with the finite principal filter property. In fact, every theory over a finite set of propositional atoms has a model which is a finite principal filter model.

Moreover, for each finite set of propositional atoms (Bellissima 1986) constructed such a model which has the property that no two distinct worlds in this structure are bisimilar. In other words, this structure is the bisimulation class representative as well as the canonical model.

Theorem 17. Let K = ⟨W, R, V ⟩ be a Kripke structure with finite principal filters, then ∀w_{1}, w_{2} ∈ W. w_{1} ≈ w_{2} if and only if that w_{1} \underline{↔} w_{2}.

Proof. From right to left is simply an application of Theorem 13. From left to right, consider the filter generated by {w_{1}, w_{2}}. This equals ↑ (w_{1})∪ ↑ (w_{2}). Since ↑ (w_{1}) is finite and ↑ (w_{2}) is finite, also ↑ (w_{1})∪ ↑ (w_{2}) is finite. We apply Theorem 14 to conclude that w_{1} \underline{↔} w_{2} in K ↑ \{w_{1}, w_{2}\}. However, a bisimulation between w_{1} and w_{2} in K ↑ {w_{1}, w_{2}} is also a bisimulation in K.

Saturation Now we attempt to generalize to saturated structures in the lines of what has been accomplished in the modal setting. See Hollenberg (1994) for an excellent overview and de Rijke (1996) for a collection of papers pertinent to the following generalizations.

We now give a definition which is similar in spirit to m-saturation found in (Hollenberg 1994).

Definition 18. Let K = ⟨W, R, V ⟩ be a Kripke structure, then K is

– weakly conjunctively saturated if for every theory Θ_{s}, if for every finite subset θ_{f} of Θ_{s} there is world in K which satisfies ∧θ_{f} (the conjunction of formulas in θ_{f}), then there is a world in K which satisfies all of Θ_{s}, i.e.

∀Θ_{s}.(∀ finite θ_{f} ⊆ Θ_{s}.∃w.∀θ ∈ θ_{f}.w ⊧_{K} θ) → ∃w′.∀θ ∈ Θ_{s}.w′ ⊧_{K} θ,

– weakly disjunctively saturated if for every set of formulas Θ_{r}, if for every finite subset θ_{f} of Θ_{r} there is world in K which refutes ∨θ_{f} (the disjunction of the formulas in θ_{f}), then there is a world in K which refutes all of Θ_{r}.

∀Θ_{r}.(∀ finite θ_{f} ⊆ Θ_{r}. ∃w.∀θ ∈ θ_{f}.w |̸=_{K} θ) → ∃w′.∀θ ∈ Θ_{r}.w′ |̸=_{K} θ,

– weakly saturated if for every pair of disjoint sets of formulas Θ_{s} and Θ_{r} such that Θ_{s} is a theory, if for every finite subset θ_{s}, θ_{r}, in Θ_{s} and Θ_{r} respectively, there is a world in K which satisfies ∧θ_{s}, and a world in K which refutes ∨θ_{r}, then there is a world in K which satisfies all of Θ_{s} and refutes all of Θ_{r},

∀Θ_{s}.∀Θ_{r}. Θ_{s} ∩ Θ_{r} = ∅  →
[((∀ finite θ_{f} ⊆ Θ_{s}. ∃w.∀θ ∈ θ_{f}.w ⊧_{K} θ)∧
(∀ finite θ_{f} ⊆ Θ_{r}. ∃w.∀θ ∈ θ_{f}.w |̸=_{K} θ))
→  ∃w′.∀θ ∈ Θ_{s}.∀θ′ ∈ Θ_{r}. w′ ⊧_{K} θ and w′ |̸=_{K} θ′].

Definition 19. Let K = ⟨W, R, V ⟩ be a Kripke structure, then K is

– locally conjunctively saturated if for every w ∈ W, K ↑ w is weakly conjunctively saturated,

– locally disjunctively saturated if for every w ∈ W, K ↑ w is weakly disjunctively saturated, and

– locally saturated for every w ∈ W, K ↑ w is weakly saturated.

Definition 20. Let K = ⟨W, R, V ⟩ be a Kripke structure, then K is

– conjunctively saturated if K is weakly conjunctively saturated and locally conjunctively saturated,

– disjunctively saturated if K is weakly disjunctively saturated and locally disjunctively saturated, and

– saturated if K is weakly saturated and locally saturated.

Theorem 21. Let K = ⟨W, R, V ⟩ be a saturated Kripke structure, then ∀w_{1}, w_{2} ∈ W. w_{1} ≈ w_{2} if and only if w_{1} \underline{↔} w_{2}.

Proof. From right to left, we simply use the fact that bisimulation is truth preserving and apply Theorem 13. From left to right assume w_{1}Rw′_{1}. Let Θ = T h(w′_{1}) and Θ_{r} be the complement of Θ. Let Φ = {∧θ_{f} ⊃ ∨φ_{f} | θ_{f} ⊆ Θ where θ_{f} is finite and φ_{f} ⊆ Θ_{r} where φ_{f} is finite}.

All of Φ is refuted at w_{2}, by construction, and for every θ_{f}, w_{2} |̸=_{K}∼ (∧θ_{f}). This means that for every ϕ = (∧θ_{f}) ⊃ (∨φ_{f}) there is a world w′ above w_{2} such that w′ ⊧_{K} ∧θ_{f} and w′ |̸=_{K} ∨φ_{f}.

By conjunctive saturation, there is a world w′_{2} in K ↑ w_{2} which satisfies all of Θ, by disjunctive saturation, there is a world w′_{2} in K ↑ w_{2} which refutes all of Θ_{r}. By saturation, we can use the same world w′_{2} to satisfy Θ and refute Θ_{r}. Therefore, w′_{2} has theory exactly Θ as needed.

We need both clauses in the definition of saturation to generalize this result to bisimulation between structures. In the proof above, K need only be a locally saturated structure.

Lemma 22. Let K be a Kripke structure.

1. If K is locally saturated, it is not necessarily weakly saturated.

2. If K is weakly saturated, it is not necessarily locally saturated.

Proof. Counterexample to 1) Let this structure be denoted K_{1}.

w_{1} = {q_{1}} w_{2} = {q_{2}} … w_{n} = {q_{n}} …

Counterexample to 2) Add to K_{1} a bottom world connected to all worlds w_{i} and call it w_{b}. Also add a world w disconnected from K_{1}. The world which witnesses the saturation of K ↑ w_{b} is not above w_{b}.

K_{1}

⋮

w_{b} = ∅  w = ∅

[figure]

w_{∗} = ∅

When drawing Kripke structures, we show the name of the world and the value of the valuation function V at that world. The arcs represent the accessibility relation where arcs derivable by transitivity or reflexivity are not shown.

4 Comparison with the Modal Case

Our definitions of finite principal filter structures and saturated structures are not their modal counterparts applied to intuitionistic Kripke models. In the modal case, the series of structures,

1. finite,

2. image-finite, and

3. saturated structures

are generalizations of each other in numerical order. Since finite principal filter structures are a candidate for an analogue of image-finite structures we might assume that they are saturated. Here we provide a counterexample.

Lemma 23. 1. Finite principal filter structures are not necessarily saturated.

Proof. K_{1} from Lemma 22 is neither

1. conjunctively saturated, namely for every finite subset of Q = {q_{i} | i ∈ ℕ}, a world in K satisfies the conjunction of intuitionistic negations of each element in that subset, but no world satisfies ⋀_{i} ∼ q_{i} i ∈ ℕ,

2. nor disjunctively saturated, because no world refutes ⋁_{i} q_{i} i ∈ ℕ.

We could rectify the problem with saturation by adding a new world w_{0}.

w_{0} = ∅ w_{1} = {q_{1}} w_{2} = {q_{2}} … w_{n} = {q_{n}} …

There is another counterexample which only uses two propositional atoms.

Lemma 24. Finite principal filter structures over a finite set of propositional atoms are not necessarily saturated.

Proof. We take K_{2} the free Kripke model on two generators {p, q}. It has the theory True. From (Bellissima 1986) we know that this is a finite filter model with an infinite anti-chain given by the w_{i}’s.

Take Θ now to be the theory of intuitionistic logic over two generators (the theory True). Every subset of Θ is satisfied in this structure, and every subset of non-valid formulas is refuted in this structure, but there is no world which is a witness to this fact. For the theory True in K_{2} to be witnessed at a world, we would need to add a point w_{∗}.

K_{2}^{∗} [figure: K_{2}; ⋮; w_{1} w_{2} … w_{n} …; w_{∗} = ∅]

Once we have added that w_{∗}, we cannot stop there. We would need to add a continuum of points; one for every subset of the infinite anti-chain in order to saturate this structure. Saturatedness must hold for all Θ. This means that for arbitrary infinite structures, we cannot always obtain a correspondence between structures which have the same set of valid formulas and bisimilar structures.

4.1 Image Finite Structures?

Another result in modal logics is that bisimilarity and theory equivalence correspond for image finite structures. There are two manners in which we could define image finite structures. When we view Kripke structures as annotated labeled transitions systems with only a single label then, because of transitivity, image finite structures are simply the finite principal filter structures. In the preceding text, we have just studied this form of image finite structure. Another quite reasonable reading of an image finite structure requires an alternate transformation from a Kripke structure to a labeled transition system. This alternate transformation labels transitions between Kripke worlds with the set of propositional atoms that have “just become true”. That is for each pair of worlds w, w′ such that wRw′ let us label the transition with the difference among the propositional atoms.

Definition 25. A Kripke structure, K = ⟨W, R, V ⟩ is image finite when for every world w and for every propositional atom p, the set {w′ | p ∈ V (w′) − V (w) ∧ w′ is an immediate successor of w} is finite.

Using the previous definition, the following serves as a counterexample to the proposed result that two image finite structures with the same theory are bisimilar.

Theorem 26. (Bellissima 1986) If the number of propositional atoms is greater than 1, then every canonical Kripke model has an infinite anti-chain.

Proposition 27. Two image finite structures with the same theory are not necessarily bisimilar.

Proof. Take K_{2}^{∗} (from Lemma 23), as one structure. Let K′ be a variation of the structure K_{2} in which every infinite subset of the antichain has a world representing the infinite meet. These new worlds are above the bottom world w′_{∗} which is the meet of every element of the infinite anti-chain. The worlds w_{∗} and w′_{∗} both have the same theory. However w_{∗} and w′_{∗} are not bisimilar. Hence K′ and K_{2}^{∗} are not bisimilar.

4.2 Modal Saturation

Modal m-saturation (Hollenberg 1994) is most similar to locally saturated because the modal case concerns itself with only pointed modal structures, i.e. structures which contain a world w_{∗} from which all other worlds are accessible. If we insist that the intuitionistic Kripke structures are pointed, then locally saturated is the same as saturated. However, as we saw, some very natural structures like the canonical Kripke model, K_{2}, for propositional intuitionistic logic over two generators are not pointed. K_{2} cannot be made saturated and pointed without adding a continuum of points. Hence structures which are not necessarily pointed arise naturally in intuitionistic logic. Given this, to obtain a correspondence between structures with the same theory and bisimilar structures we need the global view of saturation given in Definition 20.

5 Bisimulation between structures

The definition of bisimulation can be extended slightly to include the equivalence of two worlds from different structures.

Definition 28. Let K = ⟨W, R, V ⟩ and K′ = ⟨W′, R′, V′⟩ be two Kripke structures over P, then K is bisimilar to K′, K \underline{↔} K′, if there is a relation S ⊆ W ×W′ such that

– ∀w ∈ W ∃w′ ∈ W′ such that w S w′, and

– ∀w′ ∈ W′ ∃w ∈ W such that w S w′, and

– x S y implies V (x) = V′(y), and

– x S y implies ∀x′ ∈ W. x R x′ → (∃y′ ∈ W′. y R′ y′ ∧ x′ S y′), and

– x S y implies ∀y′ ∈ W′. y R′ y′ → (∃x′ ∈ W. x R x′ ∧ x′ S y′).

Definition 29. Let K = ⟨W, R, V ⟩, K′ = ⟨W′, R′, V′⟩ be two Kripke structures. K is a logical substructure of K′, written K ⊆ K′, when for any valid formula φ in K, φ is valid in K′.

K and K′ are elementarily equivalent, K ≈ K′, when K ⊆ K′ and K′ ⊆ K.

Lemma 30. Let K and K′ be two finite/finite principal filter/saturated structures.

K is a logical substructure of K′ if and only if K′ is bisimilar to some sub-Kripke structure of K.

That is whenever the theory of K = ⟨W, R, V ⟩ is included in the theory of K′ = ⟨W′, R′, V′⟩, then there exists a U ⊆ W such that K′ is bisimilar to K ↑ U.

Definition 31. Let K = ⟨W, R, V ⟩ and K′ = ⟨W′, R′, V′⟩ be two Kripke structures over P. We say that K is isomorphic to K′, denoted K ≅ K′, if there is a bijection on worlds, f: W → W′, such that

– ∀w, w′ ∈ W. w R w′ if and only if f(w) R′ f(w′), and

– ∀w ∈ W. V (w) = V′(f(w)).

We can make a quotient structure using theory equivalence on worlds where the set of equivalences classes under ≈ is W/ ≈ and apply Lemma 12 to produce K/ ≈. The following is a corollary to Corollary 15/ Theorem 17/Theorem 21.

Corollary 32. Let K = ⟨W, R, V ⟩ be a finite/finite principal filter/saturated Kripke structure, then K/\underline{↔} ≅ K/ ≈.

Lemma 33. Let K = ⟨W, R, V ⟩ and K′ = ⟨W′, R′, V′⟩ be two finite/finite principal filter/ saturated Kripke structures over P, then K and K′ are bisimilar, K \underline{↔} K′, if and only if K/\underline{↔} is isomorphic to K′/\underline{↔}.

Theorem 34. Let K = ⟨W, R, V ⟩ and K′ = ⟨W′, R′, V′⟩ be two finite/finite principal filter/saturated Kripke structures over P, then K and K′ have the same set of valid formulas, K ≈ K′, if and only if K/ ≈ is isomorphic to K′/ ≈.

Corollary 35. Let K = ⟨W, R, V ⟩ and K′ = ⟨W′, R′, V′⟩ be two finite/finite principal filter/saturated Kripke structures over P, then the following are all equivalent,

(1) K ≈ K′ (2) K \underline{↔} K′ (3) K/\underline{↔} ≅ K′/\underline{↔}
(4) K/ ≈ ≅ K′/ ≈ (5) K/ ≈ ≅ K′/\underline{↔}

6 Conclusion

Bisimulation has been examined in conjunction with modal logics starting with van Benthem’s correspondence theory (1976). It has been shown that two finite Kripke structures for modal systems have the same set of valid formulas if and only if the two Kripke structures are bisimilar. Although the forward direction of our correspondence (Theorem 13) can be obtained as a corollary of the corresponding results for modal logic, the backwards direction (Theorem 14) strengthens the traditional modal results.

Goldblatt has also studied validity preserving constructions for modal logics and a survey is found in (Goldblatt 1993). We considered a similar problem for intuitionistic logic. This is non-trivial, as the translations from intuitionistic logic into modal logics (Feferman 1986) are not onto. There is further difficulty because it has been shown that bisimulation is characterized by ◇ and negation and conjunction. However there is no definable intuitionistic connective which corresponds to ◇ nor to classical negation. Therefore we would expect a stronger notion than bisimulation to characterize intuitionistic logic. Two structures could differ on a modal formula but not on any intuitionistic formula.

There is however extra structure in intuitionistic models, namely monotonicity. There are deep connections between monotonicity, computability and intuitionistic logic (McKinsey 1941, McKinsey and Tarski 1946, Birkhoff 1948, Scott 1972). It is this connection that allows the reduct of the models to the monotonic ones to exactly parallel the reduct of the modal logic to intuitionistic logic. Restricting our language to intuitionistic logic and restricting our model to open sets is orthogonal to elementary equivalence and thus bisimulation.

Nonetheless, we have obtained a correspondence between theory equivalence and bisimilarity for finite structures, for finite principal filter structures and for saturated structures.

7 Acknowledgments

The author is deeply indebted to Rob van Glabbeek and Tom Costello for helpful discussions and reading the manuscript. This research also benefited from discussions with Johan van Benthem, Albert Visser, Solomon Feferman and an anonymous referee.

References

Aczel, P. 1988. Non-Well-Founded Sets. Vol. 14 of Lecture Notes. CSLI. Bellissima, F. 1986. Finitely generated free Heyting algebras. Journal of Symbolic Logic 51(1):152–165. Benthem, J. v. 1976. Modal Correspondence theory. PhD thesis, Mathematical Institute, University of Amsterdam. See also Correspondence Theory, Handbook of philosophical logic, Vol. II, Reidel, Dordrecht 1984. Birkhoff, G. 1948. Lattice Theory. Vol. 25. A.M.S. Colloq. Publications. Feferman, S. (Ed.). 1986. Kurt Gödel Collected Works. Oxford, UK: Oxford University Press. Fitting, M. C. 1969. Intuitionistic logic, model theory and forcing. North-Holland. Goldblatt, R. 1993. Mathematics of modality. Vol. 43 of Lecture Notes. CSLI. Heyting, A. 1966. Intuitionism – An Introduction. North-Holland. Hollenberg, M. 1994. Hennessy-Milner classes and process algebra. Technical Report 124, Utrecht Research Institute for Philosophy. Kripke, S. 1963. A semantical analysis of modal logic I: normal modal propositional calculi. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 9:67– 96. Announced in Journal of Symbolic Logic, 24, 1959, p. 323. Kripke, S. A. 1965. Semantical analysis of intuitionistic logic I. In Formal Systems and Recursive Functions, 92–130. Amsterdam: (Proc. 8th Logic Colloq. Oxford 1963) North-Holland. Lewis, C., and C. Langford. 1932. Symbolic Logic. The Century Company. 2nd ed. 1959, Dover Publications, Inc. McKinsey, J. 1941. A solution to the decision problem for the Lewis systems S.2 and S.4 with an application to topology. Journal of Symbolic Logic 6:117–134. McKinsey, J., and A. Tarski. 1944. The algebra of topology. Annals of Mathematics 45:141–191. McKinsey, J., and A. Tarski. 1946. On closed elements in closure algebras. Annals of Mathematics 47:122–162. Milner, R. 1980. A Calculus of Communicating Systems, LNCS 92. Springer-Verlag. Nishimura, I. 1960. On formulas in one variable in intuitionistic propositional calculus. Journal of Symbolic Logic 25:327–331. Rasiowa, H., and R. Sikorski. 1963. The Mathematics of Metamathematics. Vol. 41 of Polska Akademia Nauk. Monografie matematyczne. Warsaw. Ríger, L. 1957. Zamétka o t. naz. svobodnyh algébrah c zamykaniámi. Czechoslovak Mathematical Journal 7(82):16–20. Rijke, M. d. 1996. Modal Logics and Process Algebra. Cambridge University Press and CSLI. Rodenburg, P. 1986. Intuitionistic Correspondence Theory. PhD thesis, University of Amsterdam. Scott, D. 1972. Continuous lattices. In Proc. 1971 Dalhousie Conference: LNM 274, 97–136. Springer-Verlag.