:: On the Two Short Axiomatizations of Ortholattices
:: by Wioletta Truszkowska and Adam Grabowski
::
:: Received June 28, 2003
:: Copyright (c) 2003-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 XBOOLE_0, ROBBINS1, SUBSET_1, ARYTM_3, LATTICES, ROBBINS2;
notations STRUCT_0, LATTICES, ROBBINS1;
constructors ROBBINS1;
registrations LATTICES, ROBBINS1, STRUCT_0;
begin :: One Axiom for Boolean Algebra
definition
let L be non empty ComplLLattStr;
attr L is satisfying_DN_1 means
:: ROBBINS2:def 1
for x, y, z, u being Element of L
holds (((x + y)` + z)` + (x + (z` + (z + u)`)`)`)` = z;
end;
registration
cluster TrivComplLat -> satisfying_DN_1;
cluster TrivOrtLat -> satisfying_DN_1;
end;
registration
cluster join-commutative join-associative satisfying_DN_1 for non empty
ComplLLattStr;
end;
reserve L for satisfying_DN_1 non empty ComplLLattStr;
reserve x, y, z for Element of L;
theorem :: ROBBINS2:1
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u,
v being Element of L holds ((x + y)` + (((z + u)` + x)` + (y` + (y + v)`)`)`)`
= y;
theorem :: ROBBINS2:2
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u
being Element of L holds ((x + y)` + ((z + x)` + (y` + (y + u)`)`)`)` = y;
theorem :: ROBBINS2:3
for L being satisfying_DN_1 non empty ComplLLattStr, x being
Element of L holds ((x + x`)` + x)` = x`;
theorem :: ROBBINS2:4
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u
being Element of L holds ((x + y)` + ((z + x)` + (((y + y`)` + y)` + (y + u)`)`
)`)` = y;
theorem :: ROBBINS2:5
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds ((x + y)` + ((z + x)` + y)`)` = y;
theorem :: ROBBINS2:6
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds ((x + y)` + (x` + y)`)` = y;
theorem :: ROBBINS2:7
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (((x + y)` + x)` + (x + y)`)` = x;
theorem :: ROBBINS2:8
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + ((x + y)` + x)`)` = (x + y)`;
theorem :: ROBBINS2:9
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (((x + y)` + z)` + (x + z)`)` = z;
theorem :: ROBBINS2:10
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (x + ((y + z)` + (y + x)`)`)` = (y + x)`;
theorem :: ROBBINS2:11
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds ((((x + y)` + z)` + (x` + y)`)` + y)` = (x` + y)`;
theorem :: ROBBINS2:12
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (x + ((y + z)` + (z + x)`)`)` = (z + x)`;
theorem :: ROBBINS2:13
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u
being Element of L holds ((x + y)` + ((z + x)` + (y` + (u + y)`)`)`)` = y;
theorem :: ROBBINS2:14
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + y)` = (y + x)`;
theorem :: ROBBINS2:15
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (((x + y)` + (y + z)`)` + z)` = (y + z)`;
theorem :: ROBBINS2:16
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds ((x + ((x + y)` + z)`)` + z)` = ((x + y)` + z)`;
theorem :: ROBBINS2:17
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (((x + y)` + x)` + y)` = (y + y)`;
theorem :: ROBBINS2:18
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x` + (y + x)`)` = x;
theorem :: ROBBINS2:19
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds ((x + y)` + y`)` = y;
theorem :: ROBBINS2:20
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + (y + x`)`)` = x`;
theorem :: ROBBINS2:21
for L being satisfying_DN_1 non empty ComplLLattStr, x being
Element of L holds (x + x)` = x`;
theorem :: ROBBINS2:22
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (((x + y)` + x)` + y)` = y`;
theorem :: ROBBINS2:23
for L being satisfying_DN_1 non empty ComplLLattStr, x being
Element of L holds x`` = x;
theorem :: ROBBINS2:24
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds ((x + y)` + x)`+ y = y``;
theorem :: ROBBINS2:25
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + y)`` = y + x;
theorem :: ROBBINS2:26
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds x + ((y + z)` + (y + x)`)` = (y + x )``;
theorem :: ROBBINS2:27
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds x + y = y + x;
registration
cluster satisfying_DN_1 -> join-commutative for non empty ComplLLattStr;
end;
theorem :: ROBBINS2:28
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds ((x + y)` + x)` + y = y;
theorem :: ROBBINS2:29
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds ((x + y)` + y)`+ x = x;
theorem :: ROBBINS2:30
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds x + ((y + x)` + y)` = x;
theorem :: ROBBINS2:31
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + y`)` + (y` + y)` = (x + y`)`;
theorem :: ROBBINS2:32
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + y)` + (y + y`)` = (x + y)`;
theorem :: ROBBINS2:33
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + y)` + (y` + y)` = (x + y)`;
theorem :: ROBBINS2:34
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds ((x + y`)`` + y)` = (y` + y)`;
theorem :: ROBBINS2:35
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds ((x + y`) + y)` = (y` + y)`;
theorem :: ROBBINS2:36
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds ((((x + y`) + z)` + y)` + (y` + y)`)` = y;
theorem :: ROBBINS2:37
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds x + ((y + z)` + (y + x)`)` = y + x;
theorem :: ROBBINS2:38
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds x + (y + ((z + y)` + x)`)` = (z + y)` + x;
theorem :: ROBBINS2:39
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being
Element of L holds x + ((y + x)` + (y + z)`)` = y + x;
theorem :: ROBBINS2:40
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds ((x + y)` + ((x + y)` + (x + z)`)`)` + y = y;
theorem :: ROBBINS2:41
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (((x + y`) + z)` + y)`` = y;
theorem :: ROBBINS2:42
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds x + ((y + x`) + z)` = x;
theorem :: ROBBINS2:43
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds x` + ((y + x) + z)` = x`;
theorem :: ROBBINS2:44
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + y)` + x = x + y`;
theorem :: ROBBINS2:45
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + (x + y`)`)` = (x + y)`;
theorem :: ROBBINS2:46
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds ((x + y)` + (x + z))` + y = y;
theorem :: ROBBINS2:47
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (((x + y)` + z)` + (x` + y)`)` + y = (x` + y)``;
theorem :: ROBBINS2:48
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (((x + y)` + z)` + (x` + y)`)` + y = x` + y;
theorem :: ROBBINS2:49
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (x` + ((y + x)`` + (y + z))`)` + (y + z) = (y + x)``+
(y + z);
theorem :: ROBBINS2:50
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (x` + ((y + x) + (y + z))`)` + (y + z) = (y + x)`` + (
y + z);
theorem :: ROBBINS2:51
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (x` + ((y + x) + (y + z))`)` + (y + z) = (y + x) + (y
+ z);
theorem :: ROBBINS2:52
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds x`` + (y + z) = (y + x) + (y + z);
theorem :: ROBBINS2:53
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (x + y) + (x + z) = y + (x + z);
theorem :: ROBBINS2:54
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being
Element of L holds (x + y) + (x + z) = z + (x + y);
theorem :: ROBBINS2:55
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds x + (y + z) = z + (y + x);
theorem :: ROBBINS2:56
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being
Element of L holds x + (y + z) = y + (z + x);
theorem :: ROBBINS2:57
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being
Element of L holds (x + y) + z = x + (y + z);
registration
cluster satisfying_DN_1 -> join-associative for non empty ComplLLattStr;
cluster satisfying_DN_1 -> Robbins for non empty ComplLLattStr;
end;
theorem :: ROBBINS2:58
for L being non empty ComplLLattStr, x, z being Element of L st L
is join-commutative join-associative Huntington holds (z + x) *' (z + x`) = z
;
theorem :: ROBBINS2:59
for L being join-commutative join-associative non empty ComplLLattStr
st L is Robbins holds L is satisfying_DN_1;
registration
cluster join-commutative join-associative Robbins -> satisfying_DN_1 for non
empty ComplLLattStr;
end;
registration
cluster satisfying_DN_1 de_Morgan for preOrthoLattice;
end;
registration
cluster satisfying_DN_1 de_Morgan -> Boolean for preOrthoLattice;
cluster Boolean -> satisfying_DN_1 for well-complemented preOrthoLattice;
end;
begin :: Meredith Two Axioms for Boolean Algebras
definition
let L be non empty ComplLLattStr;
attr L is satisfying_MD_1 means
:: ROBBINS2:def 2
for x, y being Element of L holds (x` + y)` + x = x;
attr L is satisfying_MD_2 means
:: ROBBINS2:def 3
for x, y, z being Element of L holds (x` + y)` + (z + y) = y + (z + x);
end;
registration
cluster satisfying_MD_1 satisfying_MD_2 -> join-commutative join-associative
Huntington for non empty ComplLLattStr;
cluster join-commutative join-associative Huntington -> satisfying_MD_1
satisfying_MD_2 for non empty ComplLLattStr;
end;
registration
cluster satisfying_MD_1 satisfying_MD_2 satisfying_DN_1 de_Morgan
for preOrthoLattice;
end;
registration
cluster satisfying_MD_1 satisfying_MD_2 de_Morgan -> Boolean for
preOrthoLattice;
cluster Boolean -> satisfying_MD_1 satisfying_MD_2 for well-complemented
preOrthoLattice;
end;