Do these axioms define a boolean algebra? In Awodey's "Category Theory", he defines a boolean algebra $\mathcal{B}$ as

*

*a poset $(B,\leq)$ along with

*two elements $0$ and $1$, along with

*two binary operations $\lor, \land$, and

*an unary operation $\lnot$
such that

*

*$0 \leq a$

*$a \leq 1$

*$a \leq c,\;b \leq c \iff a \lor b \leq c$

*$c \leq a,\;c \leq b \iff c \leq a \land b$

*$a \leq \lnot b \iff a \land b = 0$

*$\lnot \lnot a = a$
From wikipedia I see that a boolean algebra is a distributive complemented lattice. The first 4 axioms make $\mathcal{B}$ a bounded lattice, and I was able to convince myself that 1-6 imply that the lattice is complemented and that the complement is unique.
I can not seem to show that 1-6 imply distributivity. I can use 3-4 to show that
$$
(a \land b) \lor (a \land c) \leq a \land (b \lor c)
$$
But can't show that 1-6 imply the converse, i.e. that 1-6 imply
$$
a \land (b \lor c) \leq (a \land b) \lor (a \land c)
$$
 A: It seems like you already deduced that
$$x\wedge x = x,\quad
x\wedge y = y \wedge x,\quad
x\wedge(y\wedge z) = (x\wedge y)\wedge z$$
are identities satisfied by the algebra.
(And also that $a\wedge b=a$ iff $a\leq b$.)
Now consider the result

Theorem (O. Frink).
Let $\mathbf A = (A,\cdot,',0)$ be an algebra of type $(2,1,0)$ (that is, $\cdot$ is binary, $'$ is unary, and $0$ is nullary), such that
$(1)\quad xx=x$,
$(2)\quad xy=yx,$
$(3)\quad (xy)z=x(yz),$
$(4)\quad xy=x$ iff $xy'=0$.
Define $\mathbf B = (A,\cdot,+,',0,1)$, where $x+y=(x'y')'$ and $1=0'$.
Then $\mathbf B$ is a Boolean algebra.

The original proof is in
O. Frink, Representations of Boolean algebras, Bulletin Amer. Math. Soc. 47 (1941) 775-776.
An alternative proof (without using duality) can be found in
R. Padmanabhan, A first order proof of a theorem of Frink, Algebra Universalis, 13 (1981) 397-400.
Here, there is an explicit proof of the distributivity.
Now you only have to prove that your algebra satisfies condition $(4)$ of Frink's theorem.
Using your conditions (5) and (6), if $a$ and $b$ are members of the algebra, then
$$ab=a \Leftrightarrow a \leq b \Leftrightarrow a \leq b'' \Leftrightarrow ab'=0,$$
and so indeed, the algebra satisfies all the hypothesis in the theorem.
