FOL: Dealing with different "classes" of elements in the domain

Question

Consider the FOL-signature: $$\Sigma = \langle\{balance\; /\; 1, spouse\; /\; 1\}, \{Rich \; / \; 1, > / \;1 \}\rangle$$

where $balance$ and $spouse$ are function symbols of arity 1 and $Rich$ and $>$ are predicate symbols of arity 1.

Now consider the formula:

$$\forall x ((balance(x) > 1.000.000$ \; \lor balance(spouse(x)) > 1.000.000$) \to Rich(x))$$

While the formula itself is a well-formed $\Sigma$-Formula, applying semantics may lead to some weirdness. What bothers me are the following points:

• Both money and people share one domain
• The functions $balance$, $spouse$ and the predicate $Rich$ make only sense when applied to the "people" subset of the domain. What would the spouse of some arbitrary amount of money be?
• The function $>$ makes only sense when applied to the "people" subset of the domain.
• $\forall x$ includes all values for "money" in the domain. This probably has some strange effects on the semantics of the formula itself.

My main question is how this problem is dealt with in practice. Is it actually an issue? How could it be solved?

Answer 1

The problem you mention can be dealt with in two different manners:

1. By relativizing the quantifiers, in your example as follows, using appropriate unary predicates:

∀ (person(x) $\rightarrow$ ((()>1.000.000$∨(())>1.000.000$)→ℎ()))

2. By using a many-sorted logic ([https://en.wikipedia.org/wiki/Many-sorted_logic][1])