Motivation, background. Kolmogorov's and Heyting's explanations of
the logical constants.
An overview of the polymorhic type theory. This is an obsolete
theory which is a historical stepping stone towards the
monomorphic theory. Syntax: the theory of expressions with their
Semantics of the different judgement forms. Structure of the
The cartesian product between two sets and the disjoint union of a
family of sets. Different reading of the rules. Enumeration sets.
Natural numbers. The cartesian product of a family of sets and its
special cases (the for all quantifier, the set of functions,
A brief overview of the monomorphic theory. Types and
objects. Definitions. How to represent a proof. How to build a proof.
The compiler example.
Universes and wellorderings. How to express different inductive
sets using wellorderings and the problem with intensional
Peano's fourth axiom.