Does Huntington's axiomatization of boolean algebras include idempotence?

Question

In different places Huntington's axiomatization of boolean algebras is

1. $x\vee y=y\vee x$ for all $x$ and $y$,
2. $(x\vee y)\vee z=x\vee(y\vee z)$ for all $x$, $y$ and $z$,
3. $(x'\vee y)'\vee(x'\vee y')'=x$ for all $x$ and $y$.

I am not able to show that idempotence $x\vee x=x$ for all $x$ follows.

In Huntington 1933 however, idempotence is included in the list of axioms.

My question: Can boolean algebras be axiomatized without idempotence? If 'yes' a proof of idempotence would be welcome.

Answer 1

By replacing $(x,y)$ in $$(x'\vee y)'\vee(x'\vee y')'=x \tag{H}$$ by $(x,x''), (x',x''), (x',x')$ and $(x'',x')$, respectively, we get \begin{align} (x'\vee x'')'\vee(x'\vee x''')' &= x \tag{1}\\ (x''\vee x'')'\vee(x''\vee x''')' &= x' \tag{2}\\ (x''\vee x'')'\vee(x''\vee x')' &= x' \tag{3}\\ (x'''\vee x')'\vee(x'''\vee x'')' &= x'' \tag{4} \end{align}

Now, using the above, let us see that $x\vee x'=x'\vee x''$.
\begin{align} x \vee x' &= (x'\vee x'')'\vee(x'\vee x''')' \vee x' \tag{by (1)}\\ &= ((x'\vee x'')'\vee(x'\vee x''')') \vee ((x''\vee x'')'\vee(x''\vee x''')') \tag{by (2)}\\ &= ((x''\vee x'')'\vee(x''\vee x')') \vee ((x'''\vee x'')'\vee(x'''\vee x')') \tag{com&assoc}\\ &= x' \vee x''. \tag{by (3) and (4)} \end{align} (The step above justified as "com&assoc" means that it's by commutativity and associativity.)

From $x\vee x'=x'\vee x''$ we conclude that $$x'\vee x'' = x'' \vee x'''$$ (applying the formula to $x'$ in place of $x$), and, by commutativity, $$x'\vee x'' = x'''\vee x''.$$ This allows to see that the LHS of (1) and (4) are the same, and so, $$x''=x.\tag{5}$$

We also have that $(x \vee x')' = (y \vee y')'$ for every $x$ and $y$.
Indeed, from \begin{align} x &= (x' \vee y')' \vee (x' \vee y'')'\\ x' &= (x'' \vee y')' \vee (x'' \vee y'')' \end{align} we get, after some recombination as above, the desired result. Thus, we can define a constant $$0 = (x \vee x')'.$$ In particular, using $x''=x$, it follows that $$0\vee0'=0',\tag{6}$$ and, as $0'=x \vee x'$, for all $x$, taking $x=0\vee0$, $$(0\vee0)\vee(0\vee0)'=0',$$ But \begin{align} 0' &= (0''\vee0)'\vee(0''\vee0')'\tag{by (H)}\\ &= (0\vee0)'\vee(0\vee0')'\\ &= (0\vee0)'\vee0''\tag{by (6)}\\ &= 0 \vee (0 \vee 0)', \end{align} and so $$(0 \vee 0) \vee (0 \vee 0)' = 0 \vee (0 \vee 0)'. \tag{7}$$

Next, we show that $0\vee0=0$.
We saw above that $0'=0 \vee (0 \vee 0)'$, and so by (7), \begin{align} 0 \vee 0' = (0\vee 0) \vee (0 \vee 0)' = (0 \vee 0)', \end{align} whence, by (6), $0' = (0 \vee 0)'$, and therefore, $$0 = 0 \vee 0.\tag{8}$$

Now we prove that $x \vee 0 = x$. \begin{align} (x \vee 0)' &= ((x\vee0)\vee0)' \vee ((x\vee0)\vee0')'\tag{by (H)}\\ &= (x \vee (0\vee0))' \vee (x \vee (0\vee0'))'\tag{associativity}\\ &= (x\vee 0)' \vee (x \vee 0')'\tag{by (6) and (8)}\\ &= x'.\tag{by (H)} \end{align}

Finally, \begin{align} x' &= (x \vee x)' \vee (x \vee x')' \tag{by (H)}\\ &= (x \vee x)' \vee 0\\ &= (x \vee x)', \end{align} whence $x = x \vee x$.