What is the difference between $x:A$ and $x \Xi A$? 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

$\tau$ is a set of type symbols;
$\sqsubseteq$ is a partial ordering on $\tau$, called the subtype relation;
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

$v : A$ for $\alpha (v) = A$,
$f : A_1,...,A_n \to A$ for $\alpha(f)=((A_1,...,A_n),A)$,
$p: A_1,...,A_n$ for $\alpha(p)=(A_1,...,A_n)$,
$x \Xi A$ (read: $x$ is an instance of $A$) for $\Xi A(x)$,
$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.
$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$.