# 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.)

## 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.

• Basically, you can't write $x:A$ inside the language. The ":" relation lives in the metatheory, only. Instead $x \Xi A$ is an expression inside the language (the theory).
– chi
May 31, 2017 at 14:54

$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$.