Express lattice axioms using implication and universal quantification

Question

I'd like to ask for some help with homework. My task is to express lattice axioms in signature $(\leq, =, \sup, \inf)$ using only implication and universal quantification. Here are these axioms in $(\leq, =)$ signature:

• $\forall x (x \leq x)$ - reflexivity
• $\forall x \forall y \forall z (x \leq y \land y \leq z \to x \leq z)$ - transitivity
• $\forall x \forall y (x \leq y \land y \leq x \to x = y)$ - antisymmetry
• $\forall x \forall y \exists z (x \leq z \land y \leq z \land (\forall w (x \leq w \land y \leq w \to z \leq w)))$ - supremum
• $\forall x \forall y \exists z (z \leq x \land z \leq y \land (\forall w (w \leq x \land w \leq y \to w \leq z)))$ - infimum

I believe I've done the first 3 axioms right:

• reflexivity is the same
• $\forall x \forall y \forall z ((\sup(x, y) \leq \sup(y, z) \to y \leq z) \to x \leq z)$ - transitivity
• $\forall x \forall y (\sup(x, y) = \inf(x, y) \to x = y)$ - antisymmetry

I've stuck with supremum and infimum. I've thought about something like that:

• $\forall x \forall y \forall z (\sup(x, y) = z \to \forall w (x \leq w \land y \leq w \to z \leq w))$

But then again I should somehow get rid of conjunction. How can I do it?

Thank you.

Answer 1

It is easy to see that for any three formulas $\phi, \psi$ and $\theta$ the formula $\phi \to \psi \to \theta$ is equivalent to $\phi \land \psi \to \theta$ (where $\phi \to \psi \to \theta$ means $\phi \to (\psi \to \theta)$, i.e. $\to$ associates to the right).

Using this we can rewrite, for example, antisymmetry as

$$ \forall x \forall y (x \leq y \to y \leq x \to x =y) $$ and transitivity to $$ \forall x \forall y \forall z(x \leq y \to y \leq z \to x \leq z) $$

The supremum axiom would thus be, following your start attempt, written as $$ \forall x\forall y \forall z(\sup(x,y)=z \to \forall w(x \leq w \to y \leq w \to z \leq w)) $$ but you could simplify this by getting rid of the $z$ in the quantification if $\sup$ is a function symbol, i.e. you could state $$ \forall x\forall y \forall w(x \leq w \to y \leq w \to \sup(x,y) \leq w)) $$ but note that these to are not enough to characterize suprema on their own, you also need, for instance $$ \forall x\forall y (x \leq \sup(x,y)) $$ and $$ \forall x\forall y (y \leq \sup(x,y)). $$