Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden.
powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden.
powered by
Abstract
Nelson’s constructive logic with strong negation \(\mathbf {N3}\) can be presented (to within definitional equivalence) as the axiomatic extension \(\mathbf {NInFL}_{ew}\) of the involutive full Lambek calculus with exchange and weakening by the Nelson axiom
The algebraic counterpart of \(\mathbf {NInFL}_{ew}\) is the recently introduced class of Nelson residuated lattices. These are commutative integral bounded residuated lattices \(\langle A; \wedge , \vee , *, \Rightarrow , 0, 1 \rangle \) that: (i) are compatibly involutive in the sense that \(\mathop {\sim }\mathop {\sim }a = a\) for all \(a \in A\), where \(\mathop {\sim }a := a \Rightarrow 0\), and (ii) satisfy the Nelson identity, namely the algebraic analogue of (Nelson\(_{\vdash }\)), viz.
The present paper focuses on the role played by the Nelson identity in the context of compatibly involutive commutative integral bounded residuated lattices. We present several characterisations of the identity (Nelson) in this setting, which variously permit us to comprehend its model-theoretic content from order-theoretic, syntactic, and congruence-theoretic perspectives. Notably, we show that a compatibly involutive commutative integral bounded residuated lattice \(\mathbf {A}\) is a Nelson residuated lattice iff for all \(a, b \in A\), the congruence condition
$$\begin{aligned} \varTheta ^{\mathbf {A}}(0, a) = \varTheta ^{\mathbf {A}}(0, b) \quad \text {and} \quad \varTheta ^{\mathbf {A}}(1, a) = \varTheta ^{\mathbf {A}}(1, b) \quad \text {implies} \quad a = b \end{aligned}$$
holds. This observation, together with others of the main results, opens the door to studying the characteristic property of Nelson residuated lattices (and hence Nelson’s constructive logic with strong negation) from a purely abstract perspective.
Implicative lattices, also called Brouwerian lattices or generalised Heyting algebras in the literature, are precisely the 0-free subreducts of Heyting algebras \(\langle A; \wedge , \vee , \rightarrow , 0,1 \rangle \).
We avoid using \(\wedge , \vee , \rightarrow , \Rightarrow \), etc., as logical symbols of the first-order language with equality \(\varLambda [{{\,\mathrm{{\textsc {fol}}}\,}}, \approx ]\), as determined by the algebraic language type \(\varLambda \), since these symbols are employed extensively to denote connective symbols of the algebraic language types considered throughout the paper.
Implicative semilattices, also called Brouwerian semilattices in the literature, are precisely the \(\langle \rightarrow , \wedge \rangle \)-subreducts of Heyting algebras \(\langle A; \wedge , \vee , \rightarrow , 0, 1 \rangle \).
In many texts, compatibly involutive commutative (integral) residuated lattices are simply referred to as involutive commutative (integral) residuated lattices. Here we follow the terminological conventions of Hsieh and Raftery (2007); note that in our previous work (Nascimento et al. 2018a, b) (and likewise in the earlier paper Galatos and Raftery 2004 of Galatos and Raftery) compatibly involutive commutative (integral) residuated lattices are called involutive commutative (integral) residuated lattices.
Numerous sequent calculi for constructive logic with strong negation have been proposed in the literature, including the systems of Almukdad and Nelson (1984), Gurevich (1977), Kutschera (1969), López-Escobar (1972), Thomason (1969), and Zaslavsky (1978). The sequent calculus of Metcalfe (2009) is distinguished among these systems in that—unlike any of the other calculi cited above—it does not contain rules acting on more than one connective at a time. See Kozak (2014, Footnote 3).
The topological study of Nelson algebras can be traced back at least to Cignoli (1986); Sendlewski (1990). For \(\mathbf {N4}\)-lattices, a topological duality was first introduced in Odintsov (2010); see also Jansana and Rivieccio (2014). We notice in passing that the special filters of the first kind used in the duality of Odintsov (2010) coincide, within Nelson algebras, with our filters as defined in Sect. 2
