Natural deduction and models

Lecture outline:

• Curry-Howard;
• Gentzen's natural deduction;
• inductive definitions following Martin-Löf;
• algebraic presentation of type theory and term model as initial model;
• some examples of models, in particular the set model and prefix models.