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.

Rate this:

Like this:

Be the first to like this post.

This entry was posted in 閒聊. Bookmark the permalink.

4 Responses to An equational way to prove associativity of least upper bounds

recorriendo | November 26, 2011 at 4:39 pm |

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

最近念proof theory念得好辛苦~~
XOO | November 27, 2011 at 1:47 am |

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

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

嗯嗯，謝謝您的回應，所以你大學是念數學系的？台灣有哪個數學系有老師作邏輯/基礎方面的工作啊？據我所知好像都是哲學系的老師…
XOO | December 9, 2011 at 10:46 am |

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

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

S	M	T	W	T	F	S
« Jul
		1	2	3	4	5
6	7	8	9	10	11	12
13	14	15	16	17	18	19
20	21	22	23	24	25	26
27	28	29	30	31

An equational way to prove associativity of least upper bounds

Rate this:

Like this:

4 Responses to An equational way to prove associativity of least upper bounds

Leave a Reply Cancel reply

Archives

Follow “XOO's”