REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/4876
Tytuł: Two Axiomatizations of Nelson Algebras
Autorzy: Grabowski, Adam
Słowa kluczowe: quasi-pseudo-Boolean algebras
Nelson lattices
de Morgan lattices
Data wydania: 2015
Data dodania: 15-gru-2016
Wydawca: De Gruyter Open
Źródło: Formalized Mathematics, Volume 23, Issue 2, 115–125
Abstrakt: 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].
Afiliacja: Institute of Informatics, University of Białystok, Ciołkowskiego 1M, 15-245 Białystok, Poland
URI: http://hdl.handle.net/11320/4876
DOI: 10.1515/forma-2015-0012
ISSN: 1426-2630
1898-9934
Typ Dokumentu: Article
Występuje w kolekcji(ach):Artykuły naukowe (WMiI)
Formalized Mathematics, 2015, Volume 23, Issue 2

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2015-0012.pdf245,99 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki


Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons