# An equational way to prove associativity of least upper bounds

Traditionally, to prove the associativity of the least upper bounds, i.e. $x \vee (y \vee z) = (x \vee y) \vee z$ we need few lines to prove the inequality from the left hand side and conversely. However, by turning the definition of finit join to the adjunction form, we have a more compact and algebraic-like way to do it.

Let $P$ be a poset and $P^2$ be the Cartesian product with Cartesian order which is induced by the product diagram. Note $x \vee y \leq z$ if and only if $\langle x, y \rangle \leq \langle z, z \rangle$ where $z \in P, \langle x, y \rangle \in P^2$. Therefore $x \vee (y \vee z) \leq a \equiv \langle x, y \vee z \rangle \leq \langle a, a \rangle \equiv \langle x, \langle y, z \rangle \rangle \leq \langle a, \langle a, a \rangle \rangle \equiv \langle \langle x, y \rangle, z \rangle \leq \langle \langle a, a \rangle, a \rangle \equiv (x \vee y) \vee z \leq a$.  Finally, $(x \vee y) \vee z \leq a \equiv x \vee (y \vee z) \leq a$ for every $a$ implies $(x \vee y) \vee z = x \vee (y \vee z)$.

We can also prove some properties automatically from this form. To see $x \vee x = x$, just replace $\langle x, y \rangle$ with $\langle x, x \rangle$; to see $x \leq x \vee y$ replace $z$ with $x \vee y$ itself.

## 4 thoughts on “An equational way to prove associativity of least upper bounds”

1. recorriendo

請問您是在哪裡研究logic/theoretical computer science呢？我想朝這方面發展卻不知道哪裡在這方面的研究比較強 (好像歐洲作這方面的比美國多？)

最近念proof theory念得好辛苦~~

• 嗨，我在英國唸書。當初在台灣遇到從英國回來的老師，對這方面有所研究，反過來美系的都沒遇到，有興趣就前來英國唸了。歐洲方面做這方面的還滿多的。

純 proof theory 我也沒學過，我從比較實務的 functional programming 如 Haskell 跟 Agda 慢慢往 lambda calculus 跟 type theory 切入這方面，本身背景也是數學，學起來背後的數學理論比較習慣些。從能夠摸得到的東西開始總是比較容易一些。

2. recorriendo

嗯嗯，謝謝您的回應，所以你大學是念數學系的？台灣有哪個數學系有老師作邏輯/基礎方面的工作啊？據我所知好像都是哲學系的老師…

• 當初是數學跟資訊主修，但我想數學背景影響比較深遠。

至於第二個問題，我不清楚 …
東華的魏澤人似乎有在作 descriptive set theory，近日不曉得如何。當初在中研院的穆信成實驗室下跟了一年，相關的 functional programming 跟 dependent type theory 大概在那個時候接觸的。同時間認識蔡益坤老師有作 program verification 用到 finite model theory 還有 modal logic。但要說純數理邏輯或基礎的，我倒不曉得。