Wansing's bi-intuitionistic logic: semantics, extension and unilateralisation

ABSTRACT

The well-known algebraic semantics and topological semantics for intuitionistic logic ($\mathsf{Int}$) is here extended to Wansing's bi-intuitionistic logic ($\mathsf{2}\mathsf{Int}$). The logic $\mathsf{2}\mathsf{Int}$ is also characterised by a quasi-twist structure semantics, which leads to an alternative topological characterisation of $\mathsf{2}\mathsf{Int}$. Later, notions of Fregean negation and of unilateralisation are proposed. The logic $\mathsf{2}\mathsf{Int}$ is extended with a ‘Fregean negation’ connective $\sim$, obtaining $\mathsf{2}\mathsf{In}{\mathsf{t}}^{\sim }$, and it is showed that the logic $\mathsf{N}{\mathsf{4}}^{\star }$ (an extension of Nelson's paraconsistent logic) results to be the unilateralisation of $\mathsf{2}\mathsf{In}{\mathsf{t}}^{\sim }$ via $\sim$. The logic $\mathsf{2}\mathsf{In}{\mathsf{t}}^{\sim }$ is also characterised by a Kripke-style semantics, a twist structure semantics and a topological semantics.

KEYWORDS:

• Wansing's bi-intuitionistic logic
• algebraic semantics
• topological semantics
• twist structure semantics
• unilateralisation

Acknowledgments

The author is deeply grateful to the anonymous referees for their valuable comments and suggestions which led to important improvements to the article.

Disclosure statement

No potential conflict of interest was reported by the author(s).

Notes

1 Although Trafford (2015) presents co-intuitionistic logic as an alternative presentation and interpretation of Urbas's dual-intuitionistic logic, while the latter is formalised by a single-antecedent multiple-succedent sequent system, which following the usual practice must be interpreted in a verificationist way (i.e. the truth of the single antecedent entails the truth of some succedent), the former is formalised by a multiple-antecedent single-succedent sequent system (the result of interchange antecedents and succedents in dual-intuitionistic logic), and it is interpreted in a falsificationalist way (i.e. the falsity of all the antecedents entails the falsity of the succedent). Trafford's shift in perspective simplifies the formalisation of $\mathsf{CoInt}$ by means of a natural deduction system, which is made in Section 2, a task that presents some technical difficulties for dual-intuitionistic logic (cf. Tranchini, 2012). Moreover, in dual-intuitionistic logic it is impossible to define a connective ⇝ such that $A⇝B$ iff B is deducible from A (cf. Urbas, 1996, Theorem 5.4), which makes it difficult to combine this logic with $\mathsf{Int}$ to obtain a bi-intuitionistic logic, a task that results natural in Trafford's perspective under which $\mathsf{CoInt}$ turns out to be a fragment of Wansing's bi-intuitionistic logic (see Section 2). Therefore, we prefer to differentiate here between ‘dual-intuitionist logic’ and ‘co-intuitionistic logic’, although in some texts these names of logics are considered synonymous (see, for instance, Bellin, 2014).

2 Although in Wansing (2016) only weak completeness for the Kripke-style semantics for $\mathsf{2}\mathsf{Int}$ is proven, the strong completeness of this semantics is proven in Drobyshevich (2019).

3 The interpretation of $(B\prec A{)}^{+}$ differs from the more familiar interpretation of $B\prec A$ in the Kripke-style semantics for Rauszer's bi-intuitionistic logic, where $\hat{v}(w,B\prec A)=1$ iff $\hat{v}(w^{\prime },B)=1$ and $\hat{v}(w^{\prime },A)=0$, for some $w^{\prime }\le w$. This difference is explained in Wansing (2016).

4 It is, of course, also possible to characterise both $\mathsf{Int}$ and $\mathsf{CoInt}$ by means of Brouwerian algebras and use this fact to algebraically characterise $\mathsf{2}\mathsf{Int}$.

5 The relation ${\equiv }_{\mathrm{\Gamma }}$ corresponds to the so-called Frege relation, which is used in a generalisation of the Lindenbaum–Tarski method (cf. Font et al., 2003, Section 2).

6 As pointed out in Negri and von Plato (2001, p. 18), ‘In natural deduction, if two derivations $\mathrm{\Gamma }⊢A$ and $A,\mathrm{\Delta }⊢C$ are given, we can join them together into a derivation $\mathrm{\Gamma },\mathrm{\Delta }⊢C$, through a substitution. The sequent calculus rule corresponding to this is cut.’

7 In Odintsov (2008) and other references, it is not considered an operation ${.-}_{\bowtie }$ in twist structures. Such operation is added here in order to interpret co-implication.

8 If operation ${.-}_{\bowtie }$ is not considered, the definition of twist structure here corresponds with the definition of full twist structure in Odintsov (2008, p. 139), where a twist structure $\mathcal{A}$ is any subalgebra of the full twist structure such that ${\pi }_1\left(\mathcal{A}\right)=\mathcal{H}$. Only complete twist structures are considered in this paper, so the term ‘full’ is not used.

Additional information

Funding

This work was supported by the Universidad de Antioquia, Medellín, Colombia [grant number 2020/36612], and São Paulo Research Foundation (FAPESP), São Paulo, Brazil [grant number 2020/16353-3].