@MISC{SHEFFER1.MIZ,
  AUTHOR = {Kozarkiewicz, Violetta and Grabowski, Adam},
  TITLE = {Axiomatization of {B}oolean Algebras Based on {S}heffer Stroke},
  SECTION1 = {Preliminaries},
  SECTION2 = {Huntington's First Axiomatization of Boolean Algebras},
  SECTION3 = {Axiomatization Based on Sheffer Stroke},
  DAY = {31},
  MONTH = {May},
  YEAR = {2004},
  ADDRESS1 = {University of Bia{\l}ystok},
  ADDRESS2 = {University of Bia{\l}ystok},
  SUMMARY = {We formalized another axiomatization of Boolean algebras. The classical
  one, as introduced in \cite{LATTICES.ABS},
  ``the fourth set of postulates''
  due to Huntington \cite{Huntington1} (\cite{ROBBINS1.ABS} in Mizar)
  and the single axiom
  in terms of disjunction and negation \cite{ROBBINS2.ABS}.
  In this article, we aimed at the description of Boolean algebras
  using Sheffer stroke according to \cite{Sheffer:1913}, namely
  by the following three axioms:
  $$(x | x) | (x | x) = x$$
  $$x | (y | (y | y)) = x | x$$
  $$(x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x)$$
  ($\upharpoonright$ is used instead of $|$ in the translation
  of our Mizar article).
  Since M.~Sheffer in his original paper proved the equivalence
  of it and Huntington's ``first set of postulates'', we introduced
  also this axiomatization of BAs.}}


@ARTICLE{Sheffer:1913,
    AUTHOR = {Sheffer, Maurice},
     TITLE = {A Set of Five Independent Postulates
              for Boolean Algebras, with Application to Logical Constants},
   JOURNAL = {Transactions of American Mathematical Society},
    VOLUME = {14},
    NUMBER = {4},
     PAGES = {481--488},
      YEAR = {1913}}