Abstract
Bi-intuitionistic logic is the result of adding the dual of intuitionistic implication to intuitionistic logic. In this note, we characterize the expressive power of this logic by showing that the first order formulas equivalent to translations of bi-intuitionistic propositional formulas are exactly those preserved under bi-intuitionistic directed bisimulations. The proof technique is originally due to Lindström and, in contrast to the most common proofs of this kind of result, it does not use the machinery of neither saturated models nor elementary chains.
Similar content being viewed by others
References
Blackburn P., de Rijke M., Venema Y.: Modal Logic. Cambridge University Press, Cambridge (2001)
Flum J., First-order logic and its extensions. In Proceedings of the International Summer Institute and Logic Colloquium, Kiel 1974, Springer-Verlag, New York, 1975, pp. 248-310.
Hodges W.: Model Theory. Cambridge University Press, Cambridge (1993)
Goré R., Postniece L.: Combining derivations and refutations for cut-free completeness in Bi-intuitionistic logic. Journal of Logic and Computation 20(1), 233–260 (2010)
Kurtonina N., de Rijke M.: Simulating without negation. Journal of Logic and Computation 7(4), 501–522 (1997)
Lindström P.: On extensions of elementary logic. Theoria 35, 1–11 (1969)
Marker D.: Model Theory: An Introduction. Springer, Berlin (2002)
Restall G.: An Introduction to Substructural Logics. Routledge, London (2000)
Restall, G., Extending intuitionistic logic with subtraction, URL: http://consequently.org/writing/, 1997.
Rauszer C.: A formalization of the propositional calculus in H-B logic. Studia Logica 33, 23–34 (1974)
Rauszer C.: Model theory for an extension of intuitionistic logic. Studia Logica 36, 73–87 (1977)
Rauszer C.: Applications of Kripke models to Heyting–Brouwer logic. Studia Logica 36(1/2), 61–71 (1977)
Olkhovikov G. K.: Model-theoretic characterization of intuitionistic propositional formulas. The Review of Symbolic Logic 6(2), 348–365 (2013)
Wansing H.: Constructive negation, implication, and co-implication. Journal of Applied Non-Classical Logics 18(2–3), 341–364 (2008)
Wolter F.: On logics with coimplication. Journal of Philosophical Logic 27(4), 353–387 (1998)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Badia, G. Bi-Simulating in Bi-Intuitionistic Logic. Stud Logica 104, 1037–1050 (2016). https://doi.org/10.1007/s11225-016-9664-1
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-016-9664-1