# Two Axiomatizations of Nelson Algebras

Formalized Mathematics (2015)

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

## Access Full Article

top## Abstract

top## How to cite

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

@article{AdamGrabowski2015,

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] 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] Diana Brignole. Equational characterization of Nelson algebra. Notre Dame Journal of Formal Logic, (3):285-297, 1969. Zbl0212.31901
- [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] 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] Czesław Bylinski. Binary operations. Formalized Mathematics, 1(1):175-180, 1990.
- [6] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.
- [7] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
- [8] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
- [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] Adam Grabowski. Mechanizing complemented lattices within Mizar system. Journal of Automated Reasoning, 2015. doi:10.1007/s10817-015-9333-5. Zbl06585255
- [11] Adam Grabowski. Robbins algebras vs. Boolean algebras. Formalized Mathematics, 9(4): 681-690, 2001. Zbl0984.06500
- [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] Adam Grabowski and Markus Moschner. Formalization of ortholattices via orthoposets. Formalized Mathematics, 13(1):189-197, 2005.
- [14] David Nelson. Constructible falsity. Journal of Symbolic Logic, 14:16-26, 1949. Zbl0033.24304
- [15] Helena Rasiowa. Algebraic Models of Logics. Warsaw University, 2001. Zbl0299.02069
- [16] Helena Rasiowa. An Algebraic Approach to Non-Classical Logics. North Holland, 1974.
- [17] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
- [18] Stanisław Zukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215-222, 1990.

## Citations in EuDML Documents

top## NotesEmbed ?

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