What is the difference between $x:A$ and $x \Xi A$?

Question

Given a type hierarchy $(\tau,\sqsubseteq)$ and a signature $(VSym, FSym, PSym, \alpha)$, one says that the typing function $\alpha$ assigns to each variable symbol $x \in VSym$ a non-empty type $A \in \tau \setminus\{\bot\}$ and is written as:

$$ x: A \tag1$$

Furthermore, for every type $A \in \tau \setminus\{\bot\}$, there is a predicate symbol $\Xi A \in PSym$ called the type predicate which tells us if or not a certain $x$ is an instance of type $A$. We write it as:

$$x \Xi A \tag2$$

That makes me think what set constitutes the domain of a predicate symbol. Clearly, if the domain is $VSym$, then $(1)$ and $(2)$ mean exactly the same thing, and therefore, would be a redundancy of definition.

If not, which is surely the case, how do they differ? In particular, can you tell if a certain object is an instance of a certain type and not just a variable symbol with the given type assigned to it (or vice versa)?

More precisely, if a predicate symbol is a function from a certain domain to the set $\{\mathrm{True},\mathrm{False}\}$, what exactly is the domain of this map? Is there any overlap of this domain with $VSym$?

I am reading the chapter on first order logic from Deductive Software Verification – The KeY Book. (I am not fully sure if this question fits in a mathematics or a computer science forum.)

Thank you for your time.

---

Background:

Please refer to this document (the first couple of pages actually) to update yourself with the relevant ideas and definitions. Here's a brief summary.

---

A type hierarchy is a pair $\mathscr T = (\tau,\sqsubseteq)$, where

1. $\tau$ is a set of type symbols;
2. $\sqsubseteq$ is a partial ordering on $\tau$, called the subtype relation;
3. there are two designated type symbols, the empty type $\bot \in \tau$ and the universal type $\top \in \tau$ with $ \bot \sqsubseteq A \sqsubseteq \top \forall A \in \tau$.

---

A signature (for a given type hierarchy $\mathscr T$) is a quadruple $\Sigma = (VSym, FSym, PSym, \alpha)$ of

• a set of variable symbols $VSym$,
• a set of function symbols $FSym$,
• a set of predicate symbols $PSym$, and
• a typing function $\alpha$,

such that

• $\alpha(v) \in \tau_q := \tau \setminus\{\bot\}\ \forall v \in VSym$,
• $\alpha(f) \in \tau_q^* \times \tau_q\ \forall f ∈ FSym$, where $\tau_q^*$ is the set of all (possibly empty) sequences of elements in $\tau_q$, and
• $\alpha(p) \in \tau_q^*\ \forall p \in PSym$.
• There is a function symbol $(A) \in FSym$ with $\alpha((A)) = ((\top),A)$ for any $A \in \tau_q$, called the cast to type A.
• There is a predicate symbol $\doteq \in PSym$ with $α(\doteq) = (\top,\top)$.
• There is a predicate symbol $\Xi A \in PSym$ with $\alpha(\Xi A) = (\top)$ for any $A \in \tau$, called the type predicate for type A.

---

Notation: We write

1. $v : A$ for $\alpha (v) = A$,
2. $f : A_1,...,A_n \to A$ for $\alpha(f)=((A_1,...,A_n),A)$,
3. $p: A_1,...,A_n$ for $\alpha(p)=(A_1,...,A_n)$,
4. $x \Xi A$ (read: $x$ is an instance of $A$) for $\Xi A(x)$,
5. $x \doteq y$ for $\doteq(x,y)$.

---

NOTE: Some texts (such as the document linked above) implicitly do the type assignment carried out by $\alpha$ and write down the definition in the standard notation mentioned above.

Answer 1

$x:A$ is a statement about objects in the formal system, like, for example, $\vdash 2+4:\texttt{int}$, whereas $x\Xi A$ is an expression in the formal system, like $\texttt{if}~ 2 + 4 ~\texttt{==}~5 ~\texttt{then}~ e_1~ \texttt{else} ~e_2$.