So, I want to use model theory to approach an applied task. Developing the corresponding vocabulary, I realized I needed real numbers within my formulas and, thus, real numbers within the language. I decided to introduce a sort of Real Number, function, and relation symbols representing the standard arithmetic operations, order relations, etc. As I understand, I cannot just say that the interpretation of this sort is one particular constant set for all structures. Another approach would be to specify all axioms of real numbers so that the sort implementations are mutually isomorphic within all structures. I could say that I assume those axioms exist within the theory without defining them explicitly. However, I'm not sure it is possible.
So, my questions are:
- It may be better just to abandon the idea of approaching an applied task using model theory, which seems to fit better for dealing with abstract structures. What do you think?
- If it's generally okay to approach the modelling of a real-world system using model theory, how can I use real numbers within my vocabulary?
Edit: I can formulate the question concisely. How do you use real numbers in your vocabulary (language) and consequently within formulas in model theory?
Edit: As Z. A. K. suggested in the comments, the question may look like this:
"If my language $L$ includes a sort $R$, binary operations $+$, $\cdot$ on $R$, and binary relations $<$, $\leq$ on $R$, what is the preferred/standard/customary way of stating/enforcing/requiring that the $\textit{interpretation}$ of the sort $R$ in any $L$-structure I consider should be $\mathbb{R}$ with its usual arithmetic and ordering?"
In general, everything gets messier. While a version of the downward Lowenheim-Skolem theorem persists (e.g. if our "target structure" is $\mathbb{R}$ we just replace $\aleph_0$ with $2^{\aleph_0}$), the compactness theorem - which is far more crucial in most applications - breaks horribly. Indeed, deep set-theoretic issues enter even seemingly-basic questions; see e.g. this old MO question of mine and its periphera.
A useful phrase here is "classification theory over a predicate" - see e.g. the introduction to Pillay/Shelah's paper of that name. So the topic is indeed studied. But I would be very hesitant to expect the usual tools from first-order model theory to apply directly to any interesting problem in this setting.