User:Dfeuer/Properties of Heyting Algebras

Let $(L, \wedge, \vee, \preceq)$ be a Heyting algebra.

Let $x, y, z \in L$.

Then:

Lemma

$x \to y = \top \iff x \preceq y$

Proof

Suppose $x \preceq y$.

Then $x \land \top = x \preceq y$, so $x \to y = \top$.

Suppose $x \to y = \top$.

Then $x \land \top \preceq y$.

But $x \land \top = x$, so $x \preceq y$.

Thm 1

If $x \to y = top$ and $y \to x = \top$ then $x = y$.

Proof

We have $x \land \top \preceq y$ and $y \land \top \preceq x$.

Thus $x \preceq y$ and $y \preceq x$, so $x = y$.

Thm 2

If $\top \to x = \top$ then $x = \top$

Proof

We have $\top \land \top \preceq x$, so $\top \preceq x$, so $x = \top$.

Thm 3

$x \to (y \to x) = \top$

Proof

We will show that $x \preceq (y \to x)$. The theorem will then follow from the lemma.

We have that $y \to x$ is the greatest $z$ such that $y \land z \preceq x$.

But $y \land x \preceq x$ by the definition of meet, so $x \preceq z$.

That is, $x \preceq (y \to x)$.

Thm 4

$(x \to (y \to z)) \to ((x \to y) \to (x \to z)) = \top$

Proof

By the lemma, it is sufficient to show that:

$x \to (y \to z) \preceq (x \to y) \to (x \to z)$

By the definition of relative pseudocomplement, this is equivalent to showing that:

$(x \to (y \to z)) \land (x \to y) \preceq x \to z$

Let $m = (x \to (y \to z)) \land (x \to y)$.

By the definition of meet, $m \preceq x \to (y \to z)$ and $m \preceq x \to y$.

Then $m \land x \preceq y \to z$ and $m \land x \preceq y$.

Thus $m \land x \land y \preceq z$ and $m \land x \preceq y$.

Since $m \land x \preceq y$, $m \land x \land y = m \land x$.

Thus $m \land x \preceq z$.

By the definition of pseudocomplement, $m \preceq x \to z$.