I am doing a research in foundation of maths, especially in logic area. Right now, I am building a set $\mathbb{L}$ through this five axioms:
- Additive axiom: closeness, commutative, associative, 0 as identity, additive inverse.
- Multiplicative axiom: closeness, commutative, associative, 1 as identity, multiplicative inverse.
- Distributive axiom.
- Total partial order axiom: reflexive, transitivity, anti-symmetry, totality.
- Existence of positive infinitesimal.
As you might noticed already, axioms 1-4 are just like axioms in reals. The only addition in here is axiom 5, which make everything be much more complicated.
My problem for now is I want to prove that $\mathbb{L}$ is consistent and therefore, semantically, I need to provide a model for it. Can you help me with it? I have been thinking about this for weeks and still cannot come up with a right one. I thought $\mathbb{R}^\omega$ with a lexicographic order would be a right model, but unfortunately, I didn't think it is. Cheers!
What you are describing are precisely the non-Archimedean ordered fields. ("Non-Archimedean" refers to the existence of infinitesimals and infinite elements; the "ordered field" bit covers the rest.)
There are lots of these (e.g., continuum-many non-isomorphic countable examples). One way to construct them is via ultrapowers: fix a nonprincipal ultrafilter $\mathcal{U}$ on a set $I$, and let $$\prod_I\mathbb{R}/\mathcal{U}$$ be the set of maps $I\rightarrow \mathbb{R}$, thought of as $I$-length sequences of reals, modulo the equivalence relation $$(a_i)_{i\in I}\sim (b_i)_{i\in I}\iff \{i: a_i=b_i\}\in\mathcal{U}.$$ This is a set, and we can define an ordering $<$ and operations $+$ and $\times$ on it in the obvious way (we have to check that this is well-defined, but this is not hard and a good exercise). The resulting object is a non-Archimedean (since $\mathcal{U}$ is nonprincipal) ordered field.
In fact, the ordered field $\prod_I\mathbb{R}/\mathcal{U}$ is an elementary extension of the ordered field of real numbers; this is (an instance of) Los' Theorem. So, among other things, it is a real closed field, and its first-order theory is computable.
As far as examples of these things go: there are natural examples of non-Archimedean ordered fields, such as fields of power series (see e.g. https://en.wikipedia.org/wiki/Formal_power_series#Ring_structure).