Does Huntington's axiomatization of boolean algebras include idempotence? In different places Huntington's axiomatization of boolean algebras is

*

*$x\vee y=y\vee x$ for all $x$ and $y$,

*$(x\vee y)\vee z=x\vee(y\vee z)$ for all $x$, $y$ and $z$,

*$(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.
 A: 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$.
