Calculus of constructions

A term in the calculus of constructions is constructed using the following rules:

• ${\displaystyle \mathbf {T} }$ is a term (also called type);
• ${\displaystyle \mathbf {P} }$ is a term (also called prop, the type of all propositions);
• Variables (${\displaystyle x,y,\ldots }$) are terms;
• If ${\displaystyle A}$ and ${\displaystyle B}$ are terms, then so is ${\displaystyle (AB)}$;
• If ${\displaystyle A}$ and ${\displaystyle B}$ are terms and ${\displaystyle x}$ is a variable, then the following are also terms:
  • ${\displaystyle (\lambda x:A.B)}$,
  • ${\displaystyle (\forall x:A.B)}$.

In other words, the term syntax, in BNF, is then:

${\displaystyle e::=\mathbf {T} \mid \mathbf {P} \mid x\mid e\,e\mid \lambda x{\mathbin {:}}e.e\mid \forall x{\mathbin {:}}e.e}$

The calculus of constructions has five kinds of objects:

1. proofs, which are terms whose types are propositions;
2. propositions, which are also known as small types;
3. predicates, which are functions that return propositions;
4. large types, which are the types of predicates (${\displaystyle \mathbf {P} }$ is an example of a large type);
5. ${\displaystyle \mathbf {T} }$ itself, which is the type of large types.

The calculus of constructions allows proving typing judgments:

${\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots \vdash t:B}$

Which can be read as the implication

If variables ${\displaystyle x_{1},x_{2},\ldots }$ have types ${\displaystyle A_{1},A_{2},\ldots }$, then term ${\displaystyle t}$ has type ${\displaystyle B}$.

The valid judgments for the calculus of constructions are derivable from a set of inference rules. In the following, we use ${\displaystyle \Gamma }$ to mean a sequence of type assignments ${\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots }$; ${\displaystyle A,B,C,D}$ to mean terms; and ${\displaystyle K,L}$ to mean either ${\displaystyle \mathbf {P} }$ or ${\displaystyle \mathbf {T} }$. We shall write ${\displaystyle B[x:=N]}$ to mean the result of substituting the term ${\displaystyle N}$ for the free variable ${\displaystyle x}$ in the term ${\displaystyle B}$.

An inference rule is written in the form

${\displaystyle {\Gamma \vdash A:B} \over {\Gamma '\vdash C:D}}$

which means

If ${\displaystyle \Gamma \vdash A:B}$ is a valid judgment, then so is ${\displaystyle \Gamma '\vdash C:D}$

1. ${\displaystyle {{} \over \Gamma \vdash \mathbf {P}$ :\mathbf {T} }}

2. ${\displaystyle {{} \over {\Gamma ,x:A,\Gamma '\vdash x:A}}}$

3. ${\displaystyle {\Gamma \vdash A:K\qquad \qquad \Gamma ,x:A\vdash B:L \over {\Gamma \vdash (\forall x:A.B):L}}}$

4. ${\displaystyle {\Gamma \vdash A:K\qquad \qquad \Gamma ,x:A\vdash N:B \over {\Gamma \vdash (\lambda x:A.N):(\forall x:A.B)}}}$

5. ${\displaystyle {\Gamma \vdash M:(\forall x:A.B)\qquad \qquad \Gamma \vdash N:A \over {\Gamma \vdash MN:B[x:=N]}}}$

6. ${\displaystyle {\Gamma \vdash M:A\qquad \qquad A=_{\beta }B\qquad \qquad \Gamma \vdash B:K \over {\Gamma \vdash M:B}}}$

The calculus of constructions has very few basic operators: the only logical operator for forming propositions is ${\displaystyle \forall }$. However, this one operator is sufficient to define all the other logical operators:

${\displaystyle {\begin{array}{ccll}A\Rightarrow B&\equiv &\forall x:A.B&(x\notin B)\\A\wedge B&\equiv &\forall C:\mathbf {P} .(A\Rightarrow B\Rightarrow C)\Rightarrow C&\\A\vee B&\equiv &\forall C:\mathbf {P} .(A\Rightarrow C)\Rightarrow (B\Rightarrow C)\Rightarrow C&\\\neg A&\equiv &\forall C:\mathbf {P} .(A\Rightarrow C)&\\\exists x:A.B&\equiv &\forall C:\mathbf {P} .(\forall x:A.(B\Rightarrow C))\Rightarrow C&\end{array}}}$

The basic data types used in computer science can be defined within the calculus of constructions:

Booleans

${\displaystyle \forall A:\mathbf {P} .A\Rightarrow A\Rightarrow A}$

Naturals

${\displaystyle \forall A:\mathbf {P} .(A\Rightarrow A)\Rightarrow (A\Rightarrow A)}$

Product ${\displaystyle A\times B}$

${\displaystyle A\wedge B}$

Disjoint union ${\displaystyle A+B}$

${\displaystyle A\vee B}$

Note that Booleans and Naturals are defined in the same way as in Church encoding. However, additional problems arise from propositional extensionality and proof irrelevance.[2]