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?
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$:
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):