# Equivalence of definitions of Heyting Algebra

I encountered the following problem in Burris' A Course in Universal Algebra:

If $$\langle H,\vee,\wedge,\rightarrow,0,1\rangle$$ is a Heyting algebra and $$a,b\in H$$ show that $$a\rightarrow b$$ is the largest element $$c$$ of $$H$$ such that $$a\wedge c\leq b$$.

The definition given for a Heyting algebra is a distributive bounded lattice with a binary operation $$\rightarrow$$ where the following hold:

1. $$x\rightarrow x=1$$,
2. $$(x\rightarrow y)\wedge y=y$$,
3. $$x\wedge (x\to y)=x\wedge y$$,
4. $$x\to (y\wedge z)=(x\to y)\wedge(x\to z)$$,
5. $$(x\vee y)\to z=(x\to z)\wedge(y\to z)$$.

It is clear that $$(a\to b)\wedge a=a\wedge b\leq b$$, but if $$x\wedge a\leq b$$ I am struggling to show that $$x\leq a\to b$$. I want to manipulate $$x\wedge (a\to b)$$ to $$x$$, but I cannot seem to find any way to do this.

For example I tried $$x\wedge (a\to b)=x\wedge(a\to((x\wedge a)\vee b))=x\wedge (a\to((x\vee b)\wedge(a\vee b)))\\=x\wedge((a\to(x\vee b))\wedge(a\to(a\vee b))),$$ and I get stuck. I figure $$a\to(a\vee b)$$ ought to be $$1$$ (which I cannot show), which would give me $$x\wedge(a\to (x\vee b))$$, which I don't know what to do with. Any help would be greatly appreciated.

From (4) you get immediately that $$y \leq z \Rightarrow x\to y \leq x\to z,$$ whence $$$$x\wedge a \leq b \Rightarrow a\to (x\wedge a) \leq a\to b. \tag{*}$$$$ Now, \begin{align} x &\leq a \to x \tag{by (2)}\\ &= (a\to x) \wedge (a\to a) \tag{by (1)}\\ &= a \to (x \wedge a) \tag{by (4)}\\ &\leq a \to b. \tag{by (*)} \end{align} I think that the first observation (that $$\to$$ is order preserving in the second coordinate) is the main trick here.