On présente le lambda calcul du second ordre ainsi que sa preuve de normailsation. On parle de l'expressivité du système (fonctions dont la terminaison peut être prouvée dans l'arithmétique du second ordre).
On présente enfin l'application de la normalisation forte à la preuve de cohérence de l'arithmétique du second ordre (après avoir mis en évidence ce qui, dans la preuve de nomalisation forte nécessitait l'usage de l'ordre 3).