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.
There's a distinction between syntax and semantics and between talking about the logic (meta-logic) and talking within the logic.
$\alpha$ and the $t : A$ notation is talking about the logic, and particularly which terms and formulas are in it. If we have $1+x \in \text{Trm}_\mathsf{Int}$, to know if this is a well-formed term of type $\mathsf{Int}$ requires knowing what the type of $+$, $1$, and $x$ are, e.g. $+ : \mathsf{Int}\times\mathsf{Int}\to\mathsf{Int}$, $1 :\,\to\mathsf{Int}$, and $x:\mathsf{Int}$. Given these we can verify with general rules that $1+x$ is well-formed and has type $\mathsf{Int}$. If $x : \mathsf{Bool}$ instead, then $1+x$ just wouldn't be a well-formed term at all, and there would be no meaning in asking any further questions about the term. Indeed, $(1+x)\Xi\mathsf{Int}$ would itself be an ill-formed formula. A completely analogous situation happens in programming languages. If you have a Java program that's ill-typed, it doesn't make sense to ask how it would behave despite being ill-typed. The meaning of Java programs is simply not defined for ill-typed programs. You could even say ill-typed Java programs aren't actually Java programs at all.
The rules in the technical report more or less build in the subsumption rule that you could write as: if $t \in \text{Trm}_A$ and $A \sqsubseteq B$ then $t \in \text{Trm}_B$. Therefore, for every well-formed term $t$, $t \in \text{Trm}_\top$. In particular, for a predicate symbol $p(A)$, $p(t)$ is a well-formed formula for any $t\in\text{Trm}_B$ where $B\sqsubseteq A$, so as far as any formula is concerned, a term of type $B$ is just as good as a term of type $A$. The definition of semantics they give just outright states, using their notation, $D^B \subseteq D^A$ if $B\sqsubseteq A$. Completeness with respect to this notion of semantics requires the subsumption rule. As for $\Xi A$, there need to be rules or axioms describing it. Now, as a meta-logical statement, you could say: whenever $t \in \text{Trm}_A$, the theorem $t\Xi A$ is provable. An instance of this would be since $1+1 \in \text{Trm}_\mathsf{Int}$, $(1+1)\Xi\mathsf{Int}$ is provable. So this meta-theorem is saying, for every term $t$ such that $t \in \text{Trm}_A$, we can find a proof of $t\Xi A$. In contrast, within the logic we have the statement $\forall x:A.x\Xi A$ (or using the notation in the technical report: $\forall A\ x; x\Xi A$). This is a single theorem within the logic. In fact, $\forall x.x\Xi\top$ is true, but the meta-logical statement "everything is a well-formed term of type $\top$" definitely is not as not everything is a well-formed term or even anything like a term. Going by the technical report, I assume $\Xi A$ is related to the $\text{instance}_A$ function symbol which leads to $\forall \top\ x;(x\Xi A \iff \exists A\ y; y \doteq x)$ as the defining axiom for $\Xi A$. (I've tweaked it slightly as for their JFOL the axiom for $\text{instance}_A$ is restricted to "Objects" which is not the top type in their hierarchy. As far as I can tell, $\text{instance}_\mathsf{int}(3)$ is left unspecified if $\mathsf{int}$ is a primitive Java type i.e. $\mathsf{int}\not\sqsubseteq \mathsf{Object}$ where $3:\,\to\mathsf{int}$.)
There's a similar syntax versus semantics issue in your question about predicate symbols. A predicate symbol is not "a function to the set $\{\text{True}, \text{False}\}$". A predicate symbol is, as its name suggests, just a symbol, a piece of syntax. Classical first-order logic happens to have a sound and complete semantics where we can interpret formulas as picking out subsets of the Cartesian product of interpretations of the types of its domain which we can then identify with characteristic functions, but there is absolutely no need to do this. We can work entirely syntactically, and computer scientists tend to lean this way as programming itself is highly syntactic. It is also the case that this interpretation is not sound and complete for other logics. If you are dead set on working semantically, the domain of a predicate symbol $p(A, B)$, for example, is the Cartesian product $[\![A]\!]\times[\![B]\!] \subseteq [\![\top]\!]\times[\![\top]\!]$ where $[\![\_]\!]$ is the interpretation function that sends a type to a set. There is an interpretation function sending terms to elements of the appropriate set, which I'll also write $[\![\_]\!]$, such that $[\![t]\!]\in[\![A]\!]$ when $t \in \text{Trm}_A$. So the interpretation of the variable symbol $x : A$ will be in the domain of the interpretation of a predicate $p(A)$. (To be completely pedantic, we interpret terms, not variable symbols, and variable symbols only embed into terms; they aren't necessarily terms in and of themselves.) The term part of the interpretation is a set function $\text{Trm}_A \to [\![A]\!]$ for each type $A$. This function need not be surjective, which is to say there can be elements of $[\![A]\!]$ which don't correspond to any term. So, the interpretation of a type, i.e. $[\![A]\!]$ is an arbitrary set which must satisfy some rules. We can map terms into this set, but the elements are not (usually) terms themselves and there can be other elements. The interpretation of predicate and function symbols needs to correctly work with all elements of these sets, even ones that don't correspond to terms. Again, none of this interpretation stuff is at all necessary to work with or understand the logic. Indeed, computer implementations usually don't use this at all and operate purely syntactically. (Model checking does leverage semantics though.) It's certainly a rich field and it provides a different perspective to the logic, but it is not necessary.
Summarizing, $x : B$ is data provided which is used to define what a well-formed formula is. It is used to produce the meta-logical predicate $t\in\text{Trm}_A$ stating that a term $t$ is well formed and has type $A$ (similarly for formulas). $t\Xi A$ is a formula within the logic that can be formally proven or refuted with the rules of the logic. Semantically, $[\![\Xi A]\!] = [\![A]\!]\subseteq[\![\top]\!]$. In some ways $\Xi A$ does kind of internalize the typing judgement. We could eliminate all types except for $\top$ and instead of having for $p : A,B$, $p(t_1,t_2)$ where $t_1 \in \text{Trm}_A$ and $t_2 \in\text{Trm}_B$, we could say this is really an abbreviation for $t_1\Xi A \land t_2\Xi B \land p(t_1,t_2)$ where $p : \top,\top$ and $t_1, t_2 \in\text{Trm}_\top$. Nevertheless, for the purpose of semantics, the roles of $\Xi A$ and the typing judgement are different. The typing judgement specifies what the domains of the interpretation functions are while $\Xi A$ is just an element of one of those domains.