辞書式順序が完全律を満たすことを示す

takker.icon

$ \top

$ \implies\forall(x_1,x_2),(y_1,y_2)\in A_1\times A_2.(x_1\le_1y_1\lor y_1\le_1x_1)\land(x_2\le_2y_2\lor y_2\le_2x_2)

$ \forall(x_1,x_2),(y_1,y_2)\in A_1\times A_2.(x_1,x_2)\le_{1\times2}(y_1,y_2)\lor(y_1,y_2)\le_{1\times2}(x_1,x_2)

$ \iff\forall(x_1,x_2),(y_1,y_2)\in A_1\times A_2.x_1<_1y_1\lor(x_1=y_1\land x_2\le_2y_2)\lor y_1<_1x_1\lor(y_1=x_1\land y_2\le_2x_2)

$ \iff\forall(x_1,x_2),(y_1,y_2)\in A_1\times A_2.(x_1\le_1y_1\land(x_1<_1y_1\lor x_2\le_2y_2))\lor(y_1\le_1x_1\land(y_1<_1x_1\lor y_2\le_2x_2))

$ \iff\forall(x_1,x_2),(y_1,y_2)\in A_1\times A_2.(x_1\le_1y_1\land(x_1\le_1y_1\lor x_2\le_2y_2)\land(x_1\neq y_1\lor x_2\le_2y_2))\lor(y_1\le_1x_1\land(y_1\le_1x_1\lor y_2\le_2x_2)\land(y_1\neq x_1\lor y_2\le_2x_2))

$ \iff\forall(x_1,x_2),(y_1,y_2)\in A_1\times A_2.(x_1\le_1y_1\lor y_1\le_1x_1)\land(x_1\le_1y_1\lor y_1<_1x_1\lor y_2\le_2x_2)\land(x_1<_1y_1\lor x_2\le_2y_2\lor y_1\le_1x_1)\land(x_1<_1y_1\lor x_2\le_2y_2\lor y_1<_1x_1\lor y_2\le_2x_2)

こんがらがっちゃったtakker.icon

場合分けしたほうがいいかも

背理法なら一発で示せるだろうけど、あんまりやりたくないな

完全律を$ \forall x,y\in A. x>y\implies x\le yの形に変形すれば示せた

証明は明日書く

背理法なし(二重否定除去なし)で示す方法を探りたいけど、うまくいくかどうか……

場合わけ4つでいいんじゃないのnishio.icon

大なり、＊のとき、以上

イコール、以上のとき、以上

イコール、小なりのとき、小なり

小なり、＊のとき、小なり

(スマホなので表記が雑)

これで全パターン網羅してて、どのパターンでも条件を満たしてることが言える

清書

任意の全順序集合$ (A_1,\le_1),(A_2,\le_2)に対して、$ A_1\times A_2上の二項関係$ \le_{1\times2}を次のように定義する

$ (x_1,x_2)\le_{1\times 2}(y_1,y_2):\iff x_1<_1 y_1\lor(x_1=y_1\land x_2\le_2 y_2)

$ \forall x,y\in A_1\times A_2.x\le y\lor y\le xを示す

$ x = (x_1, x_2), y = (y_1, y_2)とする

場合わけ

(1): $ x_1\le_1 y_1でないとき

$ \le_1が全順序なので$ y_1<_1 x_1

よって$ y \le_{1\times 2} x

(2):$ x_1\le_1 y_1のとき

(2-1):$ x_1<_1 y_1のとき$ x \le_{1\times 2} y

(2-2):$ x_1 = y_1のとき

(2-2-1)$ x_2\le_1 y_2のとき$ x \le_{1\times 2} y

(2-2-2) $ x_2\le_1 y_2でないとき

$ \le_2が全順序なので$ y_2\le_2 x_2

よって$ y \le_{1\times 2} x

よって任意の$ x,y\in A_1\times A_2 について $ x\le y または $ y\le xである。 Q.E.D.

感想

現時点でScrapboxに書かれてる中には$ <の定義がない

$ x < y := (x \le y) \land (x\ne y)

$ x \not\le y \iff x > y

書き忘れてたtakker.icon

ありがとうございます。やはり場合分けが王道takker.icon

書き直しtakker.icon

場合分けルート

$ \top

$ \implies\forall(x_1,x_2),(y_1,y_2)\in A_1\times A_2.(x_1\le_1y_1\lor y_1\le_1x_1)\land(x_2\le_2y_2\lor y_2\le_2x_2)

$ \because完全律

$ \iff\forall(x_1,x_2),(y_1,y_2)\in A_1\times A_2.

$ (x_1\le_1y_1\land x_2\le_2y_2)

$ \lor(x_1\le_1y_1\land y_2\le_2x_2)

$ \lor(y_1\le_1x_1\land x_2\le_2y_2)

$ \lor(y_1\le_1x_1\land y_2\le_2x_2)

分配法則

$ \iff\forall(x_1,x_2),(y_1,y_2)\in A_1\times A_2.

$ (x_1<_1y_1\land x_2\le_2y_2)

$ \lor(x_1<_1y_1\land y_2\le_2x_2)

$ \lor(y_1<_1x_1\land x_2\le_2y_2)

$ \lor(y_1<_1x_1\land y_2\le_2x_2)

$ \lor(x_1=y_1\land x_2\le_2y_2)

$ \lor(x_1=y_1\land y_2\le_2x_2)

$ \lor(y_1=x_1\land x_2\le_2y_2)

$ \lor(y_1=x_1\land y_2\le_2x_2)

P⇒(P∧¬Q)∨Qと分配法則

$ \iff\forall(x_1,x_2),(y_1,y_2)\in A_1\times A_2.

$ (x_1<_1y_1\land x_2\le_2y_2)

$ \lor(x_1<_1y_1\land y_2\le_2x_2)

$ \lor(y_1<_1x_1\land x_2\le_2y_2)

$ \lor(y_1<_1x_1\land y_2\le_2x_2)

$ \lor(x_1=y_1\land x_2\le_2y_2)

$ \lor(y_1=x_1\land y_2\le_2x_2)

同じものを削った

$ \implies\forall(x_1,x_2),(y_1,y_2)\in A_1\times A_2.

$ (x_1<_1y_1)

$ \lor(y_1<_1x_1)

$ \lor(x_1=y_1\land x_2\le_2y_2)

$ \lor(y_1=x_1\land y_2\le_2x_2)

連言除去

$ \iff\forall(x_1,x_2),(y_1,y_2)\in A_1\times A_2.

$ (x_1,x_2)\le_{1\times2}(y_1,y_2)

$ \lor(y_1,y_2)\le_{1\times2}(x_1,x_2)

$ \lor(x_1,x_2)\le_{1\times2}(y_1,y_2)

$ \lor(y_1,y_2)\le_{1\times2}(x_1,x_2)

定義に沿って組み立てた

$ \underline{\iff\forall x,y\in A_1\times A_2.x\le_{1\times2}y\lor y\le_{1\times2}x\quad}_\blacksquare

二重否定除去を回避して証明するのはおそらく不可能takker.icon

場合分けで証明するさい、$ x_1<_1 y_1\lor x_1= y_1\implies x_1\le_1 y_1 という操作が必要

これは(P∧¬Q)∨Q⇒Pで示せる

しかし(P∧¬Q)∨Q⇒Pは二重否定除去を仮定しないと導出不能