Understanding sorts in many sorted logic intuitively

Question

I have a variable set $v$ of size 6.

$V =\{a,b,c,p,q,r\}$

I have two statements

$\forall_{x \in \{a,b,c\}} x$ is an integer

$\forall_{x \in \{p,q,r\}} x$ is an irrational number

Now I am using a sort set $S = \{\mathbf{Z}, \mathbf{R-Q}\} $

Now I assign $a,b,c$ to sort $\mathbf{Z}$ and remaining three variables to another sort $\mathbf{R-Q}$

My two statements become true now. Thus sort is either a set or a mechanism to differentiate or to assign variables a particular identity.

Is my understanding true?

Answer 1

For each sort $\sigma_i$ we have the corresponding variables $v_1^i, v_2^i, \ldots$.

Sorts are "kind" of objects that we want to distinguish.

Consider the silly example: we want to speak of humans and numbers at the same time.

Instead of considering a single domain $D$ with humans and number together, we "divide" the domain into two sorts : $S_1$ with all and only humans and $S_2$ with all and only numbers.

In this way, we quantify separately on humans, using variables of sort $\sigma_1$, and on mumbers, using variables of sort $\sigma_2$.

A less silly example is the definition of limit of a sequnce :

for each real number $\epsilon >0$, there exists a natural number $N$ such that, for every natural number $n\geq N$, we have $|x_{n}-x| < \epsilon$.

The usual formula :

$\forall \epsilon \in \mathbb R^+ \ \exists N \in \mathbb N \ \forall n \in \mathbb N \ldots$

can be rewritten in two-sorted logic using $N,M,n,m$ as variables for the sort $S_1$ of natural numbers and using $\epsilon, \delta, x, y$ as variables for the sort $S_2$ of the real numbers, to get :

$\forall \epsilon >0 \ \exists N \ \forall n \ldots$.

---

Many-sorted logic can be easily rewritten into standard (one sort) predicate logic with suitable predicates.

We use $\text N(x)$ to symbolize the fact that $x$ is a natural and $\text R(x)$ for the reals.

In this way we have :

$\forall x \ \exists y \ \forall z \ (\text R(x) \land \text N(y) \land \text N(z) \land (x > 0) \ldots)$

taht we usually abbreviate as $\forall x \in \mathbb R^+ \ldots$

Answer 2

You're mixing together syntax and semantics. Sorts are a syntactic concept hence the discussion of "sort symbols" in your previous question. As that answer indicates, sorts get interpreted into sets (typically) when we consider the semantics of the many-sorted logic. Furthermore, the consumer of our (syntactic) logical theory is the one who gets to decide what sets the sorts get interpreted as, not us as the definer of the logical theory. The only influence the definer of the logical theory gets on what sets the sorts are interpreted as is via the axioms of the theory. It is rarely the case that axioms can pin down the interpretation of a sort to a precise set or even a precise (infinite) cardinality. If there is a model (i.e. valid semantics) of a first-order theory (many-sorted or otherwise) that interprets a sort as an infinite set, then there are also models that interpret that sort as an infinite set of any given infinite cardinality.

So, while technically allowable (mostly by accident), it makes little sense to use $\mathbb Z$ and $\mathbb R\setminus \mathbb Q$ as sort( symbol)s. In particular, there is absolutely nothing requiring the sort $\mathbb Z$ to be interpreted as the set $\mathbb Z$. Sorts should be thought of as meaningless names. The only aspect of a sort that we care about is its identity. When studying formal logic in more minimalistic foundations, such as PRA, we can easily model sorts and many-sorted logic, but sets don't even exist.

Related to the first paragraph, you may also find it rather difficult to produce a formal formula that means "$x$ is an integer" or "$x$ is irrational". There are a bunch of different obstacles that could arise with respect to this, but the best you could hope for is that in your intended semantics the formula interprets as "is an integer" in the usual set-theoretic sense. There will be other semantics where the interpretation of that formula contains things which are very much not elements of $\mathbb Z$ or even sets that are in bijection with $\mathbb Z$.

What sorts do is allow us to constrain the syntax of terms and formulas. That is, they affect the definition of well-formed formulas/terms which will in turn affect the semantics. This is particularly useful for function symbols, because, as Mauro ALLEGRANZA demonstrated, the translation of many-sorted predicate symbols is fairly straightforward. Many-sorted function symbols, on the other hand, have to be replaced with predicate symbols in general since the interpretation of these many-sorted function symbols will be functions that aren't total on the new combined domain. This isn't a technical barrier, but it is annoying and awkward. For example, the theory of vector spaces is naturally 2-sorted with a sort for scalars and a sort for vectors. Scaling can then be represented by a function symbol of sort $(\mathsf{S},\mathsf{V})\to\mathsf{V}$. If we combined the sorts $\mathsf S$ and $\mathsf V$ into one sort, then this function symbol would allowing "scaling" a vector by a vector. We don't want to allow that so we're forced to encode the function symbol as a predicate symbol with additional axioms to force its interpretation to be a partial functional relation. This makes the syntax inconvenient as we can no longer just write something like $w=s\cdot v_1+s\cdot v_2$ but instead need something like $\exists u,v.S(s,v_1,u)\land S(s,v_2,v)\land A(u,v,w)$.

Answer 3

There is a subtle difference between sorts and "plain" sets, coming from the semantics which many-sorted first-order logic uses. Specifically, a structure in a many-sorted language must (in every presentation I've seen) have the property that every element belongs to exactly one sort. The obvious restriction this imposes is that sorts can't overlap, but this isn't really essential; the real problem occurs when we have infinitely many sorts. If we try to replace sorts by predicate symbols (so go from many-sorted to usual first-order), we run into a problem: by the compactness theorem, we will in general have structures with elements not belonging to any predicate symbol, but this corresponds to a structure with an element not belonging to any sort. So there is a sense in which many-sorted logic has a bit more power than first-order logic.

However, in practice we rarely run into situations where we actually need infinitely many sorts, and the disjointness of sorts isn't really that important, so it's generally fine to think of sorts as just (distinguished) sets.

Answer 4

The formulas you wrote have a misunderstanding of multi-sorted logic. If your sort set is $\{Z, I\}$, then every variable has to be annotated into one of these two sorts when you write a formula. Moreover, you cannot use the sorts themselves as predicates. So you can write $$ \forall x^I \phi(x^I)$$ or $$ \exists w^Z \psi(w^Z)$$ where $x^I$ is a variable of sort $I$ and $w^Z$ is a variable of sort $Z$, and $\phi$ and $\psi$ are appropriate formulas.

You cannot write $\forall x \in \{a, b, c\}$ for several reasons, but one is that the $x$ has no sort on it, while every variable in multi-sorted logic does. You can't "assign" a variable to a sort - the variable itself already tells you what sort that variable is.

Separately, the sorts in multi-sorted logic are not predicates. You cannot write, for example $Z(u)$ or $u \in Z$ to assert that $u$ is in sort $Z$. The variable $u$ would already carry a sort explicitly, and that is the sort of that variable, which can never change. So, for example, $u^Z$ and $u^I$ are completely different variables, which the logic does not view as related to each other in any way.

I think you are mixing together multi-sorted logic and first-order set theory, but they have very different syntax, and have to be treated separately.