問：空でない有限全順序集合のHasse図が一直線上に並ぶことを示せ
解いている途中で空集合だと成立しないことに気づいたので、タイトルに「空でない」を入れたtakker.icon
全順序の定義が「任意の元について〜」だから空でも成り立つのか…nishio.icon
念の為テキストとwikipediaの定義に「空でない」という但し書きがないか見てみましたが、なかったです。うせやろtakker.icon
わざわざ証明するまででもなさそう
全順序の時一直線上に並ぶから何も言ってなさすぎてウケるnishio.icon
一点に3本の線が集まることがないことを言う
最大値と最小値以外線が一本にならないことを言う
こんな感じ？
加えて直線が1本しかないことも言うtakker.icon
最大値と最小値以外線が一本にならないことを言う 端点が2つしかないので1本であるnishio.icon
そうでしたtakker.icon
よく考えたら、一直線上に並ぶってペアノの公理のことじゃんtakker.icon 有限であること以外ほぼ一緒
一直線上に並ぶことの証明がだるそうで飛ばしてたけど、ペアノの公理の類推から証明を組み立てるのならそんなに難しくなさそう 確かに一点に3本の線が集まることがないことを言うより「最大値以外には必ずただ一つの点が次にくる」の方が楽かnishio.icon
証明するぞ～takker.icon
まずはペアノの公理を参考に、「一直線上に並ぶ」を論理式で実装する 「Hasse図にて$ aの次に$ bがくる」という関係を$ S(a,b)で定義しておく $ S(a,b):\iff a< b\land\forall x\in U.(a\le x\le b\implies a=x\lor x=b)
1. 分岐の禁止$ \forall x,y,z\in U.S(x,y)\land S(x,z)\implies y=z
2. 合流の禁止$ \forall x,y\in U.S(x,z)\land(y,z)\implies x=y
3. 最大元以外は次がある$ \forall x\in U.(\lnot\exist y\in U.S(x,y)\implies x=\max U)
ちなみにここで最大元の存在を使ったので、「有限全順序集合のHasse図が一直線上に並ぶ」ではなく「空でない有限全順序集合のHasse図が一直線上に並ぶ」しか示せないことになる
まあ空集合は並べるもなにもないか……
4. ループの禁止$ \forall x\in U.\lnot S(x,\min U)
1~4を証明できれば、題意を示せる
証明
1. $ \forall x,y,z\in U.
$ S(x,y)\land S(x,z)
$ \iff x< y\land x< z\land\forall u\in U.(x\le u\le y\implies x=u\lor u=y)\land\forall u\in U.(x\le u\le z\implies x=u\lor u=z)
$ \implies x< y\land x< z\land(x\le z\le y\implies x=z\lor z=y)\land(x\le y\le z\implies x=y\lor y=z)
$ \because前者に$ u=z、後者に$ u=yを代入
$ \implies (x\le y\le z\lor x\le z\le y)\land(x\le z\le y\implies z=y)\land(x\le y\le z\implies y=z)
$ \because完全律と$ x\neq y\land x\neq zを適用 $ \implies y=z
$ \because$ \lor除去
$ \underline{\therefore\forall x,y,z\in U.S(x,y)\land S(x,z)\implies y=z\quad}_\blacksquare
2. $ \forall x,y,z\in U.
$ \iff x<z\land y<z\land\forall u\in U.(x\le u\le z\implies x=u\lor u=z)\land\forall u\in U.(y\le u\le z\implies y=u\lor u=z)
$ \implies x< z\land y< z\land(x\le y\le z\implies x=y\lor y=z)\land(y\le x\le z\implies y=x\lor x=z)
$ \because前者に$ u=y、後者に$ u=xを代入
$ \implies (x\le y\le z\lor y\le x\le z)\land(x\le y\le z\implies x=y)\land(y\le x\le z\implies y=x)
$ \because完全律と$ x\neq z\land y\neq zを適用 $ \implies x=y
$ \because$ \lor除去
$ \underline{\therefore\forall x,y,z\in U.S(x,z)\land S(y,z)\implies x=y\quad}_\blacksquare
3. $ \forall x\in U.
$ \lnot\exist y\in U.S(x,y)
$ \iff\forall y\in U.\lnot S(x,y)
$ \iff\forall y\in U. (x<y\implies\lnot\forall u\in U.(x\le u\le y\implies x=u\lor u=y))
$ \iff\forall y\in U. (x<y\implies\exist u\in U.(x\le u\le y\land x\neq u\land u\neq y))
$ \iff\forall y\in U. (x<y\implies\exist u\in U.(x< u< y))
悪手だtakker.icon
おそらく無限降下列を示せばいけそうだが、論理式が大量にネストしそうでやりたくない 対偶の$ \forall x\in U.(x\neq\max U\implies\exist y\in U.S(x,y))を示そう
うーん？まって。これ相当ややこしいぞ
$ Uの有限性を使うのは確定
$ \phi:[1..n]⤖U で数え上げる
方針
A. $ \forall y\in U. (x<y\implies\exist u\in U.(x< u< y))で作った$ uを繰り返し$ yに代入し、$ uにできる要素を取り尽くすことで矛盾を導く
無限降下列$ u_0,u_1,\cdotsが存在しないことを示す
B. $ Uから$ xの後者にくる要素を検索する
何らかのソート・アルゴリズムを用いて全単射な単調写像$ \varphi:[1..n]⤖U を作成し、$ \varphi^{-1}(x)<\varphi^{-1}(\max U)であることを示して$ \exist y\in U.S(x,y)を導く $ \varphi^{-1}(x)+1を$ yに採用する
Bやれたら数学とアルゴリズムの経験値積めそうだけど、カロリーがとんでもなさそう
「次の一つを見つける」と「ソートする」では後者の方が格段に難しいので「クイックソートを作らねばならない」が変な気がするnishio.icon
xが最大値でないならより大きなyがある、それが直後であるなら終了、直後でないなら間の値zがあるわけだからそれをyとして再実行、このアルゴリズムは有限回で停止する、という流れ
厳密に言うのの難しさは度外視してる
(追記: そもそも存在することが言えればいいだけで、それを特定する必要はなかった、二人とも必要以上に問題を難しくしている)
あtakker.icon
$ \lnot(x=\max U)\iff\lnot\forall m\in U. m\le x\underset{\text{完全律}}{\iff}\exist m\in U. x< m
ほんとだ、$ x<mとなる要素はすぐ求まるのか
あとは$ \forall u\in U.(x\le u\le n\implies x=u\lor n=u)を示せればいい
このアルゴリズムは有限回で停止することを示す必要がある
$ m=nなら終了
$ m\neq nなら$ mを足がかりに、$ xのすぐ後にある$ nまで戻す
Aと同じ方法を使う
「毎ステップで選ばれる元は異なっているので集合の要素数以下のステップ数で終了する」nishio.icon
だけど、そもそも「存在する」を言いたいだけだったらステップを進める作業がいらない気がしてきた
古典論理で存在命題を証明する方法は二つtakker.icon
1. 特定の値$ tで成り立つ($ P(t))ことを示して存在導入($ P(t)\vdash\exist xP(x))する 2. $ \lnot\forall xP(x)から矛盾を示して背理法を適用する 他にはなかった……はず
「存在する」を言いたいだけは2に該当する
でもそんなことできるかな……
いやできるかも
$ x\neq\max U\land\lnot\exist y\in U.S(x,y)から矛盾を導けばいい
Aのほうがマシかな……
なんか謎に難しい話になってるな…nishio.icon
takker.iconがもっと簡単な定式化に気づいてない可能性もあるtakker.icon
とりあえず一晩置こう
仕切り直し
$ \forall x\in U.(x\neq\max U\implies\exist y\in U.S(x,y))案
$ \forall x\in U.
$ \lnot(x=\max U)
$ \iff\lnot\forall m\in U. m\le x
$ \implies\exist m\in U. x< m
nishio.iconさん助言より気付いた展開
これ以降はステップ進める必要ありそうtakker.icon
$ \forall x\in U.(x\neq\max U\land\lnot\exist y\in U.S(x,y)\implies\bot)(背理法)案
$ \forall x\in U.
$ \lnot(x=\max U)\land\lnot\exist y\in U.S(x,y)
$ \iff\begin{dcases}\exist m\in U.x<m\\\forall y\in U. (x<y\implies\exist u\in U.(x< u< y))\end{dcases}
$ \iff\exist m_0\in U\begin{dcases}x<m_0\\\exist m_1\in U.(x<m_1<m_0)\\\forall y\in U. (x<y\implies\exist u\in U.(x< u< y))\end{dcases}
背理法使う場合でも、結局$ xの直後の要素にたどり着くまでステップ踏まないとだめかあtakker.icon
→(A)
ここまで解いてるtakker.icon
4.
これは簡単だからやっておこう
$ \forall x\in U.
$ S(x,\min U)
$ \implies x<\min U
$ \implies \exist m\in U.x < m\land\forall u\in U. m\le u
$ \implies\exist m\in U. x<m\le x
$ \implies\bot
$ \underline{\therefore\forall x\in U.\lnot S(x,\min U)\quad}_\blacksquare
ちなみにこの結果から、最小元が存在する前順序集合をHasse図にしたとき、最小元には戻らないことがわかる
(A)背理法で解く
途中でステップを進める作業が出てくる
数ステップ進めて、数学的帰納法を適用する述語$ P(n)を特定する
$ \forall x\in U.
$ \lnot(x=\max U)\land\lnot\exist y\in U.S(x,y)
$ \iff\begin{dcases}\exist m\in U.x<m\\\forall y\in U. (x<y\implies\exist u\in U.(x< u< y))\end{dcases}
$ \iff\exist m_0\in U\begin{dcases}x<m_0\\\exist m_1\in U.(x<m_1<m_0)\\\forall y\in U. (x<y\implies\exist u\in U.(x< u< y))\end{dcases}
$ \iff\exist m_0,m_1\in U\begin{dcases}x<m_1<m_0\\\forall y\in U. (x<y\implies\exist u\in U.(x< u< y))\end{dcases}
$ \iff\exist m_0,m_1,m_2\in U\begin{dcases}x<m_2<m_1<m_0\\\forall y\in U. (x<y\implies\exist u\in U.(x< u< y))\end{dcases}
$ \iff\exist m_0,m_1,m_2,m_3\in U\begin{dcases}x<m_3<m_2<m_1<m_0\\\forall y\in U. (x<y\implies\exist u\in U.(x< u< y))\end{dcases}
$ \cdots
$ \implies\forall n\in\N\exist m:[1..n]\to U\forall i\le n\forall j<i.x<m_i<m_j ー(1)
このあとの展開
$ \forall i\le n\forall j<i.x<m_i<m_jから$ m_\bulletの単射性を示せるはず
$ U は有限集合だから$ \exist l\in\N\exist\phi:[1..l]⤖U が成立
(1)に$ n=l+1 を代入して$ m_\bullet:[1..l+1]\rightarrowtail U を得る
単射を$ \rightarrowtailと表している
これと$ \phi:[1..l]⤖U より単射$ \phi^{-1}(m_\bullet):[1..l+1]\rightarrowtail[1..l] を得る
以上より$ \forall x\in U.(x\neq\max U\land\lnot\exist y\in U.S(x,y)\implies\bot)が得られる
かなり回りくどいが、証明はできそうなのでこの方針でいくtakker.icon
refactoringは後でやればいい
証明
$ \forall x\in U.
$ \lnot(x=\max U)\land\lnot\exist y\in U.S(x,y)
$ \iff\begin{dcases}\exist m_1\in U.x<m_1\\\forall y\in U. (x<y\implies\exist u\in U.(x< u< y))\end{dcases}
$ \iff\begin{dcases}\exist m_1,m_2\in U.(x<m_2<m_1)\\\forall y\in U. (x<y\implies\exist u\in U.(x< u< y))\end{dcases}
$ \iff\begin{dcases}\exist m:[1..2]\to U\forall i\le 2\forall j<i.x<m_i<m_j\\\forall y\in U. (x<y\implies\exist u\in U.(x< u< y))\end{dcases}
$ \iff\begin{dcases}P(2)\\\forall y\in U. (x<y\implies\exist u\in U.(x< u< y))\end{dcases}
$ P(n):\iff\exist m:[1..n]\to U\forall i\le n\forall j<i.x<m_i<m_j とした
$ \iff\begin{dcases}P(2)\\\forall y\in U. (x<y\implies\exist u\in U.(x< u< y))\\\forall n\ge2.\end{dcases}
$ P(n)
$ \iff\exist m:[1..n]\to U\forall i\le n\forall j<i.x<m_i<m_j
$ \iff\exist m:[1..n]\to U\forall i\le n\begin{dcases}\forall j<i.x<m_i<m_j\\\exist u\in U.(x<u<m_i)\end{dcases}
$ \because\forall y\in U. (x<y\implies\exist u\in U.(x< u< y))
$ \iff\exist m:[1..n+1]\to U\forall i\le n+1\forall j<i.x<m_i<m_j
$ m_{n+1}に$ uを割り当てた
$ \iff P(n+1)
$ \implies\begin{dcases}P(2)\\\forall n\ge2.(P(n)\implies P(n+1))\end{dcases}
$ \implies\forall n\ge2.P(n)
$ \iff\forall n\ge2\exist m:[1..n]\to U\forall i\le n\forall j<i.x<m_i<m_j
$ \implies\forall n\ge2\exist m:[1..n]\to U\forall i,j\in[1..n].
$ m_i=m_j
$ \iff \lnot(m_i<m_j)\land m_i=m_j
$ \implies\lnot(j<i)\land m_i=m_j
$ \because\forall i\le n\forall j<i.x<m_i<m_jの対偶
$ \iff(\lnot(j\le i)\lor j=i)\land m_i=m_j
$ \implies (i\le j\lor i=j)\land m_i=m_j
$ \iff (i<j\lor i=j)\land m_i=m_j
$ \implies(m_j<m_i\lor i=j)\land m_i=m_j
$ \because\forall i\le n\forall j<i.x<m_i<m_jの$ iに$ jを、$ jに$ iを代入
$ \implies i=j
$ \implies\forall n\ge2\exist m:[1..n]\to U\forall i,j\in[1..n].(m_i=m_j\implies i=j)
$ \iff \forall n\ge2\exist m:[1..n]\rightarrowtail U
$ \iff\begin{dcases}\forall n\ge2\exist m:[1..n]\rightarrowtail U\\\exist n\in\N\exist\phi:[1..n]⤖U\end{dcases}
$ \because Uは有限集合
$ \implies\exist n\in\N\exist\phi:[1..n]⤖U\exist m:[1..n+1]\rightarrowtail U
$ \implies\exist n\in\N\exist\psi:[1..n+1]\rightarrowtail[1..n]
$ \phi^{-1}\circ mを$ \psiと置いた
$ \implies\bot
$ \implies\forall x\in U.\lnot(\exist y\in U.S(x,y)\land\lnot x=\max U)
$ \underline{\iff\forall x\in U.(\lnot\exist y\in U.S(x,y)\implies x=\max U)\quad}_\blacksquare
証明(失敗)
1. $ \forall x,y,z\in U.
$ S(x,y)\land S(x,z)
$ \iff x\le y\land x\le z\land\forall u\in U.(x\le u\le y\implies x=u\lor u=y)\land\forall u\in U.(x\le u\le z\implies x=u\lor u=z)
$ \implies x\le y\land x\le z\land(x\le x\le y\implies x=x\lor x=y)\land(x\le x\le z\implies x=x\lor x=z)
$ \because u=xを代入
$ \implies x\le y\land x\le z\land(x\le y\implies x=y)\land(x\le z\implies x=z)
$ \implies x=y\land x=z
$ \implies y=z
$ \underline{\therefore\forall x,y,z\in U.S(x,y)\land S(x,z)\implies y=z\quad}_\blacksquare
2. $ \forall x,y,z\in U.
$ S(x,z)\land S(y,z)
$ \iff x\le z\land y\le z\land\forall u\in U.(x\le u\le z\implies x=u\lor u=z)\land\forall u\in U.(y\le u\le z\implies y=u\lor u=z)
$ \implies x\le z\land y\le z\land(x\le z\le z\implies x=z\lor z=z)\land(y\le z\le z\implies y=z\lor z=z)
$ \because u=zを代入
$ \implies x\le z\land y\le z\land(x\le z\implies x=z)\land(y\le z\implies y=z)
$ \implies x=z\land y=z
$ \implies x=y
$ \underline{\therefore\forall x,y,z\in U.S(x,z)\land S(y,z)\implies x=y\quad}_\blacksquare
ちょっとまって。おかしいぞtakker.icon
半順序集合なら分岐も合流も可能
全順序集合になって初めて分岐・合流不能になる
にも関わらず、1,2を反射律のみで証明してしまった
これでは半順序集合でも分岐・合流不可になってしまう！
あ……$ x=x\lor x=y\implies x=yしてた……
正：$ x=x\le x=y\iff\top
仕切り直し！！
そもそも$ S(a,b)の定義を間違えていた
誤$ S(a,b):\iff a\le b\land\forall x\in U.(a\le x\le b\implies a=x\lor x=b)
正$ S(a,b):\iff a< b\land\forall x\in U.(a\le x\le b\implies a=x\lor x=b)
「誤」だと、反射律$ \forall x\in U. S(x,x)が成立してしまい、非常に面倒な場合分けが生じてしまう