Sistemi deduttivi in teoria della dimostrazione e didattica

L’integrazione tra formalizzazione logica e analisi didattica ha radici molto profonde. La presente tesi magistrale si propone di formalizzare tre sistemi deduttivi fondamentali: la Deduzione Naturale, i Sistemi Assiomatici e il Calcolo dei Sequenti, nelle logiche proposizionale e di primo ordine. L’analisi si concentra sull'equivalenza dei tre sistemi e sulla comprensione e formalizzazione delle loro proprietà di correttezza e completezza, ponendo particolare attenzione al loro ruolo nell’ambito della didattica delle dimostrazioni. Si esamina come proporre, in linea con le Indicazioni Nazionali, le dimostrazioni agli studenti e come esse siano percepite, evidenziando il rapporto tra spiegazione e argomentazione. Si esplora inoltre il collegamento di tali sistemi con i proof assistant, che rappresentano una nuova frontiera nell’ambito della verifica formale delle dimostrazioni. Si approfondisce l’analisi nel caso dell’implicazione logica, con particolare attenzione alla distinzione tra linguaggio naturale e formale. Si discute la natura delle regole di inferenza, focalizzandosi sul modus ponens e sulla distinzione essenziale tra implicazione e deduzione. Questo lavoro mira a fornire una base solida per comprendere e utilizzare in modo efficace i sistemi deduttivi nella pratica matematica e nell’insegnamento.