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 teorema di Goedel, focalizzando i concetti di "matematica costruttiva" e "finitaria". Per questa anaisi 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.