Please use this identifier to cite or link to this item: http://hdl.handle.net/2307/5024
Title: On proofs and types in second order logic
Authors: Pistone, Paolo
Advisor: Abrusci, Vito Michele
Keywords: proof theory
type theory
second order logic
Issue Date: 27-Mar-2015
Publisher: Università degli studi Roma Tre
Abstract: In questa tesi sono considerate alcune questioni riguardanti la teoria della dimostrazione della logica del secondo ordine e della sua controparte costruttiva, il Sistema F (Girard 1971). Le analisi sviluppate ruotano attorno al tema centrale della apparente “circolarità” delle dimostrazioni del secondo ordine, che si riflette nella possibilità di tipare nel Sistema F forme di auto-applicazione, laddove la diagnosi di Russell era che i tipi dovessero servire a eliminare i \circoli viziosi" (Poincaré 1900) che emergono dall'applicazione di una funzione a se stessa. Lo studio di tale sistema costituisce dunque il punto di partenza di una ricerca incentrata su risultati e prospettive logiche molto spesso ignorate dalla letteratura filosofica sul secondo ordine. L'analisi delle circolarità è condotta sulla base di una distinzione metodologica tra due approcci in teoria della dimostrazione: quello della giustificazione (“le pourquoi", Girard 2000), indirizzato alle dimostrazioni di coerenza e all'Hauptsatz, e quello della comprensione (“le comment", Girard 2000), indirizzato alla caratterizzazione della struttura combinatoria delle prove (viste come entità computazionali, o programmi). Particolare interesse è rivolto, in questa seconda prospettiva, all'analisi di prove scorrette o paradossi, come il paradosso di Girard. Nella prima parte della tesi, dedicata al “pourquoi", gli argomenti tradizionali sui “circoli viziosi" sono confrontati con la prospettiva che emerge dalla dimostrazione dell'Hauptsatz per la logica del secondo ordine (ottenuta in Girard 1971 attraverso la tecnica dei candidati di riducibilità). Nella seconda parte della tesi, dedicata al “comment", sono proposti due approcci combinatori ai “circoli viziosi", con alcuni risultati tecnici: il primo basato sulla teoria del polimorfismo parametrico, il secondo sull'analisi geometrica del tipaggio ottenuta attraverso la teoria dell'unificazione.
URI: http://hdl.handle.net/2307/5024
Access Rights: info:eu-repo/semantics/openAccess
Appears in Collections:Dipartimento di Filosofia, Comunicazione e Spettacolo
T - Tesi di dottorato

Files in This Item:
File Description SizeFormat
Tesi Pistone.pdf1.98 MBAdobe PDFView/Open
Show full item record Recommend this item

Page view(s)

79
Last Week
0
Last month
0
checked on Mar 28, 2024

Download(s)

104
checked on Mar 28, 2024

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.