Editing Calculus of constructions (section)

===Judgments===

The calculus of constructions allows proving '''typing judgments''':

:<math> x_1:A_1, x_2:A_2, \ldots \vdash t:B</math>,

which can be read as the implication

: If variables <math>x_1, x_2, \ldots</math> have, respectively, types <math>A_1, A_2, \ldots</math>, then term <math>t</math> has type <math>B</math>.

The valid judgments for the calculus of constructions are derivable from a set of [[Rule of inference|inference rules]]. In the following, we use <math>\Gamma</math> to mean a sequence of type assignments 
<math> x_1:A_1, x_2:A_2, \ldots </math>; <math>A, B, C, D</math> to mean terms; and <math>K, L</math> to mean either <math>\mathbf{P}</math> or <math>\mathbf{T}</math>. We shall write <math>B[x:=N]</math> to mean the result of substituting the term <math>N</math> for the [[free variable]] <math>x</math> in the term <math>B</math>.

An inference rule is written in the form

:<math>\frac{\Gamma \vdash A:B}{\Gamma' \vdash C:D}</math>,

which means

: if <math> \Gamma \vdash A:B </math> is a valid judgment, then so is <math> \Gamma' \vdash C:D </math>.