1 Basic Definitions and Lemmas
1.1 Vectors
For any vector \(v : \operatorname{Fin}2 \to X\), we have \(v = ![v(0), v(1)]\).
For any function \(f : X \to Y\) and elements \(x_1, x_2 \in X\), we have \(f \circ ![x_1, x_2] = ![f(x_1), f(x_2)]\).
1.2 Theories
The theory of dense linear orders contains the reflexive sentence.
The theory of dense linear orders without end points contains the transitive sentence.
The theory of dense linear orders without end points contains the antisymmetric sentence.
The theory of dense linear orders without end points contains the total sentence.
The theory of dense linear orders without end points contains the no bottom element sentence.
The theory of dense linear orders without end points contains the no top element sentence.
The theory of dense linear orders without end points contains the densely ordered sentence.
Models of the theory of dense linear orders without end points satisfies the no bottom element sentence.
Models of the theory of dense linear orders without end points satisfies the no top element sentence.
Models of the theory of dense linear orders without end points satisfies the densely ordered sentence.