The abstract of the Mizar article:

On the Two Short Axiomatizations of Ortholattices

by

Wioletta Truszkowska, and

Adam Grabowski

Received June 28, 2003

MML identifier: ROBBINS2

[ Mizar article, MML identifier index ]

environ

 vocabulary LATTICES, SUBSET_1, ARYTM_3, ROBBINS1, ROBBINS2;
 notation STRUCT_0, LATTICES, ROBBINS1;
 constructors REALSET1, ROBBINS1;
 clusters ROBBINS1;


begin :: One Axiom for Boolean Algebra

definition let L be non empty ComplLattStr;
  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;

definition
  cluster TrivComplLat -> satisfying_DN_1;
  cluster TrivOrtLat -> satisfying_DN_1;
end;

definition
  cluster join-commutative join-associative satisfying_DN_1
    (non empty ComplLattStr);
end;

 reserve L for satisfying_DN_1 (non empty ComplLattStr);
 reserve x, y, z, u, v for Element of L;

theorem :: ROBBINS2:1  :: A61
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z, u, v being Element of L holds
    ((x + y)` + (((z + u)` + x)` + (y` + (y + v)`)`)`)` = y;

theorem :: ROBBINS2:2  :: A62
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z, u being Element of L holds
    ((x + y)` + ((z + x)` + (y` + (y + u)`)`)`)` = y;

theorem :: ROBBINS2:3  :: A63
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x being Element of L holds
    ((x + x`)` + x)` = x`;

theorem :: ROBBINS2:4  :: A64
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z, u being Element of L holds
    ((x + y)` + ((z + x)` + (((y + y`)` + y)` + (y + u)`)`)`)` = y;

theorem :: ROBBINS2:5  :: A65
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    ((x + y)` + ((z + x)` + y)`)` = y;

theorem :: ROBBINS2:6  :: A66
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    ((x + y)` + (x` + y)`)` = y;

theorem :: ROBBINS2:7  :: A67
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (((x + y)` + x)` + (x + y)`)` = x;

theorem :: ROBBINS2:8  :: A68
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + ((x + y)` + x)`)` = (x + y)`;

theorem :: ROBBINS2:9  :: A69
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (((x + y)` + z)` + (x + z)`)` = z;

theorem :: ROBBINS2:10  :: A70
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (x + ((y + z)` + (y + x)`)`)` = (y + x)`;

theorem :: ROBBINS2:11  :: A71
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    ((((x + y)` + z)` + (x` + y)`)` + y)` = (x` + y)`;

theorem :: ROBBINS2:12  :: A72
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (x + ((y + z)` + (z + x)`)`)` = (z + x)`;

theorem :: ROBBINS2:13  :: A73
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z, u being Element of L holds
    ((x + y)` + ((z + x)` + (y` + (u + y)`)`)`)` = y;

theorem :: ROBBINS2:14  :: A74
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + y)` = (y + x)`;

theorem :: ROBBINS2:15  :: A75
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (((x + y)` + (y + z)`)` + z)` = (y + z)`;

theorem :: ROBBINS2:16  :: A76
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    ((x + ((x + y)` + z)`)` + z)` = ((x + y)` + z)`;

theorem :: ROBBINS2:17  :: A77
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (((x + y)` + x)` + y)` = (y + y)`;

theorem :: ROBBINS2:18  :: A78
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x` + (y + x)`)` = x;

theorem :: ROBBINS2:19  :: A79
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    ((x + y)` + y`)` = y;

theorem :: ROBBINS2:20  :: A80
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + (y + x`)`)` = x`;

theorem :: ROBBINS2:21  :: A81
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x being Element of L holds
    (x + x)` = x`;

theorem :: ROBBINS2:22  :: A83
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (((x + y)` + x)` + y)` = y`;

theorem :: ROBBINS2:23  :: A85
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x being Element of L holds
    x`` = x;

theorem :: ROBBINS2:24  :: A86
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    ((x + y)` + x)`+ y = y``;

theorem :: ROBBINS2:25  :: A87
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + y)`` = y + x;

theorem :: ROBBINS2:26  :: A88
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    x + ((y + z)` + (y + x)`)` = (y + x )``;

theorem :: ROBBINS2:27  :: A89
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    x + y = y + x;

definition
  cluster satisfying_DN_1 -> join-commutative (non empty ComplLattStr);
end;

theorem :: ROBBINS2:28  :: A90
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    ((x + y)` + x)` + y = y;

theorem :: ROBBINS2:29 :: A91
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    ((x + y)` + y)`+ x = x;

theorem :: ROBBINS2:30 :: A92
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    x + ((y + x)` + y)` = x;

theorem :: ROBBINS2:31  :: A93
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + y`)` + (y` + y)` = (x + y`)`;

theorem :: ROBBINS2:32  :: A94
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + y)` + (y + y`)` = (x + y)`;

theorem :: ROBBINS2:33 :: A95
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + y)` + (y` + y)` = (x + y)`;

theorem :: ROBBINS2:34  :: A96
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    ((x + y`)`` + y)` = (y` + y)`;

theorem :: ROBBINS2:35  :: A97
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    ((x + y`) + y)` = (y` + y)`;

theorem :: ROBBINS2:36  :: A98
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    ((((x + y`) + z)` + y)` + (y` + y)`)` = y;

theorem :: ROBBINS2:37  :: A99
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    x + ((y + z)` + (y + x)`)` = y + x;

theorem :: ROBBINS2:38  :: A100
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    x + (y + ((z + y)` + x)`)` = (z + y)` + x;

theorem :: ROBBINS2:39 :: A101
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    x + ((y + x)` + (y + z)`)` = y + x;

theorem :: ROBBINS2:40  :: A102
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    ((x + y)` + ((x + y)` + (x + z)`)`)` + y = y;

theorem :: ROBBINS2:41  :: A103
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (((x + y`) + z)` + y)`` = y;

theorem :: ROBBINS2:42  :: A104
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    x + ((y + x`) + z)` = x;

theorem :: ROBBINS2:43  :: A105
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    x` + ((y + x) + z)` = x`;

theorem :: ROBBINS2:44  :: A107
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + y)` + x = x + y`;

theorem :: ROBBINS2:45  :: A108
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + (x + y`)`)` = (x + y)`;

theorem :: ROBBINS2:46  :: A109
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    ((x + y)` + (x + z))` + y = y;

theorem :: ROBBINS2:47  :: A110
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (((x + y)` + z)` + (x` + y)`)` + y = (x` + y)``;

theorem :: ROBBINS2:48  :: A111
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (((x + y)` + z)` + (x` + y)`)` + y = x` + y;

theorem :: ROBBINS2:49  :: A112
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (x` + ((y + x)`` + (y + z))`)` + (y + z) = (y + x)``+ (y + z);

theorem :: ROBBINS2:50  :: A113
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (x` + ((y + x) + (y + z))`)` + (y + z) = (y + x)`` + (y + z);

theorem :: ROBBINS2:51  :: A114
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (x` + ((y + x) + (y + z))`)` + (y + z) = (y + x) + (y + z);

theorem :: ROBBINS2:52  :: A115
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    x`` + (y + z) = (y + x) + (y + z);

theorem :: ROBBINS2:53  :: A117
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (x + y) + (x + z) = y + (x + z);

theorem :: ROBBINS2:54 :: A118
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (x + y) + (x + z) = z + (x + y);

theorem :: ROBBINS2:55  :: A119
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    x + (y + z) = z + (y + x);

theorem :: ROBBINS2:56 :: A120
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    x + (y + z) = y + (z + x);

theorem :: ROBBINS2:57 :: A121
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (x + y) + z = x + (y + z);

definition
  cluster satisfying_DN_1 -> join-associative (non empty ComplLattStr);
  cluster satisfying_DN_1 -> Robbins (non empty ComplLattStr);
end;

theorem :: ROBBINS2:58
  for L being non empty ComplLattStr,
      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 non empty ComplLattStr st
    L is join-commutative join-associative Robbins holds
      L is satisfying_DN_1;

definition
  cluster join-commutative join-associative Robbins -> satisfying_DN_1
      (non empty ComplLattStr);
end;

definition
  cluster satisfying_DN_1 de_Morgan preOrthoLattice;
end;

definition
  cluster satisfying_DN_1 de_Morgan -> Boolean preOrthoLattice;
  cluster Boolean -> satisfying_DN_1 (well-complemented preOrthoLattice);
end;

begin :: Meredith Two Axioms for Boolean Algebras

definition let L be non empty ComplLattStr;
  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;

definition
  cluster satisfying_MD_1 satisfying_MD_2 ->
     join-commutative join-associative Huntington (non empty ComplLattStr);
  cluster join-commutative join-associative Huntington ->
     satisfying_MD_1 satisfying_MD_2 (non empty ComplLattStr);
end;

definition
  cluster satisfying_MD_1 satisfying_MD_2 satisfying_DN_1 de_Morgan
    preOrthoLattice;
end;

definition
  cluster satisfying_MD_1 satisfying_MD_2 de_Morgan ->
    Boolean preOrthoLattice;
  cluster Boolean -> satisfying_MD_1 satisfying_MD_2 (well-complemented
    preOrthoLattice);
end;