The situation:
An algebraic semilattice $(L, \wedge, \top)$ satisfies the following axioms:
- $\forall x \in L. x \wedge \top = x$
- $\forall x, y \in L. x \wedge y = y \wedge x$
- $\forall x, y, z \in L. (x \wedge y) \wedge z = x \wedge (y \wedge z)$
- $\forall x \in L. x \wedge x = x$
A Heyting semilattice can be defined in two equivalent ways. However, the proof that these definitions are the same is given as an exercise in every book I've read, and I can't figure it out (I'm surely missing something obvious, but I'm stuck).
Definition 1: equational definition.
There is an operation $\implies : L^2 \to L$ satisfying the following axioms:
- $\forall x \in L. (x \implies x) = \top$
- $\forall x, y \in L. x \wedge (x \implies y) = x \wedge y$
- $\forall x, y \in L. y \wedge (x \implies y) = y$
- $\forall x, y, z \in L. x \implies (y \wedge z) = (x \implies y) \wedge (x \implies z)$
Definition 2: order definition.
Define the following partial order on $L$:
$\forall x, y \in L. x \le y$ if and only if $x = x \wedge y$
There is an operation $\implies : L^2 \to L$ such that:
$\forall x, y, z \in L. x \wedge y \le z$ if and only if $x \le (y \implies z)$
Does anyone know where I can find a worked-out proof of this result?
Let us give names to the axioms, for reference.
$H$ stands for Heyting.
$(H_0)$ $x\wedge y \leq z \Leftrightarrow x \leq y \to z$.
$(H_1)$ $x\to x = 1$,
$(H_2)$ $x \wedge (x\to y) = x \wedge y$,
$(H_3)$ $(x\to y) \wedge y = y$,
$(H_4)$ $x \to (y \wedge x) = (x\to y) \wedge (x\to z)$.
We want to prove that a $\wedge$-semilattice $H$ with $1$ satisfies $(H_0)$ iff it satisfies $(H_1)-(H_4)$.
Suppose it satisfies $(H_0)$. Then, for every $a,b \in H$, $$a \wedge b \leq b \Rightarrow a \leq b \to b.$$ In particular this is true for $a=1$, and so $H$ satisfies $(H_1)$.
For $a,b,c \in H$, from $$a \to b \leq a \to b$$ we get from $(H_0)$ that $$a \wedge (a\to b) \leq b;$$ certainly $a \wedge (a\to b) \leq a$, whence $a \wedge (a\to b) \leq a\wedge b$. Conversely, from $$a \wedge b = (a \wedge b) \wedge a \leq b,$$ we obtain $$a \wedge b \leq a \to b;$$ since $a \wedge b \leq a$, it follows that $a \wedge (a\to b) = a\wedge b$, and $H$ satisfies $(H_2)$.
The verification of $(H_3)$ is easier: one inequality is obvious, and the other follows from two applications of $(H_0)$ and equations of semilattices.
To prove $(H_4)$, let $a,b,c \in H$, and use $(H_2)$ to get $$a \wedge (a \to b) = a \wedge b \leq b$$ and $$a \wedge (a \to c) = a \wedge c \leq c,$$ whence $$a \wedge (a\to b) \wedge (a\to c) \leq b \wedge c$$ and from $(H_0)$, $$(a\to b) \wedge (a\to c) \leq a \to (b \wedge c).$$ For the converse, observe first that $\to$ is order-preserving in the second coordinate:
indeed, if $u \leq v$, then $$x \wedge u \leq v$$ and from $(H_2)$, $$(x\to u) \wedge x \leq v$$ and from $(H_0)$, $$x \to u \leq x \to v.$$ Now it follows that $$a \to (b \wedge c) \leq a \to b,$$ since $b \wedge c \leq b$ and similarly $a \to (b \wedge c) \leq a \to c$, whence $$(a\to b) \wedge (a\to c) = a \to (b \wedge c),$$ that is, $H$ satisfies $(H_4)$.
Now we must prove that $H$ satisfies $(H_0)$, whenever it satisfies $(H_1)-(H_4)$.
Start with noting that from $(H_4)$ it follows that $\to$ is, again, order-preserving in the second coordinate (I'll leave that to you).
Let $a,b,c \in H$. If $a \leq b \to c$, then $$a \wedge b \leq b \wedge (b \to c) = b \wedge c \leq c.$$ Conversely, if $a \wedge b \leq c$ then $$b \to (a \wedge b) \leq b \to c,$$ and the result follows from the fact that $$a = a \wedge (b \to a),$$ whence $$a \leq b \to a = (b \to a) \wedge (b \to b) = b \to (a \wedge b).$$ (It is not difficult to find which axiom is used in each step.)