Il corso partirà dai più importanti risultati limitativi, come l'insolubilità dell problema della decisione per la logica del prim'ordine. Successivamente proseguirà analizzando diverse interpretazioni del primo e del secondo teorema di Goedel, ma anche di risultati meno noti come il teorema di Tennenbaum circa i modelli non standard dell'aritmetica. Per questa analisi si renderà necessario richiamare i più importanti modelli di computazione. Essendo le funzioni parziali ricorsive e le macchine di Turing argomenti ampiamente trattati in altri corsi, focalizzeremo soprattutto il lambda calcolo. Questo è uno dei grandi modelli di computazione, equivalente alle funzioni parziali ricorsive e alle macchine di Turing. Church utilizzò questo strumento per dimostrare l'insolubilità dello Entscheidungsproblem. Nei suoi sviluppi successivi e nelle versioni tipate, costituì la base per ulteriori ricerche intorno alla nozione di matematica finitaria e alla fondazione costruttiva della matematica e un importante collegamento fra logica e programmazione funzionale. Un altro obiettivo è quello di introdurre elementi avanzati di teoria della dimostrazione, come il calcolo a sequenti di Gentzen per vari frammenti dell'aritmetica, rilevanti nel campo della complessità computazionale