Do these axioms define a boolean algebra?

Question

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

1. $0 \leq a$
2. $a \leq 1$
3. $a \leq c,\;b \leq c \iff a \lor b \leq c$
4. $c \leq a,\;c \leq b \iff c \leq a \land b$
5. $a \leq \lnot b \iff a \land b = 0$
6. $\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) $$

Answer 1

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.