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. 請問您是在哪裡研究logic/theoretical computer science呢?我想朝這方面發展卻不知道哪裡在這方面的研究比較強 (好像歐洲作這方面的比美國多?)

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

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

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

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

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

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

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s