I am trying to prove that given some bounded lattice $(L, \vee, \wedge, \top, \bot)$, where $(L, \leq )$ is a totally ordered set with \begin{align} a \leq b : a \wedge b = a \end{align} Implies that $L$ is a Heyting algebra with the Heyting implication \begin{align} a \rightarrow b = \left\{ \begin{array}{l l} \top & \quad a\leq b\\ b & \quad \text{else} \end{array} \right. \end{align} I figured that in order to prove it I need to prove that the implication satisfies

\begin{align} (x \wedge a) \leq b \Leftrightarrow x \leq ( a \rightarrow b) \end{align} However I seem to get stuck.

  • $\begingroup$ Of course you are absolutely right. I am trying to prove it in coq, so I guess my mind was on a different level. If you create a answer I would be delighted to mark it. $\endgroup$ – budde Mar 21 '14 at 20:20
  • $\begingroup$ Okay, I'll change my comment to an answer, so the question can be marked answered. By the way, I recently started learning Coq, so if you implement this proof, could you share it? Thanks! $\endgroup$ – William DeMeo Mar 23 '14 at 15:33
  • $\begingroup$ I will do that :) $\endgroup$ – budde Mar 24 '14 at 7:52

You are right, according to the definition of Heyting algebra, you must check that the $\Leftrightarrow$ in your last displayed equation holds. This follows from the fact that your lattice is totally ordered, arguing by cases.

For example, suppose $x\wedge a \leq b$.

If $a\leq b$, then $a \rightarrow b$ is top, so it is certainly above $x$. If not $a \leq b$, then, since the lattice is totally ordered, $b< a$. This and $x\wedge a \leq b$ imply that $x$ is below $b$, hence $x \leq (a \rightarrow b)$ in this case.

The $\Leftarrow$ direction is similar.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.