Completeness of a quantifier-free axiomatization of Boolean algebra using partial-ordering

Question

Consider the following set of axioms:

1. $a \leq a$
2. $(a \leq b \mathrel{\&} b \leq a) \Rightarrow a = b$
3. $(a \leq b \mathrel{\&} b \leq c) \Rightarrow a \leq c$
4. $0 \leq a \mathrel{\&} a \leq 1$
5. $a \leq a \lor b \mathrel{\&} b \leq a \lor b \mathrel{\&} ((a \leq c \mathrel{\&} b \leq c) \Rightarrow a \lor b \leq c)$
6. $a \land b \leq a \mathrel{\&} a \land b \leq b \mathrel{\&} ((c \leq a \mathrel{\&} c \leq b) \Rightarrow c \leq a \land b)$
7. $((a \leq b \mathrel{\&} a \leq \neg b) \Rightarrow a \leq 0) \mathrel{\&} ((b \leq a \mathrel{\&} \neg b \leq a) \Rightarrow 1 \leq a)$
8. $a \nleq \neg b \Rightarrow \exists x (x \neq 0 \mathrel{\&} x \leq a \mathrel{\&} x \leq b)$

[1] says axioms 7 and 8 are independent from axioms 1-6, and that axioms 1-8 are complete for Boolean algebras, but not that axioms 7 and 8 are independent from one another in the presence of axioms 1-6, leaving open the possibility that axioms 1-7 are also complete for Boolean algebras. So my question is: are they? If not, is there a quantifier-free extension of axioms 1-7 that is?

[1]: Huntington, E. V.. "Sets of Independent Postulates for the Algebra of Logic", Transactions of the American Mathematical Society, vol. 5, no. 3, 1904, pp. 288-309.

Answer 1

Axiom 8 can be replaced by the axiom $a\vee(b\wedge c)=(a\vee b)\wedge (a\vee c)$. In the language of order theory, axioms 1-6 describe a (bounded) lattice, and adding axiom 7 gives you a complemented lattice (with a specific choice of complement operation). Boolean algebras are the same thing as complemented distributive lattices, so all you need to add to axioms 1-7 is the distributive law.

Answer 2

Here's an answer to the first question: $(8)$ cannot be proved from $(1)$-$(7)$. There is in fact a nice countermodel, namely the lattice $M_3$ equipped with a "negation" operation which yields a derangement of the intermediate elements.

More precisely, our countermodel will have underlying set $\{0,1,x,y,z\}$. The partial order is given by setting $0$ at the botom, $1$ at the top, and no other inequalities holding besides reflexivity; $\wedge$ and $\vee$ are the the usual join and meet operations. See here for a picture of this. We then let negation be the unary function sending $0$ to $1$, $1$ to $0$, and $$x\mapsto y\mapsto z\mapsto x.$$

Incidentally, the lattice $M_3$ itself (so, the countermodel without negation) is an important example in order theory; it's one of the two lattices characterizing non-distributivity, the other being $N_5$.

Of course, this leaves the second question open. EDIT: per Eric Wofsey's answer, the answer to the second question is yes.