Bisimulation and propositional intuitionistic logic

Abstract

The Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic suggests that p D 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 1 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.