Menù principale
B020988 - TEMI AVANZATI DI LOGICA
Principali informazioni
Lingua Insegnamento
Contenuto del corso
Libri di testo consigliati
Obiettivi Formativi
Prerequisiti
Metodi Didattici
Altre Informazioni
Modalità di verifica apprendimento
Programma del corso
Anno Accademico 2020-21
Anno di corso
Primo Anno - Secondo Semestre
Dipartimento di Afferenza
Lettere e Filosofia
Tipo insegnamento
Attività formativa monodisciplinare
Settore Scientifico disciplinare
M-FIL/02 - LOGICA E FILOSOFIA DELLA SCIENZA
Crediti Formativi
12
Ore Didattica
72
Periodo didattico
22/02/2021 ⇒ 28/05/2021
Frequenza Obbligatoria
Si
Tipo Valutazione
Voto Finale
Contenuto del corso
mostra
Programma del corso
mostra
Docenza
Lingua Insegnamento
Italiano.
Contenuto del corso
Introduzione alla teoria della dimostrazione
Libri di testo consigliati (Cerca nel catalogo della biblioteca)
1) Appunti del docente, accessibili online, con relativa bibliografia;
2) per approfondimenti, si possono consultare:
(i) J.Y.Girard, Proof Theory and Logical Complexity, Bibliopolis Napoli
1987;
(ii) A.S.Troelstra, H.Schwichtenberg, Basic Proof Theory, Cambridge
University Press, Cambridge 2000 (2nd ed.);
(iii) S.Negri and J. von Plato, Structural Proof Theory, Cambridge 2001;
(iv) M.H.Sorensen, P.Urczyn, Lectures on the Curry-Howard Isomorphism,
Amsterdam-New York 2006;
(iii) H.Schwichtenberg, S.S.Wainer, Proofs and Computations, Cambridge
2012.
2) per approfondimenti, si possono consultare:
(i) J.Y.Girard, Proof Theory and Logical Complexity, Bibliopolis Napoli
1987;
(ii) A.S.Troelstra, H.Schwichtenberg, Basic Proof Theory, Cambridge
University Press, Cambridge 2000 (2nd ed.);
(iii) S.Negri and J. von Plato, Structural Proof Theory, Cambridge 2001;
(iv) M.H.Sorensen, P.Urczyn, Lectures on the Curry-Howard Isomorphism,
Amsterdam-New York 2006;
(iii) H.Schwichtenberg, S.S.Wainer, Proofs and Computations, Cambridge
2012.
Obiettivi Formativi
Approfondire i fondamentali risultati sul concetto di 'dimostrazione',
emersi a partire dagli anni Trenta, e incentrati in particolare sulle
tecniche dell' 'eliminazione delle cesure' e della 'normalizzazione'
emersi a partire dagli anni Trenta, e incentrati in particolare sulle
tecniche dell' 'eliminazione delle cesure' e della 'normalizzazione'
Prerequisiti
Il corso propedeutico da 12 CFU di Logica (CdS triennale in Filosofia), o conoscenze equivalenti (in questo caso parlare con il docente prima dell'iscrizione al corso).
Metodi Didattici
Lezioni frontali integrate da esercitazioni guidate dal docente.
Altre Informazioni
I materiali per il corso (dispense, sintesi delle lezioni, esercizi, ecc.) saranno resi disponibili sulla piattaforma Moodle.
Si ricorda che è richiesta una frequenza obbligatoria per almeno i 2/3 delle lezioni.
Non sono previste modalità di esame da non frequentante se non per gli studenti con iscrizione part-time (che devono prendere contatto con il docente all'inizio del corso per concordare un programma specifico).
Si ricorda che è richiesta una frequenza obbligatoria per almeno i 2/3 delle lezioni.
Non sono previste modalità di esame da non frequentante se non per gli studenti con iscrizione part-time (che devono prendere contatto con il docente all'inizio del corso per concordare un programma specifico).
Modalità di verifica apprendimento
Esame orale di circa 45 minuti; il colloquio consta di tre argomenti, uno
scelto dal discente. Il voto risulta dalla media dei voti riportati nella
trattazione dei singoli argomenti. L'esame orale deve verificare che il
discente padroneggi i calcoli logici di Gentzen e le loro proprietà
fondamentali, applicandole a qualche semplice problema.
scelto dal discente. Il voto risulta dalla media dei voti riportati nella
trattazione dei singoli argomenti. L'esame orale deve verificare che il
discente padroneggi i calcoli logici di Gentzen e le loro proprietà
fondamentali, applicandole a qualche semplice problema.
Programma del corso
1) Complementi di logica proposizionale e predicativa (per es. forme
normali, completezza funzionale, teoremi di Skolem e Herbrand; logica
monadica).
2) Introduzione alla teoria della dimostrazione: l'approccio analitico alla
logica mediante i calcoli logici di Gentzen (formulazione G3). Il caso
proposizionale intuizionista (un calcolo con la proprietà di terminazione).
Prova dell’Hauptsatz a livello elementare e proprieà della sottoformula.
Interpolazione: il lemma di Maehara, il teorema di Craig e qualche
applicazione. Hauptsatz e contenuto computazionale. Preliminari formali.
Maggiorazione di derivazioni e intepretazioni asimmetriche. Il teorema di
Parsons-Mints-Takeuti e suoi raffinamenti. Hauptsatz e astrazione: il
paradosso di Russell e la teoria della dimostrazione. Un sistema classico
predicativo. Un sistema non classico impredicativo (calcolo logico di
Grishin). Introduzione al lambda calcolo tipato. Nozioni di base e
proprietà fondamentali. Normalizzazione forte e sue applicazioni.
normali, completezza funzionale, teoremi di Skolem e Herbrand; logica
monadica).
2) Introduzione alla teoria della dimostrazione: l'approccio analitico alla
logica mediante i calcoli logici di Gentzen (formulazione G3). Il caso
proposizionale intuizionista (un calcolo con la proprietà di terminazione).
Prova dell’Hauptsatz a livello elementare e proprieà della sottoformula.
Interpolazione: il lemma di Maehara, il teorema di Craig e qualche
applicazione. Hauptsatz e contenuto computazionale. Preliminari formali.
Maggiorazione di derivazioni e intepretazioni asimmetriche. Il teorema di
Parsons-Mints-Takeuti e suoi raffinamenti. Hauptsatz e astrazione: il
paradosso di Russell e la teoria della dimostrazione. Un sistema classico
predicativo. Un sistema non classico impredicativo (calcolo logico di
Grishin). Introduzione al lambda calcolo tipato. Nozioni di base e
proprietà fondamentali. Normalizzazione forte e sue applicazioni.