0
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ What is the origin of the problem ? You concern is correct: the standard semantics for FOL has a unique domain. If we want to separate sub domains, we have to use suitable predicates, like $H(x)$ for Human and $M(x)$ for Money. $\endgroup$ – Mauro ALLEGRANZA May 11 at 18:58
  • $\begingroup$ An alternative approach is with Many-sorted logic. $\endgroup$ – Mauro ALLEGRANZA May 11 at 19:00
  • $\begingroup$ @MauroALLEGRANZA this is part of a modelling exercise for a Knowledge Based System. $\endgroup$ – Rafael Bankosegger May 11 at 19:02
  • 1
    $\begingroup$ See Jean Gallier, Logic for computer science : Foundations of Automatic Theorem Proving (2003) , Ch.10 : Many-Sorted First-Order Logic. The general definition seems complex but the example (page 451) is simple. You need a two-sorts language with $S = \{ \text {people}, \text {integer} \}$ and the function $\text {balance}(x)$ is defined as a function from $\text {people}$ to $\text {integer}$. $\endgroup$ – Mauro ALLEGRANZA May 12 at 8:26
  • 1
    $\begingroup$ Thus, the formula will be $\forall_{ \text {people} } x \ [((\text {balance} (x) > \text { 1M }) \lor (\ldots)) \to \text {Rich}(x)]$. $\endgroup$ – Mauro ALLEGRANZA May 12 at 8:31
1
$\begingroup$

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$)→𝑅𝑖𝑐ℎ(𝑥)))

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.