What are the axioms of the class of lattices? I am asked to find a theory (set of $\mathcal{L}$-sentences) that axiomatizes the class of lattices. I wrote the following based on the definition that I'd found (over the language $\mathcal{L} = \{\leq, \cup, \cap \}$, where $\leq$ is a binary relation and $\cup, \cap$ are binary functions):


*

*$\forall x (x\leq x)$

*$\forall x \forall y \big( (x\leq y \land y \leq x) \to y = x\big)$

*$\forall x \forall y \forall z \big( (x \leq y \land y \leq z) \to x\leq z\big)$

*$\forall x \forall y \exists z (x\cup y = z \land x\leq z\land y\leq z)$

*$\forall x \forall y \exists z (x\cap y = z \land z\leq x \land z\leq y)$
I know it's customary to denote join and meet by $\lor, \land$, respectively, but I used set-theoretic notation to distinguish it from the logical symbols used in the formulas. 
Is this correct or am I missing (or got some sentences wrong) sentences?
 A: In your answer I read that a lattice is a partial order and that every pair $x,y\in L$ has an upper bound (in $x\cup y$) and has a lower bound (in $x\cap y$). That on its own is not enough for being a lattice. It should be stated the lower bound mentioned is the greatest lower bound, and that the upper bound mentioned is least upper bound.

Adopting your notation I would go for:
A lattice is a nonempty set $L$ together with two binary operations $\cup$ and
$\cap$ (read "join" and "meet"
respectively) such that the following identities are satisfied:


*

*$x\cup y=y\cup x$ and $x\cap y=y\cap x$ 

*$x\cup \left(y\cup z\right)=\left(x\cup y\right)\cup z$ and $x\cap \left(y\cap z\right)=\left(x\cap y\right)\cap z$ 

*$x\cup x=x$ and $x\cap x=x$

*$x\cup \left(x\cap y\right)=x$ and $x\cap \left(x\cup y\right)=x$
This mentions commutativity, associativity, idempotency and absorption respectively.
Actually idempotency is redundant (so the third bullet can be left out) because it is a consequence of absorption.
It can be proved on base of these axioms that the relation $\leq$ on $L$ determined by: $$x\leq y\iff x=x\cap y$$ is a partial order and also that moreover: $$x\leq y\iff y=x\cup y$$
If you want to go for sentences then you might add universal quantors.

Finally let me mention that for a poset in which every pair has a greatest lower bound and a least upper bound we can prove that the binary operations $\cup$ and
$\cap$ given by $x\cap y$ and $x\cup y$ defined as greatest lower bound and as least upper bound of $x$ and $y$ respectively satisfy the identities mentioned in the definition above. 
So actually you are quite close to a lattice. Only greatest and least were missing.
A: There is one major thing missing here: the axioms do not require $\cup$ to be the least upper bound. For example, if I take any partial order with a top element (say, $1$), then setting $x \cup y = 1$ for all $x,y$ would satisfy the axiom for $\cup$ you wrote. There is a similar problem with your axiom for $\cap$.
That being said, how can we fix this? First of all, we can simplify things. A lattice is fully encoded by either its order or its meet and join operations. We can recover the join and meet from the order as least upper bound and greatest lower bound respectively. The other way around, we can recover the order from the join as
$$
a \leq b \quad \Longleftrightarrow \quad a \cup b = b,
$$
or from the meet as
$$
a \leq b \quad \Longleftrightarrow \quad a \cap b = a,
$$
whatever you prefer.
So I will give the axiomatisations for both cases. First, if we only have an order symbol $\leq$:


*

*The first three axioms you mentioned (expressing $\leq$ is a partial order).

*$\forall xy \exists z(x \leq z \wedge y \leq z \wedge \forall w(x \leq w \wedge y \leq w \to z \leq w))$, expressing there is a least upper bound for any $x$ and $y$.

*$\forall xy \exists z(z \leq x \wedge z \leq y \wedge \forall w(w \leq x \wedge w \leq y \to w \leq z))$, expressing there is a greatest lower bound for any $x$ and $y$.


In the other case we have symbols $\cup$ and $\cap$ for join and meet. Then the following axioms are enough (see also Wikipedia for more information here):


*

*Commutativity: $\forall xy(x \cup y = y \cup x)$ and $\forall xy(x \cap y = y \cap x)$.

*Associativity: $\forall xyz((x \cup y) \cup z = x \cup (y \cup z))$ and $\forall xyz((x \cap y) \cap z = x \cap (y \cap z))$.

*Absorption: $\forall xy(x \cup (x \cap y) = x)$ and $\forall xy(x \cap (x \cup y) = x)$.

