狭義順序
$ \leに対する$ <のこと
等号が成立しなくなる
代わりに同値関係を使う
仮に作るとしたら$ \begin{dcases}\forall a\in X:\lnot(a<a)\\\forall a,b,c\in X:a<b<c\implies a<c\end{dcases}だが、これは狭義半順序となってしまう 作れる
$ a<b:\iff a\le b\land a\neq b
ただし$ a\le b\iff a<b\lor a\neq bが成立しなくなる
混乱を避けるため、擬順序では$ \leではなく$ \lesssimなど、等号ではないことを暗示する記号を使ったほうがいい 性質
(三分律)$ \forall a,b\in X:a<b\veebar b<a\veebar a=b $ \begin{dcases}\forall a,b\in X:a\le b\iff a<b\lor a=b\\<\text{は狭義全順序}\end{dcases}\iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\le\text{は全順序}\end{dcases}
証明
$ \begin{dcases}\forall a,b\in X:a\le b\iff a<b\lor a=b\\<\text{は狭義全順序}\end{dcases}
$ \iff\begin{dcases}\forall a,b\in X:a\le b\iff a<b\lor a=b\\<\text{は狭義半順序}\\\forall a,b\in X:a<b\veebar b<a\veebar a=b\end{dcases}
$ \iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\le\text{は半順序}\\\forall a,b\in X:a<b\veebar b<a\veebar a=b\end{dcases}
$ \iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\le\text{は半順序}\\\forall a,b\in X:(a\le b\land a\neq b)\veebar(b\le a\land a\neq b)\veebar a=b\end{dcases}
$ \iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\le\text{は半順序}\\\forall a,b\in X:(a\le b\land a\neq b)\veebar((b\le a\land a\neq b\land a\neq b)\lor((\lnot(b\le a)\lor a=b)\land a=b))\end{dcases}
$ \iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\le\text{は半順序}\\\forall a,b\in X:(a\le b\land a\neq b)\veebar((b\le a\land a\neq b)\lor a=b)\end{dcases}
$ \iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\le\text{は半順序}\\\forall a,b\in X:(a\le b\land a\neq b)\veebar(b\le a\lor a=b)\end{dcases}
$ \iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\le\text{は半順序}\\\forall a,b\in X:(a\le b\land a\neq b)\veebar b\le a\end{dcases}
$ \because\forall a\in X:a\le a
$ \iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\le\text{は半順序}\\\forall a,b\in X:(a\le b\land a\neq b\land\lnot(b\le a))\lor((\lnot(a\le b)\lor a=b)\land b\le a)\end{dcases}
$ \iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\le\text{は半順序}\\\forall a,b\in X:(a\le b\land a\neq b\land\lnot(b\le a))\lor((\lnot(a\le b)\land b\le a)\lor b\le a)\end{dcases}
$ \iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\le\text{は半順序}\\\forall a,b\in X:(a\le b\land a\neq b\land\lnot(b\le a))\lor b\le a\end{dcases}
$ \iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\le\text{は半順序}\\\forall a,b\in X:(a\le b\lor b\le a)\land(a\neq b\lor b\le a)\end{dcases}
$ \iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\le\text{は半順序}\\\forall a,b\in X:(a\le b\lor b\le a)\land(a=b\implies b\le a)\end{dcases}
$ \iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\le\text{は半順序}\\\forall a,b\in X:a\le b\lor b\le a\end{dcases}
$ \because\forall a\in X:a\le a
$ \underline{\iff\begin{dcases}\forall a,b\in X:a< b\iff a\le b\land a\neq b\\\le\text{は全順序}\end{dcases}\quad}_\blacksquare