Two Axiomatizations of Nelson Algebras

• Autorzy: Adam Grabowski
• Języki publikacji: EN

Abstrakty

EN

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

Słowa kluczowe

EN

quasi-pseudo-Boolean algebras; Nelson lattices; de Morgan lattices

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2015
• Tom: 23
• Numer: 2
• Strony: 115-125

Daty

wydano

2015-06-01

otrzymano

2015-04-19

online

2015-08-13

Twórcy

autor

Adam Grabowski

• Institute of Informatics University of Białystok Ciołkowskiego 1M, 15-245 Białystok Poland

Bibliografia

• [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.
• [2] Diana Brignole. Equational characterization of Nelson algebra. Notre Dame Journal of Formal Logic, (3):285-297, 1969.
• [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.
• [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.
• [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.
• [10] Adam Grabowski. Mechanizing complemented lattices within Mizar system. Journal of Automated Reasoning, 2015. doi:10.1007/s10817-015-9333-5.
• [11] Adam Grabowski. Robbins algebras vs. Boolean algebras. Formalized Mathematics, 9(4): 681-690, 2001.
• [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.
• [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.
• [15] Helena Rasiowa. Algebraic Models of Logics. Warsaw University, 2001.
• [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.

Identyfikatory

DOI

10.1515/forma-2015-0012