# Two Axiomatizations of Nelson Algebras

Formalized Mathematics (2015)

• Volume: 23, Issue: 2, page 115-125
• ISSN: 1426-2630

top

## Abstract

top
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].

## How to cite

top

Adam Grabowski. "Two Axiomatizations of Nelson Algebras." Formalized Mathematics 23.2 (2015): 115-125. <http://eudml.org/doc/271778>.

abstract = {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].},
author = {Adam Grabowski},
journal = {Formalized Mathematics},
keywords = {quasi-pseudo-Boolean algebras; Nelson lattices; de Morgan lattices; De Morgan lattices; formalization},
language = {eng},
number = {2},
pages = {115-125},
title = {Two Axiomatizations of Nelson Algebras},
url = {http://eudml.org/doc/271778},
volume = {23},
year = {2015},
}

TY - JOUR
AU - Adam Grabowski
TI - Two Axiomatizations of Nelson Algebras
JO - Formalized Mathematics
PY - 2015
VL - 23
IS - 2
SP - 115
EP - 125
AB - 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].
LA - eng
KW - quasi-pseudo-Boolean algebras; Nelson lattices; de Morgan lattices; De Morgan lattices; formalization
UR - http://eudml.org/doc/271778
ER -

## References

top
1. [1] Andrzej Białynicki-Birula and Helena Rasiowa. On the representation of quasi-Boolean algebras. Bulletin de l’Academie Polonaise des Sciences, 5:259-261, 1957. Zbl0082.01403
2. [2] Diana Brignole. Equational characterization of Nelson algebra. Notre Dame Journal of Formal Logic, (3):285-297, 1969. Zbl0212.31901
3. [3] Diana Brignole and Antonio Monteiro. Caracterisation des algèbres de Nelson par des egalités, I. Proceedings of the Japan Academy, 43(4):279-283, 1967. doi:10.3792/pja/1195521624. Zbl0158.00803
4. [4] Diana Brignole and Antonio Monteiro. Caracterisation des algèbres de Nelson par des egalités, II. Proceedings of the Japan Academy, 43(4):284-285, 1967. doi:10.3792/pja/1195521625. Zbl0158.00803
5. [5] Czesław Bylinski. Binary operations. Formalized Mathematics, 1(1):175-180, 1990.
6. [6] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.
7. [7] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
8. [8] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
9. [9] Adam Grabowski. Automated discovery of properties of rough sets. Fundamenta Informaticae, 128:65-79, 2013. doi:10.3233/FI-2013-933. Zbl1285.68180
10. [10] Adam Grabowski. Mechanizing complemented lattices within Mizar system. Journal of Automated Reasoning, 2015. doi:10.1007/s10817-015-9333-5. Zbl06585255
11. [11] Adam Grabowski. Robbins algebras vs. Boolean algebras. Formalized Mathematics, 9(4): 681-690, 2001. Zbl0984.06500
12. [12] Adam Grabowski and Markus Moschner. Managing heterogeneous theories within a mathematical knowledge repository. In Andrea Asperti, Grzegorz Bancerek, and Andrzej Trybulec, editors, Mathematical Knowledge Management Proceedings, volume 3119 of Lecture Notes in Computer Science, pages 116-129. Springer, 2004. doi:10.1007/978-3-540-27818-4 9. 3rd International Conference on Mathematical Knowledge Management, Bialowieza, Poland, Sep. 19-21, 2004. Zbl1108.68589
13. [13] Adam Grabowski and Markus Moschner. Formalization of ortholattices via orthoposets. Formalized Mathematics, 13(1):189-197, 2005.
14. [14] David Nelson. Constructible falsity. Journal of Symbolic Logic, 14:16-26, 1949. Zbl0033.24304
15. [15] Helena Rasiowa. Algebraic Models of Logics. Warsaw University, 2001. Zbl0299.02069
16. [16] Helena Rasiowa. An Algebraic Approach to Non-Classical Logics. North Holland, 1974.
17. [17] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
18. [18] Stanisław Zukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215-222, 1990.

top

## NotesEmbed?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.