Calculus of Constructions

The following is a condensed description of the Calculus of Constructions (Source: https://en.wikipedia.org/wiki/Calculus_of_constructions).

The Calculus of Constructions is a type of lambda calculus.

Terms

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

• T is a term (also called Type);
• P is a term (also called Prop, the type of all propositions);
• Variables (x, y, ...) are terms;
• If A and B are terms, then so is (A B);
• If A and B are terms and x is a variable, then the following are also terms:
  • (λx:A . B),
  • (∀x:A . B).

Objects 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 (P is an example of a large type);
5. T itself, which is the type of large types.

Judgments The calculus of constructions allows proving typing judgments:

[[https://github.com/rpi-alpaca/logic/blob/master/wiki-images/calculus/1.png|alt=octocat]]