Teoria della dimostrazione: calcoli LK, Hauptsatz e corollari. Deduzione naturale, lambda calcolo tipato,La corrispondenza di Curry-Howard. Normalizzazione. Applicazioni (PA, omega-regola; ordinali nella proof theory)). Teorema di Takeuti-Parsons-Mints