2 Model Theory and The Rest of Mathlib
2.1 Instances
Mathlib already contains a proof for the categoricity of the theory of dense linear orders without end points but it is written in terms of various instances such as ‘DenselyOrdered‘. In this section, we produce these instances for a ‘FirstOrder.Language.Order‘ structure.
Any structure of the language of orders is an ordered set.
The structure induced from \(\le \) which is induced from another structure is equal to the original structure.
By definition, the binary relation \(\le \) is equal to the interpretation of the unique binary relation symbol of the language ‘Language.order‘.
Models of the theory of dense linear orders without end points are preorders.
Models of the theory of dense linear orders without end points are partial orders.
Models of the theory of dense linear orders without end points are linear orders.
Models of the theory of dense linear orders without end points do not have a bottom element.
Models of the theory of dense linear orders without end points do not have a minimum element.
Models of the theory of dense linear orders without end points do not have a top element.
Models of the theory of dense linear orders without end points do not have a maximum element.
Models of the theory of dense linear orders without end points are densely ordered.
2.2 Homomorphisms
We also need to show that maps respecting the order structure are homomorphisms in the model theoretic sense.
A function which is an order embedding is also an embedding in the model theoretic sense.
A function which is an order isomorphism is also an isomorphism in the model theoretic sense.