scholarly journals Negation and Implication in Quasi-Nelson Logic

2021 ◽  
Vol 27 (1) ◽  
pp. 107-123
Author(s):  
Thiago Nascimento ◽  
Umberto Rivieccio
Keyword(s):  
Intuitionistic Logic ◽  
Constructive Logic ◽  
Strong Negation ◽  
Completeness Result ◽  
Nelson Algebras ◽  
Nelson Logic

Quasi-Nelson logic is a recently-introduced generalization of Nelson’s constructive logic with strong negation to a non-involutive setting. In the present paper we axiomatize the negation-implication fragment of quasi-Nelson logic (QNI-logic), which constitutes in a sense the algebraizable core of quasi-Nelson logic. We introduce a finite Hilbert-style calculus for QNI-logic, showing completeness and algebraizability with respect to the variety of QNI-algebras. Members of the latter class, also introduced and investigated in a recent paper, are precisely the negation-implication subreducts of quasi-Nelson algebras. Relying on our completeness result, we also show how the negation-implication fragments of intuitionistic logic and Nelson’s constructive logic may both be obtained as schematic extensions of QNI-logic.

scholarly journals Two Axiomatizations of Nelson Algebras

2015 ◽  
Vol 23 (2) ◽  
pp. 115-125
Author(s):  
Adam Grabowski
Keyword(s):  
Rough Sets ◽  
Algebraic Model ◽  
Formal Proof ◽  
Boolean Algebras ◽  
Constructive Logic ◽  
Strong Negation ◽  
Binary Operations ◽  
Nelson Algebra ◽  
P 75 ◽  
Nelson Algebras

Nelson algebras were first studied by Rasiowa and Białynicki- Birula [1] under the name N-lattices or quasi-pseudo-Boolean algebras. Later, in investigations by Monteiro and Brignole [3, 4], and [2] the name “Nelson algebras” was adopted - which is now commonly used to show the correspondence with Nelson’s paper [14] on constructive logic with strong negation. By a Nelson algebra we mean an abstract algebra 〈L, T, -, ¬, →, ⇒, ⊔, ⊓〉 where L is the carrier, − is a quasi-complementation (Rasiowa used the sign ~, but in Mizar “−” should be used to follow the approach described in [12] and [10]), ¬ is a weak pseudo-complementation → is weak relative pseudocomplementation and ⇒ is implicative operation. ⊔ and ⊓ are ordinary lattice binary operations of supremum and infimum. In this article we give the definition and basic properties of these algebras according to [16] and [15]. We start with preliminary section on quasi-Boolean algebras (i.e. de Morgan bounded lattices). Later we give the axioms in the form of Mizar adjectives with names corresponding with those in [15]. As our main result we give two axiomatizations (non-equational and equational) and the full formal proof of their equivalence. The second set of equations is rather long but it shows the logical essence of Nelson lattices. This formalization aims at the construction of algebraic model of rough sets [9] in our future submissions. Section 4 contains all items from Th. 1.2 and 1.3 (and the itemization is given in the text). In the fifth section we provide full formal proof of Th. 2.1 p. 75 [16].

Semi-intuitionistic Logic with Strong Negation

Studia Logica ◽  
2017 ◽  
Vol 106 (2) ◽  
pp. 281-293 ◽  
Author(s):  
Juan Manuel Cornejo ◽  
Ignacio Viglizzo
Keyword(s):  
Intuitionistic Logic ◽  
Strong Negation

Notes on N-lattices and constructive logic with strong negation

Studia Logica ◽  
1977 ◽  
Vol 36 (1-2) ◽  
pp. 109-125 ◽  
Author(s):  
D. Vakarelov
Keyword(s):  
Constructive Logic ◽  
Strong Negation

scholarly journals Co-constructive Logics for Proofs and Refutations

Studia Humana ◽  
2015 ◽  
Vol 3 (4) ◽  
pp. 22-40 ◽  
Author(s):  
James Trafford
Keyword(s):  
Intuitionistic Logic ◽  
Proof Theory ◽  
Direct Proof ◽  
Negative Information ◽  
Constructive Logic ◽  
Logic Of Proofs ◽  
Constructive Logics

Abstract This paper considers logics which are formally dual to intuitionistic logic in order to investigate a co-constructive logic for proofs and refutations. This is philosophically motivated by a set of problems regarding the nature of constructive truth, and its relation to falsity. It is well known both that intuitionism can not deal constructively with negative information, and that defining falsity by means of intuitionistic negation leads, under widely-held assumptions, to a justification of bivalence. For example, we do not want to equate falsity with the non-existence of a proof since this would render a statement such as “pi is transcendental” false prior to 1882. In addition, the intuitionist account of negation as shorthand for the derivation of absurdity is inadequate, particularly outside of purely mathematical contexts. To deal with these issues, I investigate the dual of intuitionistic logic, co-intuitionistic logic, as a logic of refutation, alongside intuitionistic logic of proofs. Direct proof and refutation are dual to each other, and are constructive, whilst there also exist syntactic, weak, negations within both logics. In this respect, the logic of refutation is weakly paraconsistent in the sense that it allows for statements for which, neither they, nor their negation, are refuted. I provide a proof theory for the co-constructive logic, a formal dualizing map between the logics, and a Kripke-style semantics. This is given an intuitive philosophical rendering in a re-interpretation of Kolmogorov's logic of problems.

scholarly journals Quasi-N4-Lattices

2021 ◽  
Author(s):  
Umberto Rivieccio
Keyword(s):  
Paraconsistent Logic ◽  
General Setting ◽  
Extension Property ◽  
Double Negation ◽  
Structure Representation ◽  
Nelson Algebras ◽  
Nelson Logic ◽  
Double Negation Law ◽  
Logical Calculi ◽  
Twist Structure

Abstract Within the Nelson family, two mutually incomparable generalizations of Nelson constructive logic with strong negation have been proposed so far. The first and more well-known, Nelson paraconsistent logic , results from dropping the explosion axiom of Nelson logic; a more recent series of papers considers the logic (dubbed quasi-Nelson logic ) obtained by rejecting the double negation law, which is thus also weaker than intuitionistic logic. The algebraic counterparts of these logical calculi are the varieties of N4-lattices and quasi-Nelson algebras . In the present paper we propose the class of quasi- N4-lattices as a common generalization of both. We show that a number of key results, including the twist-structure representation of N4-lattices and quasi-Nelson algebras, can be uniformly established in this more general setting; our new representation employs twist-structures defined over Brouwerian algebras enriched with a nucleus operator. We further show that quasi-N4-lattices form a variety that is arithmetical, possesses a ternary as well as a quaternary deductive term, and enjoys EDPC and the strong congruence extension property.

Constructive Logic with Strong Negation is a Substructural Logic. I

Studia Logica ◽  
2008 ◽  
Vol 88 (3) ◽  
pp. 325-348 ◽  
Author(s):  
Matthew Spinks ◽  
Robert Veroff
Keyword(s):  
Substructural Logic ◽  
Constructive Logic ◽  
Strong Negation
Sign in / Sign up

Export Citation Format

Share Document