:: Axiomatization of {B}oolean Algebras Based on Sheffer Stroke
::  by Violetta Kozarkiewicz and Adam Grabowski
::
:: Received May 31, 2004
:: Copyright (c) 2004-2021 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, ROBBINS1, XBOOLE_0, SUBSET_1, ARYTM_3, EQREL_1,
      STRUCT_0, BINOP_1, FUNCT_5, RELAT_1, FUNCT_1, SHEFFER1, CARD_1;
 notations TARSKI, XBOOLE_0, FUNCT_5, ORDINAL1, CARD_1, STRUCT_0, LATTICES,
      BINOP_1, ROBBINS1;
 constructors BINOP_1, ROBBINS1, FUNCT_5;
 registrations LATTICES, LATTICE6, ROBBINS1, CARD_1, STRUCT_0;


begin :: Preliminaries

theorem :: SHEFFER1:1
  for L being join-commutative join-associative Huntington non
  empty ComplLLattStr, a, b being Element of L holds (a + b)` = a` *' b`;

begin :: Huntington's First Axiomatization of Boolean Algebras

definition
  let IT be non empty LattStr;
  attr IT is upper-bounded' means
:: SHEFFER1:def 1

  ex c being Element of IT st for a
  being Element of IT holds c "/\" a = a & a "/\" c = a;
end;

definition
  let L be non empty LattStr;
  assume
 L is upper-bounded';
  func Top' L -> Element of L means
:: SHEFFER1:def 2

  for a being Element of L holds it "/\" a = a & a "/\" it = a;
end;

definition
  let IT be non empty LattStr;
  attr IT is lower-bounded' means
:: SHEFFER1:def 3

  ex c being Element of IT st for a
  being Element of IT holds c "\/" a = a & a "\/" c = a;
end;

definition
  let L be non empty LattStr;
  assume
 L is lower-bounded';
  func Bot' L -> Element of L means
:: SHEFFER1:def 4

  for a being Element of L holds it "\/" a = a & a "\/" it = a;
end;

definition
  let IT be non empty LattStr;
  attr IT is distributive' means
:: SHEFFER1:def 5

  for a, b, c being Element of IT holds
  a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c);
end;

definition
  let L be non empty LattStr, a, b be Element of L;
  pred a is_a_complement'_of b means
:: SHEFFER1:def 6

  b "\/" a = Top' L & a "\/" b = Top' L &
  b "/\" a = Bot' L & a "/\" b = Bot' L;
end;

definition
  let IT be non empty LattStr;
  attr IT is complemented' means
:: SHEFFER1:def 7

  for b being Element of IT ex a being
  Element of IT st a is_a_complement'_of b;
end;

definition
  let L be non empty LattStr, x be Element of L;
  assume
 L is complemented' distributive upper-bounded' meet-commutative;
  func x `# -> Element of L means
:: SHEFFER1:def 8

  it is_a_complement'_of x;
end;

registration
  cluster Boolean join-idempotent upper-bounded' complemented' distributive'
    lower-bounded' Lattice-like for 1-element LattStr;
end;

theorem :: SHEFFER1:2
  for L being complemented' join-commutative meet-commutative
distributive upper-bounded' distributive' non empty LattStr for x be Element
  of L holds x "\/" x `# = Top' L;

theorem :: SHEFFER1:3
  for L being complemented' join-commutative meet-commutative
  distributive upper-bounded' distributive' non empty LattStr for x being
  Element of L holds x "/\" x `# = Bot' L;

theorem :: SHEFFER1:4
  for L being complemented' join-commutative meet-commutative
  join-idempotent distributive upper-bounded' distributive' non empty LattStr
  for x being Element of L holds x "\/" Top' L = Top' L;

theorem :: SHEFFER1:5
  for L being complemented' join-commutative meet-commutative
  join-idempotent distributive upper-bounded' lower-bounded' distributive' non
  empty LattStr for x being Element of L holds x "/\" Bot' L = Bot' L;

theorem :: SHEFFER1:6
  for L being join-commutative meet-absorbing meet-commutative
  join-absorbing join-idempotent distributive non empty LattStr for x, y, z
  being Element of L holds ((x "\/" y) "\/" z) "/\" x = x;

theorem :: SHEFFER1:7
  for L being join-commutative meet-absorbing meet-commutative
  join-absorbing join-idempotent distributive' non empty LattStr for x, y, z
  being Element of L holds ((x "/\" y) "/\" z) "\/" x = x;

definition
  let G be non empty /\-SemiLattStr;
  attr G is meet-idempotent means
:: SHEFFER1:def 9

  for x being Element of G holds x "/\" x = x;
end;

theorem :: SHEFFER1:8
  for L being complemented' join-commutative meet-commutative
  distributive upper-bounded' lower-bounded' distributive' non empty LattStr
  holds L is meet-idempotent;

theorem :: SHEFFER1:9
  for L being complemented' join-commutative meet-commutative
  distributive upper-bounded' lower-bounded' distributive' non empty LattStr
  holds L is join-idempotent;

theorem :: SHEFFER1:10
  for L being complemented' join-commutative meet-commutative
  join-idempotent distributive upper-bounded' distributive' non empty LattStr
  holds L is meet-absorbing;

theorem :: SHEFFER1:11
  for L being complemented' join-commutative upper-bounded'
meet-commutative join-idempotent distributive distributive' lower-bounded' non
  empty LattStr holds L is join-absorbing;

theorem :: SHEFFER1:12
  for L being complemented' join-commutative meet-commutative
  upper-bounded' lower-bounded' join-idempotent distributive distributive' non
  empty LattStr holds L is upper-bounded;

theorem :: SHEFFER1:13
  for L being Boolean Lattice-like non empty LattStr holds L is
  upper-bounded';

theorem :: SHEFFER1:14
  for L being complemented' join-commutative meet-commutative
  upper-bounded' lower-bounded' join-idempotent distributive distributive' non
  empty LattStr holds L is lower-bounded;

theorem :: SHEFFER1:15
  for L being Boolean Lattice-like non empty LattStr holds L is
  lower-bounded';

theorem :: SHEFFER1:16
  for L being join-commutative meet-commutative meet-absorbing
  join-absorbing join-idempotent distributive non empty LattStr holds L is
  join-associative;

theorem :: SHEFFER1:17
  for L being join-commutative meet-commutative meet-absorbing
  join-absorbing join-idempotent distributive' non empty LattStr holds L is
  meet-associative;

theorem :: SHEFFER1:18
  for L being complemented' join-commutative meet-commutative
  lower-bounded' upper-bounded' join-idempotent distributive distributive' non
  empty LattStr holds Top L = Top' L;

theorem :: SHEFFER1:19
  for L being complemented' join-commutative meet-commutative
  lower-bounded' upper-bounded' join-idempotent distributive distributive' non
  empty LattStr holds Bottom L = Bot' L;

theorem :: SHEFFER1:20
  for L being Boolean distributive' Lattice-like non empty
  LattStr holds Top L = Top' L;

theorem :: SHEFFER1:21
  for L being Boolean complemented lower-bounded upper-bounded
  distributive distributive' Lattice-like non empty LattStr holds Bottom L =
  Bot' L;

theorem :: SHEFFER1:22
  for L being complemented' lower-bounded' upper-bounded'
  join-commutative meet-commutative join-idempotent distributive distributive'
  non empty LattStr, x, y being Element of L holds
  x is_a_complement'_of y iff x is_a_complement_of y;

theorem :: SHEFFER1:23
  for L being complemented' join-commutative meet-commutative
  lower-bounded' upper-bounded' join-idempotent distributive distributive' non
  empty LattStr holds L is complemented;

theorem :: SHEFFER1:24
  for L being Boolean lower-bounded' upper-bounded' distributive'
  Lattice-like non empty LattStr holds L is complemented';

theorem :: SHEFFER1:25
  for L being non empty LattStr holds L is Boolean Lattice iff L
is lower-bounded' upper-bounded' join-commutative meet-commutative distributive
  distributive' complemented';

registration
  cluster Boolean Lattice-like -> lower-bounded' upper-bounded' complemented'
join-commutative meet-commutative distributive distributive' for
non empty LattStr;
  cluster lower-bounded' upper-bounded' complemented' join-commutative
meet-commutative distributive distributive' -> Boolean Lattice-like for
non empty
    LattStr;
end;

begin :: Axiomatization Based on Sheffer Stroke

definition
  struct (1-sorted) ShefferStr (# carrier -> set, stroke -> BinOp of the
    carrier #);
end;

definition
  struct (ShefferStr,LattStr) ShefferLattStr (# carrier -> set, L_join ->
BinOp of the carrier, L_meet -> BinOp of the carrier, stroke -> BinOp of the
    carrier #);
end;

definition
  struct (ShefferStr,OrthoLattStr) ShefferOrthoLattStr (# carrier -> set,
L_join -> BinOp of the carrier, L_meet -> BinOp of the carrier, Compl -> UnOp
    of the carrier, stroke -> BinOp of the carrier #);
end;

definition
  func TrivShefferOrthoLattStr -> ShefferOrthoLattStr equals
:: SHEFFER1:def 10
  ShefferOrthoLattStr (# {0}, op2, op2, op1, op2 #);
end;

registration
  cluster 1-element for ShefferStr;
  cluster 1-element for ShefferLattStr;
  cluster 1-element for ShefferOrthoLattStr;
end;

definition
  let L be non empty ShefferStr;
  let x, y be Element of L;
  func x | y -> Element of L equals
:: SHEFFER1:def 11
  (the stroke of L).(x,y);
end;

definition
  let L be non empty ShefferOrthoLattStr;
  attr L is properly_defined means
:: SHEFFER1:def 12

  (for x being Element of L holds x |
x = x`) & (for x, y being Element of L holds x "\/" y = (x | x) | (y | y)) & (
  for x, y being Element of L holds x "/\" y = (x | y) | (x | y)) & for x, y
  being Element of L holds x | y = x` + y`;
end;

definition
  let L be non empty ShefferStr;
  attr L is satisfying_Sheffer_1 means
:: SHEFFER1:def 13

  for x being Element of L holds (x | x) | (x | x) = x;
  attr L is satisfying_Sheffer_2 means
:: SHEFFER1:def 14

  for x, y being Element of L holds x | (y | (y | y)) = x | x;
  attr L is satisfying_Sheffer_3 means
:: SHEFFER1:def 15

  for x, y, z being Element of L
  holds (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x);
end;

registration
  cluster -> satisfying_Sheffer_1 satisfying_Sheffer_2
    satisfying_Sheffer_3 for 1-element ShefferStr;
end;

registration
  cluster  -> join-commutative join-associative
   for 1-element \/-SemiLattStr;
  cluster  -> meet-commutative meet-associative
        for 1-element /\-SemiLattStr;
end;

registration
  cluster -> join-absorbing meet-absorbing Boolean for 1-element LattStr;
end;

registration
  cluster TrivShefferOrthoLattStr -> 1-element;
  cluster TrivShefferOrthoLattStr -> properly_defined well-complemented;
end;

registration
  cluster properly_defined Boolean well-complemented Lattice-like
    satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for
    non empty ShefferOrthoLattStr;
end;

theorem :: SHEFFER1:26
  for L being properly_defined Boolean well-complemented Lattice-like
  non empty ShefferOrthoLattStr holds L is satisfying_Sheffer_1;

theorem :: SHEFFER1:27
  for L being properly_defined Boolean well-complemented Lattice-like
  non empty ShefferOrthoLattStr holds L is satisfying_Sheffer_2;

theorem :: SHEFFER1:28
  for L being properly_defined Boolean well-complemented Lattice-like
  non empty ShefferOrthoLattStr holds L is satisfying_Sheffer_3;

definition
  let L be non empty ShefferStr;
  let a be Element of L;
  func a" -> Element of L equals
:: SHEFFER1:def 16
  a | a;
end;

theorem :: SHEFFER1:29
  for L being satisfying_Sheffer_3 non empty ShefferOrthoLattStr, x, y
  , z being Element of L holds (x | (y | z))" = (y" | x) | (z" | x);

theorem :: SHEFFER1:30
  for L being satisfying_Sheffer_1 non empty ShefferOrthoLattStr, x
  being Element of L holds x = (x")";

theorem :: SHEFFER1:31
  for L being satisfying_Sheffer_1 satisfying_Sheffer_2
  satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr, x, y
  being Element of L holds x | y = y | x;

theorem :: SHEFFER1:32
  for L being satisfying_Sheffer_1 satisfying_Sheffer_2
  satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr, x, y
  being Element of L holds x | (x | x) = y | (y | y);

theorem :: SHEFFER1:33
  for L being satisfying_Sheffer_1 satisfying_Sheffer_2
  satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
  is join-commutative;

theorem :: SHEFFER1:34
  for L being satisfying_Sheffer_1 satisfying_Sheffer_2
  satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
  is meet-commutative;

theorem :: SHEFFER1:35
  for L being satisfying_Sheffer_1 satisfying_Sheffer_2
  satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
  is distributive;

theorem :: SHEFFER1:36
  for L being satisfying_Sheffer_1 satisfying_Sheffer_2
  satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
  is distributive';

theorem :: SHEFFER1:37
  for L being satisfying_Sheffer_1 satisfying_Sheffer_2
  satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L
  is Boolean Lattice;