Creating the first infinitesimal by use of Compactness Theorem I would like any feedback on the soundness and form of this proof. Please excuse any idiosyncrasies due to the fact that I am self-taught.
Setup and Proof
Consider a language $\mathcal{L}$ which, apart all the first-order logic apparatus, it also has:


*

*two binary operator symbols $\hat{+}$ and $\hat{\times}$ (which will represent addition and multiplication) 

*a unary operator $\iota$ (which will represent the multiplicative inverse operator)

*binary relation symbol $\hat{<}$

*a countable set of distinguished element symbols $\left\{\hat{n}_i\right\}_{i\in\mathbb{N}}$  (which will represent all the non-negative integers) 

*Crucially a last distinguished element symbol $\hat{\partial}$, which, if the proof is correct, will represent the "first" infinitesimal.


The binary operators, binary relation and the two symbols $\hat{n}_0$ and $\hat{n}_1$ allow $\mathcal{L}$ to talk about ordered fields. The rest of the symbols are for the statement of the axioms.
The $\mathcal{L}$-theory I am looking to satisfy is a set $T =  R \cup  N \cup H$ where: 


*

*$R$ is the finite set of sentences which would require the underlying set of a model for $T$ to be a totally ordered field, with $\hat{n}_0$ and $\hat{n}_1$ being the additive and multiplicative identities respectively,

*$N = \{\hat{n}_{i+1} = \hat{n}_{i} + \hat{n}_{1}\}_{i\in\mathbb{N}}$

*$H = \left\{ \phi_i \right\}_{i\in\mathbb{N}}$ is a countable set of sentences involving $\hat{\partial}$.  Specifically:


$$\begin{align}
\phi_0 &= \hat{n}_{0} < \hat{\partial}\\
\phi_i &= \hat{\partial} < \iota(\hat{n}_i) \phantom{ejfnkjefb}\mbox{for $i\geq1$ }
\end{align}$$ 
Proposition
The theory $T$ is satisfiable.
Proof
$R \cup N$ is trivially satisfiable by a model with $\mathbb{R}$ as an underlying set for example. Furthermore, any theory $R \cup N \cup J$ , where $J$ is any finite subset of $H$ is satisfiable since it suffices to map $\hat{\partial}$ to the inverse of the successor of the largest index of the $\phi_i$ in $J$ . Thus by the Compactness Theorem, $T$ is also satisfiable.
Comment on the proof
Adding the axioms $N$ felt a little unnatural, but I wanted to be able to talk about $\partial$ being smaller than any of the elements of $1, 1/2, 1/3, 1/4 \dots$
Context
I am reading a very interesting book by Lakoff and Nunez called Where Mathematics Comes From, interested in the neural and cognitive origins of mathematical ideas. I just finished a chapter on the infinitesimals which was the clearest exposition of why these numbers are so alluring as well as divisive.
In the relevant chapter, they provide a sketch of a model theory proof that a set with at least one infinitesimal exists, but I am not completely convinced by it.
I don't know much about model theory, but I really like what Lakoff and Nunez are getting to, so I read a short introductory paper by David Marker and tried to write my own proof. I have looked up the proof to the Completeness Theorem, and I still have to wrap my head around that, but for the moment I trust Godel and Marker.
 A: The part that you are not finding intuitive is precisely the core of the completeness theorem, that is crucial to the compactness theorem. There is a technical sense in which that completeness theorem is non-constructive. And also the model produced in the proof of the completeness theorem is not at all going to be a meaningful model except for establishing the theorem.
In Henkin's construction, you start with the consistent theory and add independent sentences to the axiom set. This depends on being able to decide at each step whether a sentence is independent or not. If the original theory is recursive, the simplest way one could make such decisions is if one has the halting oracle, so that one can ask whether some recursive set of axioms is consistent or not.
Notice that in the above you need first choose some enumeration of all the sentences and iterate through them one by one, at each step adding it if it is independent. If the original theory was not already syntactically complete, you will get totally meaningless axioms being proven in the newly constructed theory, since for any independent sentence you would add either it or its negation and that choice depended on the order they are enumerated.
Ιt is easy to prove that the complete theory of the natural numbers cannot be decided by anything less than the ω-th Turing jump. So if we start with a recursive theory that interprets PA (has all of the axioms for natural numbers), and add a constant symbol $c$ and the axioms $1<c$ , $1+1<c$ , $1+1+1<c$ , $\cdots$ and use the above proof of the completeness theorem, the resulting theory must be arithmetically unsound (it proves some false sentence about natural numbers), because we can decide it using just the first Turing jump.
Note that in your case you would get an infinitesimal in the constructed model as the interpretation of $1/c$, since $c$ is bigger than any natural number.
Now you may think, what if your initial theory does not interpret PA, such as if you start with the first-order theory of the reals, which is itself already complete? At the least, you can see that the model you get by the completeness theorem via the Henkin construction is not going to make much sense, because you need a different model for each finite set of the new axioms to show that it is consistent, and then you discard the model and just utilize the consistency of finite subsets to get consistency of the whole axiom set. And also because the model you get is countable.
In sum, the model produced by the completeness theorem is not a model whose elements are real entities related semantically by the axioms, but rather a model constructed out of symbolic strings with semantics overlaid on them. I hope this explains where the unnaturalness comes from.

Nevertheless, there is an intuitive explanation avoiding the syntactic flavour of the compactness theorems. Consider what happens to the model you choose to show satisfiability, as you add the new axioms one by one. You get something like $c \to \infty$, in the sense that larger and larger lower bound is known about $c$ in the model. Given any quantifier-free sentence (in the expanded language), once you know a sufficiently large lower bound on $c$ the sentence's truth-value will be fixed from then onward, because polynomials over $c$ have well-defined behaviour as $c \to \infty$. Moreover, any sentence of the form $\exists x ( f(x) )$ will also have truth value stabilizing after some point, because a conjunction of equalities can be combined into a single equality using the identity $x=0 \land y=0 \equiv x^2+y^2=0$, and a conjunction of inequalities involving polynomials in $c,x$ will reduce to a conjunction of inequalities between asymptotic function classes since there is at most one equality that determines the asymptotic behaviour of $x$ as $c \to \infty$. This argument can (I think) be adapted to show quantifier elimination for the deductive closure of the theory $R$ of real-closed fields plus the axioms bounding $c$.
For example, consider $\exists x ( x^7 = c^3 \land x^2+4 < c )$. It may be false for the model you pick if you only have added $1 < c$ and $1+1 < c$. But once you add $1000 < c$, you can actually prove using the field axioms that $x < 10$ implies $x^7 < 1000^3 < c^3$, and since $R$ also has an axiom $\forall y\ \exists x\ ( x^7 = y^3 )$, we can prove that there is some $x$ such that $x^7 = c^3$ and $x \ge 10$, giving $x^2+4 < x^2+x^2 < x^2·2$ and then $(x^2+4)^3 < x^6·8 < x^7 = c^3$, and hence $x^2+4 < c$.
I am not sure how intuitive quantifier elimination is to you though...
A: To build a model with infinitesimals it is not necessary to learn model theory or even the compactness theorem.  It is sufficient to take an ultrapower of the usual model. Already Edwin Hewitt in 1948 used a version of such a construction and even introduced the term hyper-real.  In 1955 Jerzy Los proved his theorem to the effect that an ultrapower provides an elementary extension, which is exactly what you want.  More information on this can be found here; see for example this recent text that provides a technical summary.
