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].
@article{bwmeta1.element.doi-10_1515_forma-2015-0012,
author = {Adam Grabowski},
title = {Two Axiomatizations of Nelson Algebras},
journal = {Formalized Mathematics},
volume = {23},
year = {2015},
pages = {115-125},
zbl = {1318.06010},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2015-0012}
}
Adam Grabowski. Two Axiomatizations of Nelson Algebras. Formalized Mathematics, Tome 23 (2015) pp. 115-125. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2015-0012/
[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. | Zbl 0082.01403
[2] Diana Brignole. Equational characterization of Nelson algebra. Notre Dame Journal of Formal Logic, (3):285-297, 1969. | Zbl 0212.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. | Zbl 0158.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. | Zbl 0158.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. | Zbl 1285.68180
[10] Adam Grabowski. Mechanizing complemented lattices within Mizar system. Journal of Automated Reasoning, 2015. doi:10.1007/s10817-015-9333-5. | Zbl 06585255
[11] Adam Grabowski. Robbins algebras vs. Boolean algebras. Formalized Mathematics, 9(4): 681-690, 2001. | Zbl 0984.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. | Zbl 1108.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. | Zbl 0033.24304
[15] Helena Rasiowa. Algebraic Models of Logics. Warsaw University, 2001. | Zbl 0299.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.