Suppose we want to formalise some parts of mathematics within set theory, which is itself formalised in a first-order language (in the standard way). Logic is assumed to be classical. In particular, this means that – at the level of semantics – every term must have a denotation, which in turn means that every function must have as its domain the entire universe of the model (or its Cartesian product, if it has more than one argument). Let’s say that we construct within our set theory natural numbers, then integers, rational numbers and real numbers (in the standard way). At some point we would like to consider, for example, functions from real numbers to real numbers. However, if we just introduce a functional symbol to the language, then the corresponding function has to have as its domain the entire universe of set theory, not just real numbers. How to deal with this issue? Here are some options that I find unsatisfactory:
(1) Consider the theory of real numbers only, not the entire set theory – then every model of this theory will be just a set of all real numbers. This is fine if we are interested in real numbers only. However, if we are going to consider other set-theoretic constructions that are not real numbers, then we should better stay within full set theory. And even if we want to restrict to real numbers only, there will be functions that are not defined on all real numbers, such as division, which is not defined if the second argument is $0$.
(2) Change classical logic into free logic (which allows terms without denotation; cf. here and here) or many-sorted logic (which allows functions with different domains, depending on the type of a function). This is unsatisfactory mainly because using functions with domain that is not the entire universe of the model is commonplace in mathematics but the official logic of mathematics seems to be classical first-order logic, so there should be some solution within it. In any case, I am just interested in solutions within classical first-order logic.
(3) Choose some arbitrary object as the value of the function for the arguments for which we want it to be ill-defined (cf. here). This is unsatisfactory because it is commonplace in mathematics to talk about functions on some restricted domain, not about functions that work as we want on the intended domain and arbitrarily elsewhere. For example, when we write $f : \mathbb{N} \to \mathbb{R}$, we really mean a function whose domain is exactly $\mathbb{N}$.
(4) Use relational symbols to simulate functions (cf. here). This sounds promising because this is in agreement with how functions are defined in set theory. However, this also is unsatisfactory because when we write mathematical formulas, we use functional symbols and we use terms such as $f(x)$.
Perhaps we can think about functional notation as an abbreviation for relational notation. For example, if we write $f(x)=y$, we really mean $R_f (x, y)$ for some relation $R_f$ satisfying $\forall_x \left[\left( \forall_y \neg R(x,y) \right) \vee \left(\exists!_y R(x,y)\right)\right]$. However, it is not clear to me how then should we think about formulas of a more complex form, such as $g(f(x), f(y)) = z$.
I believe that there should be some solution that is both fully correct formally and does justice to the usual practice. Perhaps some variant of option (4) would work but more details are needed.
