Express lattice axioms using implication and universal quantification 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.
 A: 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)).
$$
