Bisimulation and Propositional Intuitionistic Logic

Anna Patterson

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

Abstract

Brouwer suggests that p ⊃ q can be interpreted as a computation that given a proof of p constructs a proof of q. Dually we can see this as saying that every counter model of q contains a counter model of p. However, what does it mean to contain another Kripke structure? We read this as: every counter model of q contains a substructure that is bisimilar to a counter model of p.

If q and p are interderivable, then the counter models contain each other. Thus we study bisimulation as a way of studying interderivability. Using bisimulation, we are able to characterize validity in a Kripke structure.

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 structures.

1 Background

The standard model theory for intuitionistic logic (Brouwer 1928) was introduced by Kripke (1965). This model theory was originally introduced as a characterization of modal logics. 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 normal 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 pseudo-complemented 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.

Following Gödel we can see intuitionistic logic as a fragment of S4.

We prove that the finite Kripke structures for intuitionistic logic are bisimilar exactly when they entail the same set of intuitionistic formulas. Finally, 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, this result is perhaps better known in computer science as: continuous functions are computable (Scott 1972, Cutland 1980).

2 Intuitionistic Logic

We present a model theory for intuitionistic logic due to Kripke. For a nice overview of this model theory see Fitting (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 where the assignment V satisfies, for every world w, wRw′ → V (w) ⊆ V (w′).

Thus, V is monotonic on propositional atoms.

Definition 2 The satisfiability 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,

\begin{aligned}w ⊧_{K} p & ≡ & p ∈ V (w) \\ w ⊧_{K} φ ∧ ψ & ≡ & w ⊧_{K} φ and w ⊧_{K} ψ \\ w ⊧_{K} φ ∨ ψ & ≡ & w ⊧_{K} φ or w ⊧_{K} ψ \\ w ⊧_{K} φ ⊃ ψ & ≡ & ∀w′ ∈ W. w R w′ ∧ w′ ⊧_{K} φ → w′ ⊧_{K} ψ \\ w ⊧_{K} ∼ φ & ≡ & ∀w′ ∈ W. w R w′ → w′ |̸=_{K} φ \end{aligned}

Definition 3 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.

Definition 4 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 ↑ (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. This definition can be easily generalized to consider a set X ⊆ W of elements to construct a structure K ↑ X from the upward closed elements generated from X, ⋃_{w∈X} ↑ (w). This is called a sub-Kripke structure, denoted K ↑ X ⊆ K.

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 pmorphisms) 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 equivalence over a such a structure.

Definition 5 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′ ∧ x′ B y′)

The set of equivalence classes under \underline{↔} is denoted, W/ \underline{↔} and the equivalence class of w is denoted [w].

A bisimulation henceforth shall refer to the largest such bisimulation relation.

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

Lemma 6 Let K = ⟨W, R, V ⟩ be a structure, then K/ \underline{↔} = ⟨W/ \underline{↔} , R/ \underline{↔} , V/ \underline{↔} ⟩ is a structure where

[w]R/\underline{↔} [w′] ≡ ∃w_{1} ∈ [w], ∃w′_{1} ∈ [w′] such that w_{1} R w′_{1}, and V/ \underline{↔} ([w]) = V (w)

Proof: To show that K/\underline{↔} is a Kripke structure, we need only show that R/\underline{↔} is a reflexive transitive relation and that V/ \underline{↔} is monotonic with respect to propositional atoms. These follow by easy application of the definition of K and \underline{↔}.

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. The forward direction of this theorem appears as a lemma in Rodenberg’s thesis (Rodenberg 1986). The backward direction is an easy exercise in structural induction.

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

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

Now we investigate theory inclusion in a Kripke structure.

Definition 8 Let K = ⟨W, R, V ⟩ be a Kripke structure, then the theory of w_{1} is a subset of w_{2}, denoted w_{1} ⊆ w_{2}, if for all formulas φ, w_{1} ⊧_{K} φ implies w_{2} ⊧_{K} φ.

Definition 9 Let K = ⟨W, R, V ⟩ be a Kripke structure, then w_{1} and w_{2} are elementarily equivalent, denoted w_{1} ≈ w_{2}, if w_{1} ⊆ w_{2} and w_{2} ⊆ w_{1}.

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.

Lemma 10 Let K = ⟨W, R, V ⟩ be a finite Kripke structure.

w_{2} ⊆ w_{1} if and only if ∃w′_{2} ∈ W. such that w_{2}Rw′_{2} and w′_{2} ≈ w_{1}.

Proof: First we show from left to right. Let the theory at w_{1} be Θ. We want to show that there is a world above w_{2} with exactly the theory Θ, given that w_{2} ⊆ w_{1}.

1. We define a formula γ 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, let γ be the finite conjunction ⋀_{w∈W_{<}} ϕ_{w}. In K, by construction, every world which satisfies γ satisfies Θ.

We know that w_{1} ⊧_{K} γ thus w_{2} |̸=_{K}∼ γ. This implies that there is a world w′_{2} accessible from w_{2} that satisfies all of Θ.

2. 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 Θ are satisfied.

We know that w_{1} ⊧_{K} γ but w_{1} |̸=_{K} δ.Thus w_{1} |̸=_{K} γ ⊃ δ. Since w_{2} ⊆ w_{1}, then w_{2} |̸=_{K} γ ⊃ δ. Therefore there is a world accessible from w_{2} that satisfies γ and refutes δ. This means that there is a world accessible from w_{2} which satisfies exactly Θ.

To show that

∃w′_{2} ∈ W. such that w_{2}Rw′_{2} and w′_{2} ≈ w_{1}implies w_{2} ⊆ w_{1}

uses only monotonicity.

This means that if the theory of w_{2} is included in w_{1}, then w_{2} is elementarily equivalent to some world above w_{2}. This holds also between structures, that is whenever w_{2} ⊆ w_{1}, then there is a w′_{2} such that K ↑ w′_{2} ≈ K ↑ w_{1}.

Next we show that if two worlds in a finite Kripke structure are elementarily equivalent, then they are bisimilar.

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

Proof: We want to show that ≈ is a bisimulation. Clearly ≈ is symmetric and since w_{1} ≈ w_{2} then V (w_{1}) = V (w_{2}). Since ≈ is symmetric, we only need to show the last 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, Θ is a superset of formulas satisfied at w_{1}, hence Θ is also a superset of formulas at w_{2}. This means that w_{2} ⊆ w′_{1} as per Definition 8. We apply Lemma 10, to conclude that there is a w′_{2} such that w′_{2} ≈ w′_{1}.

Corollary 12 Let K = ⟨W, R, V ⟩ be a finite Kripke structure.

w_{2} ⊆ w_{1} if and only if ∃w′_{2} ∈ W. such that w_{2}Rw′_{2} and w′_{2} \underline{↔} w_{1}.

This follows from Lemma 10 and Theorem 11.

Corollary 13 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 Theorem 7 and 11

3.2 Extending Beyond the Finite

3.2.1 Finite Principal Filter Structures

We now extend this result to a larger class of structures. We first discuss this class, and then prove a theorem analogous to Corollary 13.

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

Making the set of worlds accessible from any world finite seems like a quite restrictive condition. However, this condition does not imply that the entire structure is finite for there could exist a 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(Bellissima 1986).

Definition 15 A Kripke structure K is a canonical model for propositional intuitionistic logic if every valid propositional intuitionistic formula is valid in K and K refutes every underivable formula.

We call such structures canonical Kripke models.

It follows from the work of Riger and Nishimura (1957, 1960) that there are no finite canonical Kripke models for 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. This means that 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 16 Let K = ⟨W, R, V ⟩ be a Kripke structure with finite principal filters, then w_{1} ≈ w_{2} implies that w_{1} \underline{↔} w_{2}.

Proof: 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 11 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.

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

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

Proof: This follows from Theorem 7 and 16

3.2.2 Finitely Axiomatizable

We now consider another natural class of structures similar to finite principal filter structures. This is a generalization which allows infinite repetitions of elementarily equivalent worlds.

Definition 18 K is wholly finitely axiomatizable whenever ∀w ∈ K, the theory of w is equivalent in K to a finitely axiomatizable theory.

Theorem 19 Let K = ⟨W, R, V ⟩ be a wholly finitely axiomatizable Kripke structure, then w_{1} ≈ w_{2} if and only if w_{1} \underline{↔} w_{2}.

Outline of Proof: From left to right, we simply apply Theorem 7. From right to left we modify the proof of Lemma 10 to get an analogy here. Let w_{1}Rw′_{1}. By monotonicity the theory of w_{1} is included in w′_{1}, hence w_{1} ⊆ w′_{1}. Since w_{1} ≈ w_{2}, then w_{2} ⊆ w′_{1}. Let Θ be the theory at w′_{1}.

We can find the formula γ representing the theory Θ of w′_{1} because every world is finitely axiomatizable.

By monotonicity all worlds above w_{2} include the theory of w_{2}. Since all worlds have finitely axiomatizable theories, this means that there are only finitely many non-elementarily equivalent worlds above w_{2}. Whence we can construct a formula δ from worlds above w_{2} which satisfy some formula not in Θ.

We know that w′_{1} ⊧_{K} γ but w′_{1} |̸=_{K} δ. Thus w_{1} |̸=_{K} γ ⊃ δ. Since w_{2} ≈ w_{1}, we know that w_{2} |̸=_{K} γ ⊃ δ.

This means that there is a world accessible from w_{2} that satisfies γ and refutes δ. Thus there must be a world world accessible from w_{2} which satisfies exactly Θ.

At this point we can apply the same argument as in Theorem 11 to conclude that ≈ is a bisimulation.

3.2.3 Saturation

Now we attempt to generalize more 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.

Conjunctive saturation means that if we satisfy every finite conjunct, then we satisfy the infinite conjunct as well. Disjunctive saturation means that if refute every finite disjunction, we refute the infinite disjunction.

The latter phrase rules out structures such as

q_{1}  q_{2}  … q_{n} …
[figure]
∅

which refutes all finite disjunctions, e.g. ∼∼ q_{1}∨ ∼∼ q_{2}. The infinite disjunct, however, is satisfied because eventually on all branches we have one of the q_{i}’s. When drawing Kripke structures, we label the worlds with the range of the valuation function and draw the arcs which represent the accessibility relation without drawing any of the transitive or reflexive arcs.

We now make a more formal argument.

Definition 20 Let K = ⟨W, R, V ⟩ be a Kripke structure, then K is conjunctively saturated if for every set of formulas Θ_{s}, whenever K satisfies every finite subset of Θ_{s}, then there is a world in K which satisfies all of Θ_{s}.

We say that K is disjunctively saturated if for every set of formula Θ_{r}, whenever K refutes every finite subset of Θ_{r}, then there is a world in K which refutes all of Θ_{r}.

1 We say that a structure is saturated if it is simultaneously ( at the same world w ) conjunctively saturated and disjunctively saturated.

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

Proof: From left to right, we simply apply Theorem 7, from right to left we modify the proof of Lemma 10 to get an analogy here. Let w_{1}Rw′_{1}. By monotonicity the theory of w_{1} is included in w′_{1}, hence w_{1} ⊆ w′_{1}. Since w_{1} ≈ w_{2}, then w_{2} ⊆ w′_{1}. Let Θ be the theory at w′_{1} and for simplicity let us assume (WLOG) that Θ is closed under finite conjunctions. Thus we show

w_{2} ⊆ w′_{1} implies ∃w′_{2} ∈ W. such that w_{2}Rw′_{2} and w′_{2} ≈ w′_{1}.

1. If a formula θ in Θ was not provable at any world accessible from w_{2}, then w_{2} ⊧_{K}∼ θ. Since w_{2} ≈ w_{1} and all of Θ is satisfied at w′_{1} above w_{1}, then w_{2} |̸=_{K}∼ θ. Therefore, every θ ∈ Θ is satisfied at some world above w_{2}. By conjunctive saturation, there is a world above w_{2} which satisfies all of Θ.

1The author would like to thank Albert Visser and Solomon Feferman for discussions and remarks about saturated structures.

2. Let Θ_{r} = {φ such that φ ∉ Θ}, note Θ_{r} is closed under finite disjunctions. The formulas θ ⊃ φ where θ ∈ Θ and φ ∈ Θ_{r} are refuted at w_{1} because w′_{1} refutes them. Since w_{1} ≈ w_{2}, then w_{2} refutes these formulas as well. Therefore there must be a world which refutes Θ_{r} by disjunctive saturation.

By saturation there is a world above w_{2} which both proves Θ and refutes Θ_{r}. This implies that there is a world above w_{2} whose theory is exactly Θ.

At this point we can apply the same argument as in Theorem 11 to conclude that ≈ is a bisimulation.

Before we are feeling to happy that we have all the same results for modal logic, we must note that there is a big difference between these structures. In the modal case, the finite principal filter structures would be saturated. Here however we provide a counterexample.

Lemma 22 Not every finite principal filter structure is saturated.

Outline of Proof: We take K_{2} the free Kripke model on two generators. It has the 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.

K_{2} [figure: w_{1} = ∅  …  w_{n} = ∅  . . . . . .]

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 Θ.

3.2.4 Image Finite Structures?

Another result in modal logics is that bisimulation and elementary 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 23 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 24 If the number of propositional atoms is greater than 1, then every canonical Kripke model has an infinite anti-chain.

Fact 25 Counterexample to: Two image finite structures with the same theory are bisimilar. Take K_{2}^{∗} (from Lemma 22), as one structure. And we define another structure from using the structure K_{2} (also defined in Lemma 22), which we will denote K′.

K′  [figure: K_{2}; ⋮; . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .; . . . . . . . . . . . . . . .; w′_{∗} = ∅]

To define K′, take all infinite subsets of the infinite anti-chain of K_{2} (which exists by Theorem 24) and make a world representing the infinite meet and assign its valuation the empty set. These new worlds are above the bottom world w′_{∗} which is the meet of every element of the infinite antichain. In both of these structures, w_{∗} and w′_{∗} both have the same theory. However w_{∗} and w′_{∗} are not bisimilar. Hence K′ and K_{2}^{∗} are not bisimilar.

4 Bisimulation between structures

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

Definition 26 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′ with w S w′
and ∀w′ ∈ W′. ∃w ∈ W with w S w′ and
x S y ⇒ V (x) = V′(y) and x S y ⇒ ∀x′ ∈ W. x R x′ → ∃y′ ∈ W′. y R′ y′ ∧ x′ S y′
and x S y ⇒ ∀y′ ∈ W′. y R′ y′ → ∃x′ ∈ W. x R x′ ∧ x′ S y′

Definition 27 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′.

Lemma 28 Let K and K′ be two finite/finite principal filter/finitely axiomatizable/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. This provides the needed interpretation promised in the abstract that one theory T is included in another T′, if the model for T′ is bisimilar to a substructure of the model for T. This also has the counter model interpretation that when T ⊆ T′ then every counter model of T′ contain a counter model of T; that is any countermodels of T′ contains a substructure bisimilar to some countermodel of T.

Definition 29 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, call this function 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)).

The following is a corollary to Theorem 13/Theorem 17/ Theorem 19/Theorem 21.

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

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

Outline of Proof: From left to right we are given a symmetric relation from which we construct the bijection in the obvious manner and from right to left we are given a bijection from which we construct the symmetric relation.

Theorem 32 Let K = ⟨W, R, V ⟩ and K′ = ⟨W′, R′, V′⟩ be two finite/finite principal filter/finitely axiomatizable/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 33 Let K = ⟨W, R, V ⟩ and K′ = ⟨W′, R′, V′⟩ be two finite/finite principal filter/finitely axiomatizable/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{↔}

5 Conclusion

Bisimulation has been examined in conjunction with modal logics starting with van Benthem’s correspondence theory (1976). He stated a similar result, 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 7) can be obtained as a corollary of the corresponding results for modal logic, the backwards direction (Theorem 11) strengthens the traditional modal results. Goldblatt has also studied validity preserving constructions for modal logics and a survey is found in (1993).

We considered the same 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 that 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 elementary equivalence and bisimulation equivalence for finite structures, for finite principal filter structures, finitely axiomatizable structures and for saturated structures.

6 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, and Solomon Feferman.

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.

Brouwer, L. 1928. Intuitionistische betrachtungen über den formalismus. Koninklijke Akademie van wetenschappen te Amsterdam, Proceedings of the section of sciences 31:374–379. In From Frege to Gödel, Jean van Heijenoort (editor), Harvard, 1967, pages 490–492.

Cutland, N. 1980. Computability: An introduction to recursive function theory. Cambridge University Press.

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 Publishing Co., Amsterdam-London. Goldblatt, R. 1993. Mathematics of modality. Vol. 43 of Lecture Notes. CSLI. Hollenberg, M. 1994. Hennessy-Milner classes and process algebra. Technical Report 124, Utrecht Research Institute for Philosophy. 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. Rodenberg, 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.