:: Two Axiomatizations of {N}elson Algebras
:: by Adam Grabowski
::
:: Received April 19, 2015
:: Copyright (c) 2015-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies LATTICES, BINOP_1, XBOOLE_0, EQREL_1, XBOOLEAN, XXREAL_0,
REALSET1, SUBSET_1, STRUCT_0, XXREAL_2, FUNCT_1, ARYTM_3, ARYTM_1,
ROBBINS1, NELSON_1, PBOOLE, ZFMISC_1, OPOSET_1;
notations TARSKI, XBOOLE_0, LATTICES, SUBSET_1, BINOP_1, FUNCT_2, STRUCT_0,
ROBBINS1, ROBBINS3;
constructors BINOP_1, ROBBINS3;
registrations STRUCT_0, LATTICES, LATTICE2, ROBBINS1, ROBBINS3, XBOOLE_0,
ZFMISC_1, LATTAD_1;
requirements SUBSET, BOOLE;
begin :: De Morgan Algebras
definition let L be non empty OrthoLattStr;
attr L is DeMorgan means
:: NELSON_1:def 1
for x, y being Element of L holds
(x "/\" y)` = x` "\/" y`;
end;
registration
cluster de_Morgan involutive -> DeMorgan for non empty OrthoLattStr;
cluster DeMorgan involutive -> de_Morgan for non empty OrthoLattStr;
end;
registration
cluster trivial -> DeMorgan for non empty OrthoLattStr;
end;
registration
cluster DeMorgan involutive bounded distributive Lattice-like for
non empty OrthoLattStr;
end;
definition
mode DeMorgan_Algebra is DeMorgan involutive
distributive Lattice-like non empty OrthoLattStr;
end;
definition
mode Quasi-Boolean_Algebra is bounded DeMorgan_Algebra;
end;
reserve L for Quasi-Boolean_Algebra,
x, y, z for Element of L;
theorem :: NELSON_1:1
(x "\/" y)` = x` "/\" y`;
theorem :: NELSON_1:2
(Top L)` = Bottom L;
theorem :: NELSON_1:3
(Bottom L)` = Top L;
theorem :: NELSON_1:4
x "/\" (x "/\" y) = x "/\" y;
theorem :: NELSON_1:5
x "\/" (x "\/" y) = x "\/" y;
begin :: The Structure and Operators in Nelson Algebras
definition
struct (OrthoLattStr) NelsonStr
(# carrier -> set,
unity -> Element of the carrier,
Compl, Nnegation -> UnOp of the carrier,
Iimpl, impl, L_join, L_meet -> BinOp of the carrier #);
end;
registration
cluster strict non empty for NelsonStr;
end;
registration
cluster trivial DeMorgan involutive bounded distributive Lattice-like for
non empty NelsonStr;
end;
definition let L be non empty NelsonStr,
a, b be Element of L;
func a => b -> Element of L equals
:: NELSON_1:def 2
(the Iimpl of L).(a,b);
end;
definition let L be non empty NelsonStr,
a, b be Element of L;
pred a < b means
:: NELSON_1:def 3
a => b = Top L;
end;
:: Lattice-like ordering
definition let L be non empty NelsonStr,
a, b be Element of L;
pred a <= b means
:: NELSON_1:def 4
a = a "/\" b;
end;
:: Strong negation operator
definition let L be non empty NelsonStr,
a be Element of L;
func ! a -> Element of L equals
:: NELSON_1:def 5
(the Nnegation of L).a;
end;
:: Strong implication
definition let L be non empty NelsonStr,
a, b be Element of L;
func a =-> b -> Element of L equals
:: NELSON_1:def 6
(the impl of L).(a,b);
end;
begin :: The Non-Equational Axiomatization of Nelson Algebras
::NdR _A1, _A2 : quasi_ordering on A
definition let L be non empty NelsonStr;
attr L is satisfying_A1 means
:: NELSON_1:def 7
for a being Element of L holds
a < a;
attr L is satisfying_A1b means
:: NELSON_1:def 8
for a, b, c being Element of L holds
a < b & b < c implies a < c;
end;
definition let L be bounded Lattice-like non empty NelsonStr;
attr L is satisfying_A2 means
:: NELSON_1:def 9
L is DeMorgan involutive distributive;
end;
registration
cluster satisfying_A2 -> DeMorgan involutive distributive
for bounded Lattice-like non empty NelsonStr;
cluster DeMorgan involutive distributive -> satisfying_A2
for bounded Lattice-like non empty NelsonStr;
end;
:: Axioms of N-algebras (according to Rasiowa)
:: These lattices are called Nelson algebras now, but Rasiowa used the name
:: either N-lattices or quasi-pseudo-boolean algebras.
definition let L be non empty NelsonStr;
attr L is satisfying_N3 means
:: NELSON_1:def 10
for x, a, b being Element of L holds
a "/\" x < b iff x < (a => b);
attr L is satisfying_N4 means
:: NELSON_1:def 11
for a, b being Element of L holds
a =-> b = (a => b) "/\" ((-b) => -a);
attr L is satisfying_N5 means
:: NELSON_1:def 12
for a, b being Element of L holds
a =-> b = Top L iff a "/\" b = a;
attr L is satisfying_N6 means
:: NELSON_1:def 13
for a, b, c being Element of L holds
a < c & b < c implies a "\/" b < c;
attr L is satisfying_N7 means
:: NELSON_1:def 14
for a, b, c being Element of L holds
a < b & a < c implies a < b "/\" c;
attr L is satisfying_N8 means
:: NELSON_1:def 15
for a, b being Element of L holds
(a "/\" -b) < -(a => b);
attr L is satisfying_N9 means
:: NELSON_1:def 16
for a, b being Element of L holds
-(a => b) < (a "/\" -b);
attr L is satisfying_N10 means
:: NELSON_1:def 17
for a being Element of L holds
a < -!a;
attr L is satisfying_N11 means
:: NELSON_1:def 18
for a being Element of L holds
-!a < a;
attr L is satisfying_N12 means
:: NELSON_1:def 19
for a, b being Element of L holds
a "/\" -a < b;
attr L is satisfying_N13 means
:: NELSON_1:def 20
for a being Element of L holds
! a = a => - Top L;
end;
registration
cluster satisfying_A1 satisfying_A1b satisfying_A2 satisfying_N3
satisfying_N4 satisfying_N5 satisfying_N6 satisfying_N7
satisfying_N8 satisfying_N9 satisfying_N10 satisfying_N11 satisfying_N12
satisfying_N13 for bounded Lattice-like non empty NelsonStr;
end;
definition
mode Nelson_Algebra is satisfying_A1 satisfying_A1b
satisfying_A2 satisfying_N3
satisfying_N4 satisfying_N5 satisfying_N6 satisfying_N7
satisfying_N8 satisfying_N9 satisfying_N10 satisfying_N11 satisfying_N12
satisfying_N13 bounded Lattice-like non empty NelsonStr;
end;
definition let L be satisfying_N4 bounded non empty NelsonStr,
a, b be Element of L;
redefine func a =-> b equals
:: NELSON_1:def 21
(a => b) "/\" ((-b) => -a);
end;
reserve L for Nelson_Algebra,
a, b, c, d, x, y, z for Element of L;
theorem :: NELSON_1:6
a [= b iff a <= b;
theorem :: NELSON_1:7
a <= b & b <= a iff a = b;
theorem :: NELSON_1:8
a "/\" b = Top L iff a = Top L & b = Top L;
::NdR RasiowaNonClassical: p 69 1.1 (2) <=> (4)
theorem :: NELSON_1:9 :: (2.1) (2.3 <=> 2.5)
a <= b iff a < b & -b < -a;
theorem :: NELSON_1:10
a "/\" b < a;
theorem :: NELSON_1:11
a < a "\/" b;
::NdR RasiowaNonClassical: p 69 1.1 (2) <=> (3)
theorem :: NELSON_1:12 :: (2.1) (2.3 <=> 2.4)
a <= b iff a =-> b = Top L;
::NdR RasiowaNonClassical: p 70 (38)
theorem :: NELSON_1:13
-(a "/\" b) = (-a) "\/" (-b);
theorem :: NELSON_1:14
(a "/\" -a) "/\" (b "\/" -b) = a "/\" -a;
theorem :: NELSON_1:15
a <= b & b <= c implies a <= c;
theorem :: NELSON_1:16
b <= c implies a "\/" b <= a "\/" c & a "/\" b <= a "/\" c;
theorem :: NELSON_1:17
(-a) "\/" b <= a => b;
theorem :: NELSON_1:18
(a => b) "/\" ((-a) "\/" b) = (-a) "\/" b;
theorem :: NELSON_1:19
(-a) "\/" b < a => b;
theorem :: NELSON_1:20
a "/\" (a => b) = a "/\" ((-a) "\/" b);
theorem :: NELSON_1:21
-x < -y implies -(z => x) < -(z => y);
theorem :: NELSON_1:22
x < y implies a "/\" (a => x) < y;
theorem :: NELSON_1:23
x < y implies a => x < a => y;
theorem :: NELSON_1:24
a => (b "/\" c) = (a => b) "/\" (a => c);
begin :: Properties of Nelson Algebras
:: Proven properties from Rasiowa's "Algebraic Models of Logic"
:: Items 2.3, 2.4, p. 92
:: The same set of properties, but with different numbers is also
:: in Rasiowa's "An Algebraic Appproach to Non-Classical Logic"
::NdR RasiowaNonClassical: p 69 1.2 (5)
theorem :: NELSON_1:25 :: (2.7)
a =-> a = Top L;
::NdR RasiowaNonClassical: p 69 1.2 (6)
theorem :: NELSON_1:26 :: (2.8)
a =-> b = Top L & b =-> c = Top L implies a =-> c = Top L;
::NdR RasiowaNonClassical: p 69 1.2 (7)
theorem :: NELSON_1:27 :: (2.9)
a =-> b = Top L & b =-> a = Top L implies a = b;
::NdR RasiowaNonClassical: p 69 1.2 (8)
theorem :: NELSON_1:28 :: (2.10)
a =-> Top L = Top L;
::NdR RasiowaNonClassical: p 69 1.3 (9)
theorem :: NELSON_1:29 :: (2.11)
a => a = Top L;
::NdR RasiowaNonClassical: p 69 1.3 (10)
theorem :: NELSON_1:30 :: (2.12)
(a => b) = (Top L) & (b => c) = (Top L) implies (a => c) = (Top L);
::NdR RasiowaNonClassical: p 69 1.3 (11)
theorem :: NELSON_1:31 :: (2.13)
b < c implies a "\/" b < a "\/" c & a "/\" b < a "/\" c;
::NdR p 69 1.3 (12)
theorem :: NELSON_1:32 :: (2.14)
a < b & c < d implies a "\/" c < b "\/" d & a "/\" c < b "/\" d;
::NdR RasiowaNonClassical: p 69 1.3 (13)
theorem :: NELSON_1:33 :: (2.15)
a "/\" (a => b) < b;
::NdR RasiowaNonClassical: p 69 1.3 (14)
theorem :: NELSON_1:34 :: (2.16)
a => (b => c) = (a "/\" b) => c;
::NdR RasiowaNonClassical: p 69 1.3 (15)
theorem :: NELSON_1:35 :: (2.17)
a => (b => c) = b => (a => c);
::NdR RasiowaNonClassical: p 69 1.3 (16)
theorem :: NELSON_1:36 :: (2.18)
a < ((a => b) => b);
::NdR RasiowaNonClassical: p 71 PROOF (50)
theorem :: NELSON_1:37 :: (2.19)
a < b => (a "/\" b);
::NdR RasiowaNonClassical: p 69 (18)
theorem :: NELSON_1:38 :: RasiowaNonClassical: p 69 (17)
a "/\" -a <= b "\/" -b;
theorem :: NELSON_1:39 :: RasiowaNonClassical: p 69 (18)
a <= b =-> (a "/\" b);
::NdR RasiowaNonClassical: p 70 1.3 (19)
theorem :: NELSON_1:40 :: (2.20)
a => !b = b => !a;
::NdR RasiowaNonClassical: p 70 1.3 (20)
theorem :: NELSON_1:41 :: (2.21)
(a => Top L) = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (21)
theorem :: NELSON_1:42 :: (2.22)
((Bottom L) => a) = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (22)
theorem :: NELSON_1:43 :: (2.23)
((Top L) => b) = b;
::NdR RasiowaNonClassical: p 70 1.3 (23)
theorem :: NELSON_1:44 :: (2.24)
a = Top L & a => b = Top L implies b = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (24)
theorem :: NELSON_1:45 :: (2.25)
a => (b => a) = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (25)
theorem :: NELSON_1:46 :: (2.26)
((a => (b => c)) => ((a => b) => (a => c))) = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (26)
theorem :: NELSON_1:47 :: (2.27)
(a => (a "\/" b)) = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (27)
theorem :: NELSON_1:48 :: (2.28)
b => (a "\/" b) = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (28)
theorem :: NELSON_1:49 :: (2.29)
(a => c) => ((b => c) => ((a "\/" b) => c)) = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (29)
theorem :: NELSON_1:50 :: (2.30)
(a "/\" b) => a = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (30)
theorem :: NELSON_1:51 :: (2.31)
(a "/\" b) => b = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (31)
theorem :: NELSON_1:52 :: (2.32)
(a => b) => ((a => c) => (a => (b "/\" c))) = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (32)
theorem :: NELSON_1:53 :: (2.33)
(a => !b) => (b => !a) = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (33)
theorem :: NELSON_1:54 :: (2.34)
(!(a => a)) => b = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (34)
theorem :: NELSON_1:55 :: (2.35)
(-a) => (a => b) = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (35)
theorem :: NELSON_1:56 :: (2.36)
((-(a => b)) => (a "/\" -b)) "/\" ((a "/\" -b) => -(a => b)) = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (36)
theorem :: NELSON_1:57 :: (2.37)
((-!a) => a) "/\" (a => (-!a)) = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (37)
theorem :: NELSON_1:58 :: (2.38)
--a = a;
::NdR RasiowaNonClassical: p 70 1.3 (39)
theorem :: NELSON_1:59 :: (2.39)
-(a "\/" b) = ((-a) "/\" (-b));
::NdR RasiowaNonClassical: p 70 1.3 (38)
theorem :: NELSON_1:60 :: (2.40)
-(a "/\" b) = ((-a) "\/" (-b));
::NdR RasiowaNonClassical: p 70 1.3 (40)
theorem :: NELSON_1:61 :: (2.41)
a < b implies b => c < a => c & c => a < c => b;
::NdR RasiowaNonClassical: p 70 1.3 (41)
theorem :: NELSON_1:62 :: (2.42)
(a => b) => ((c => d) => ((a "/\" c) => (b "/\" d))) = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (42)
theorem :: NELSON_1:63 :: (2.43)
(a => b) => ((c => d) => ((a "\/" c) => (b "\/" d))) = Top L;
::NdR RasiowaNonClassical: p 70 1.3 (43)
theorem :: NELSON_1:64 :: (2.44)
(b => a) => ((c => d) => ((a => c) => (b => d))) = Top L;
begin :: Alternative Equational Axiomatics by Rasiowa
definition let L be non empty NelsonStr;
attr L is satisfying_N0* means
:: NELSON_1:def 22
for a, b being Element of L holds
a <= b iff a =-> b = Top L;
::NdR RasiowaNonClassical: p 75 qpB1*
attr L is satisfying_N1* means
:: NELSON_1:def 23
for a, b being Element of L holds
a => (b => a) = Top L;
::NdR RasiowaNonClassical: p 75 qpB2*
attr L is satisfying_N2* means
:: NELSON_1:def 24
for a, b, c being Element of L holds
(a => (b => c)) => ((a => b) => (a => c)) = Top L;
::NdR RasiowaNonClassical: p 76 qpB3*
attr L is satisfying_N3* means
:: NELSON_1:def 25
for a being Element of L holds
((Top L) => a) = a;
::NdR RasiowaNonClassical: p 76 qpB5*
attr L is satisfying_N5* means
:: NELSON_1:def 26
for a, b being Element of L holds
((a =-> b) => ((b =-> a) => b)) = ((b =-> a) => ((a =-> b) => a));
::NdR RasiowaNonClassical: p 76 qpB6*
attr L is satisfying_N6* means
:: NELSON_1:def 27
for a, b being Element of L holds
a => (a "\/" b) = Top L;
::NdR RasiowaNonClassical: p 76 qpB7*
attr L is satisfying_N7* means
:: NELSON_1:def 28
for a, b being Element of L holds
b => (a "\/" b) = Top L;
::NdR RasiowaNonClassical: p 77 qpB8*
attr L is satisfying_N8* means
:: NELSON_1:def 29
for a, b, c being Element of L holds
(a => c) => ((b => c) => ((a "\/" b) => c)) = Top L;
::NdR RasiowaNonClassical: p 77 qpB9*
attr L is satisfying_N9* means
:: NELSON_1:def 30
for a, b being Element of L holds
(a "/\" b) => a = Top L;
::NdR RasiowaNonClassical: p 77 qpB10*
attr L is satisfying_N10* means
:: NELSON_1:def 31
for a, b being Element of L holds
(a "/\" b) => b = Top L;
::NdR RasiowaNonClassical: p 77 qpB11*
attr L is satisfying_N11* means
:: NELSON_1:def 32
for a, b, c being Element of L holds
(a => b) => ((a => c) => (a => (b "/\" c))) = Top L;
::NdR RasiowaNonClassical: p 77 qpB12*
attr L is satisfying_N12* means
:: NELSON_1:def 33
for a, b being Element of L holds
(a => !b) => (b => !a) = Top L;
::NdR RasiowaNonClassical: p 77 qpB13*
attr L is satisfying_N13* means
:: NELSON_1:def 34
for a, b being Element of L holds
(!(a => a)) => b = Top L;
::NdR RasiowaNonClassical: p 77 qpB14*
attr L is satisfying_N14* means
:: NELSON_1:def 35
for a, b being Element of L holds
(-a) => (a => b) = Top L;
::NdR RasiowaNonClassical: p 77 qpB15*
attr L is satisfying_N15* means
:: NELSON_1:def 36
for a, b being Element of L holds
((-(a => b)) => (a "/\" -b)) "/\" ((a "/\" -b) => -(a => b)) = Top L;
::NdR RasiowaNonClassical: p 77 qpB17*
attr L is satisfying_N17* means
:: NELSON_1:def 37
for a, b being Element of L holds
-(a "\/" b) = ((-a) "/\" (-b));
::NdR RasiowaNonClassical: p 77 qpB19*
attr L is satisfying_N19* means
:: NELSON_1:def 38
for a being Element of L holds
((-!a) => a) "/\" (a => (-!a)) = Top L;
end;
notation
let L be non empty NelsonStr;
::NdR RasiowaNonClassical: p 77 qpB4*
synonym L is satisfying_N4* for L is satisfying_N4;
::NdR RasiowaNonClassical: p 77 qpB16*
synonym L is satisfying_N16* for L is DeMorgan;
::NdR RasiowaNonClassical: p 77 qpB18*
synonym L is satisfying_N18* for L is involutive;
end;
registration
cluster -> satisfying_N1* satisfying_N2* satisfying_N3* satisfying_N4*
satisfying_N5* satisfying_N6* satisfying_N7* satisfying_N8*
satisfying_N9* satisfying_N10* satisfying_N11* satisfying_N12*
satisfying_N13* satisfying_N14* satisfying_N15* satisfying_N16*
satisfying_N17* satisfying_N18* satisfying_N19* for Nelson_Algebra;
end;
theorem :: NELSON_1:65
for L be non empty NelsonStr st
L is satisfying_N0* holds
L is Nelson_Algebra iff
L is satisfying_N1* satisfying_N2* satisfying_N3* satisfying_N4*
satisfying_N5* satisfying_N6* satisfying_N7* satisfying_N8*
satisfying_N9* satisfying_N10* satisfying_N11* satisfying_N12*
satisfying_N13* satisfying_N14* satisfying_N15* satisfying_N16*
satisfying_N17* satisfying_N18* satisfying_N19*;