After reading "In Defense of the Simplest Quantified Modal Logic", I wonder how to add functions to the language of the simplest quantified modal logic (QML for short). The simplest model of QML has a "global" non-empty domain of individuals that all worlds share. Hence, I think one can interpret it as a kind of many-valued logic, especially with respect to the problem of how to add functions to the language.
I haven't seen any reference that explains how to add functions to quantified modal logic or many-valued logic. My question is how to do it for QML or many-valued logic?
I would also like to know whether adding functions extends the language in a non-trivial way that can't be emulated by the same language without functions?
See my explanations below why I'm worried about this possibility.
The constants and variables of QML are rigid designators, and equality seems to be independent of the considered world. An obvious approach to add functions to QML would be as global functions on the domain of individuals, independent of the considered world. (I say obvious, because this is what I expect from functions for many-valued logic). In that case, function too would be rigid designators.
What worries me about this approach is that the available language doesn't allow to state this fact. When I say "equality seems to be independent of the considered world", I mean that it is independent for the simplest model of QML, but the available axioms for equality don't allow to prove this. In fact, the available language doesn't even allow to state this fact. This leads me to suspect that functions can't be emulated by predicates/relations for that approach, unless appropriate modal operators allowing to talk about all worlds at once are added to the language. A failure to emulate functions by a language without functions might not be a show-stopper, but it would be sort of unexpected for me.
Another approach to add functions would be to have different functions for each world acting on the domain of individuals. However, I have no idea about the advantages or disadvantages of this approach. It seems to me as if it would be possible to emulate this type of functions by predicates/relations. Functions of 0 arguments would now yield a second sort of constants which wouldn't be rigid designators. But these were already available before, simply by emulating functions via predicates. However, I'm less sure how to make sense of this approach in the context of many-valued logic.