Equality and Apartness in Bi-intuitinistic Logic


Paolo Maffezioli
Luca Tranchini


In the present paper we argue that a symmetric picture of the relationships between equality and apartness can be attained by considering these notions on the background of bi-intuitionistic logic instead of the usual intuitionistic logic. In particular we show that, as the intuitionistic negation of a relation of apartness is an equality, the dualintuitionistic co-negation of an equality is a relation of apartness. At the same time, as the intuitionistic negation of equality is not an apartness, the co-intuitionistic negation of an apartness is not an equality.






Brunner, 2004 – Brunner, A. “First-order anti-intuitionistic logic with apartness”, Logic and Logical Philosophy, 2004, Vol. 13, pp. 77–88.
Crolard, 2001 – Crolard, T. “Subtractive logic”, Theoretical Computer Science, 2001, Vol. 254, pp. 151–185.
van Dalen et al., 1979 – Van Dalen, D. and Statman, R. “Equality in presence of apartness”, in: Essays in Mathematical and Philosophical Logic, ed. by J. Hintikka, I. Niniluoto and E. Saarinen, Dordrecht: Reidel, 1979, pp. 95–116.
Gor´e et al., 2020 – Gor´e, R. and Shillito, I. “Bi-Intuitionistic logics: A new Instance of an old problem”, in: AiML 2020, ed. by N. Olivetti, R. Verbrugge, S. Negri, G. Sandu, London: College Publications, 2020, pp. 269–288.
Kowalski et al. 2017 – Kowalski, T. and Ono, H. “Analytic cut and interpolation for bi-intuitionistic logic”, The Review of Symbolic Logic, 2017, Vol. 10, pp. 259–283.
Negri, 1999 – Negri, S. “Sequent calculus proof theory of intuitionistic apartness and order relations”, Archive for Mathematical Logic, 1999, Vol. 38, pp. 521–547.
Negri et al., 2001 – Negri, S. and von Plato, J. Structural Proof Theory, Cambridge: Cambridge University Press, 2001.
Nelson, 1949 – Nelson, D. “Constructible Falsity”, The Journal of Symbolic Logic, 1949, Vol. 14, pp. 16–26.
von Plato, 2001 – von Plato, J. “Positive Lattices”, in: Reuniting the Antipodes: Constructive and Nonstandard Views of the Continuum, ed. by P. Schuster, U. Berger and H. Osswald, Dordrecht: Springer, 2001, pp. 185–197.
Rauszer, 1980 – Rauszer, C. An algebraic and Kripke-style approach to a certain extension of intuitionistic logic, Warszawa: Instytut Matematyczny Polskiej Akademi Nauk, 1980.
Rauszer, 1974a – Rauszer, C. “A formalization of the propositional calculus of H-B logic”, Studia Logica, 1974, Vol. 33, pp. 23–34.
Rauszer, 1974b – Rauszer, C. “Semi-boolean algebras and their applications to intuitionistic logic with dual operations“, Fundamaenta Mathematicae, 1974, Vol. 83, pp. 219–249.
Tranchini, 2012 – Tranchini, L. “Natural Deduction for Dual-Intuitionistic Logic”, Studia Logica, 2012, Vol. 100, pp. 631–648.
Urbas, 1996 – Urbas, I. “Dual-Intuitionistic Logic”, Notre Dame Journal of Formal Logic, 1996, Vol. 37, pp. 440–451.
Wansing, 2010 – Wansing, H. “Proofs, Disproofs, and Their Duals”, in: AiML 2010, ed. by M. Kracht, M. de Rijke, H. Wansing and M. Zakharyaschev, Stanford: CSLI Publications, 2010, pp. 483–505.
Wansing, 2016 – Wansing, H. “Falsification, natural deduction and bi-intuitionistic logic”, Journal of Logic and Computation, 2016, Vol. 26, pp. 425–450.