Typing judgments

Given a typing context, ${\cal T}$, we can assign types to terms built from the variables in the context. The judgment that term t has type T in context ${\cal T}$ is expressed by writing

$${\cal T} \vdash t \in T.$$

If we need to be explicit about the variables of ${\cal T}$ and t, we use a second-order variable $t[x_1, \ldots, x_n]$ and write

$$x_1\!:\!T_1, \ldots, x_n\!:\!T_n \vdash t[x_1, \ldots, x_n] \in T$$

When using a second-order variable we know that the only variables occurring in t are x_i. We call these variables of t free variablesvariable!free and boundfree variable.

Later, we give rules for knowing these judgments. Just as we said in section 2.2, it should be noted that $t \in T$ is not a proposition; it is not an expression that has a truth value. We are saying what an ordered pair is rather than giving a property of it. So the judgment $t \in T$ is giving the meaning of t and telling us that the expression t is well-formed or meaningful. In other presentations of predicate logic these judgments are incorporated into the syntax of terms, and there is an algorithm to check that terms are meaningful before one considers their truth. We want a more flexible approach so that typing judgments need not be decidable.

We let $P_1, P_2, \ldots$ denote propositional variables, writing $P_i\in \ Prop$, for propositional function variables, writing $P_i \in (T\rightarrow \ Prop)$ for T a type expression.

If ${\cal T} \vdash t \in T$ and $P \in(T \rightarrow \ Prop)$, then P(t) is an atomic formulaatomic formula in the context ${\cal T}$ with the variables occurring in t free; it is an instanceinstance of P. Note, we abbreviate $P\left(\left\langle t_1, \ldots, t_n\right\rangle\right)$ by $P(t_1, \ldots, t_n)$. If t is a variable, say x, then P(x) is an arbitrary instance or arbitrary value of P with free variable x. A propositional variable, $P_i\in \ Prop$, is also an atomic formula.

If F and G are formulas with free variables $\bar{x}, \bar{y}$ respectively in contexts ${\cal T}$, and if op is a connective and $Qx\!:\!A$ a quantifier, then

$$(F\:op\: G)$$

is a formula with free variables $\{\bar{x}\} \cup \{\bar{y}\}$ in context ${\cal T}$ and with immediate subformulas F and G;

$$Qv\!:\!T. F$$

is a formula in context ${\cal T}'$ where ${\cal T}'$ is ${\cal T}$ with $v\!:\!A$ removed; this formula has leading binding operator $Qv\!:\!A$with binding occurrence of v whose scopescope is F, and its free variables are $\{\bar{x}\}$ with vremoved, and all free occurrences of v in F become bound bound variablevariable!free and bound by $Qv\!:\!A$; its immediate subformula is F.

A formula is closed iff it has no free variables; such a formula is well-formed in an empty context, but its subformulas might only be well-formed in a context. A subformulasubformula G of a formula F is either an immediate subformula or a subformula of a subformula.