Bisimulation and propositional intuitionistic logic

8Citations
Citations of this article
2Readers
Mendeley users who have this article in their library.
Get full text

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.

Cite

CITATION STYLE

APA

Patterson, A. (1997). Bisimulation and propositional intuitionistic logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1243, pp. 348–360). Springer Verlag. https://doi.org/10.1007/3-540-63141-0_24

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free