問：空でない有限全順序集合のHasse図が一直線上に並ぶことを示せ
from 論理と集合から始める数学の基礎 読書会
解いている途中で空集合だと成立しないことに気づいたので、タイトルに「空でない」を入れた
全順序の定義が「任意の元について〜」だから空でも成り立つのか…
念の為テキストとwikipediaの定義に「空でない」という但し書きがないか見てみましたが、なかったです。うせやろ
わざわざ証明するまででもなさそう
全順序の時一直線上に並ぶから何も言ってなさすぎてウケる
トートロジー()
一点に3本の線が集まることがないことを言う
最大値と最小値以外線が一本にならないことを言う
こんな感じ？
加えて直線が1本しかないことも言う
最大値と最小値以外線が一本にならないことを言う 端点が2つしかないので1本である
そうでした
よく考えたら、一直線上に並ぶってペアノの公理のことじゃん
有限であること以外ほぼ一緒
一直線上に並ぶことの証明がだるそうで飛ばしてたけど、ペアノの公理の類推から証明を組み立てるのならそんなに難しくなさそう
確かに一点に3本の線が集まることがないことを言うより「最大値以外には必ずただ一つの点が次にくる」の方が楽か
証明するぞ～
まずはペアノの公理を参考に、「一直線上に並ぶ」を論理式で実装する
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)
空でない有限全順序集合には必ず(最大元|最小元)が存在するので、\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)
\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)
\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))
悪手だ
おそらく無限降下列を示せばいけそうだが、論理式が大量にネストしそうでやりたくない
対偶の\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やれたら数学とアルゴリズムの経験値積めそうだけど、カロリーがとんでもなさそう
例えば数学記号でクイックソートを作らなければならなくなる
「次の一つを見つける」と「ソートする」では後者の方が格段に難しいので「クイックソートを作らねばならない」が変な気がする
xが最大値でないならより大きなyがある、それが直後であるなら終了、直後でないなら間の値zがあるわけだからそれをyとして再実行、このアルゴリズムは有限回で停止する、という流れ
厳密に言うのの難しさは度外視してる
(追記: そもそも存在することが言えればいいだけで、それを特定する必要はなかった、二人とも必要以上に問題を難しくしている)
あ
\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と同じ方法を使う
「毎ステップで選ばれる元は異なっているので集合の要素数以下のステップ数で終了する」
だけど、そもそも「存在する」を言いたいだけだったらステップを進める作業がいらない気がしてきた
古典論理で存在命題を証明する方法は二つ
2. \lnot\forall xP(x)から矛盾を示して背理法を適用する
他にはなかった……はず
「存在する」を言いたいだけは2に該当する
でもそんなことできるかな……
いやできるかも
x\neq\max U\land\lnot\exist y\in U.S(x,y)から矛盾を導けばいい
Aのほうがマシかな……
なんか謎に難しい話になってるな…
とりあえず一晩置こう
仕切り直し
\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
\because完全律
これ以降はステップ進める必要ありそう
\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の直後の要素にたどり着くまでステップ踏まないとだめかあ
→(A)
>ここまで解いてる
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
\because非反射律
\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)が得られる
あとは(1)を数学的帰納法で示せばいい
かなり回りくどいが、証明はできそうなのでこの方針でいく
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)
\because数学的帰納法
\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
\because完全律
\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
\because鳩の巣原理
\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)
\because反射律
\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)
\because反射律
\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
ちょっとまって。おかしいぞ
半順序集合なら分岐も合流も可能
全順序集合になって初めて分岐・合流不能になる
にも関わらず、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)が成立してしまい、非常に面倒な場合分けが生じてしまう