logo SBA

ETD

Archivio digitale delle tesi discusse presso l’Università di Pisa

Tesi etd-10282020-222542


Tipo di tesi
Tesi di laurea magistrale
Autore
SABATINI, ANDREA
Indirizzo email
a.sabatini3@studenti.unipi.it, sbt.ndr95@gmail.com
URN
etd-10282020-222542
Titolo
On second-order logic from an algorithmic viewpoint
Dipartimento
CIVILTA' E FORME DEL SAPERE
Corso di studi
FILOSOFIA E FORME DEL SAPERE
Relatori
relatore Prof. Moriconi, Enrico
correlatore Prof. Piazza, Mario
Parole chiave
  • Curry-Howard correspondence
  • impredicativity
  • second-order logic
Data inizio appello
16/11/2020
Consultabilità
Completa
Riassunto
This thesis focuses on Girard/Reynolds system F, an extension of simply-typed lambda-calculus which can be treated as a prototypical programming language in the functional paradigm for polymorphism and as a computational interpretation of second-order (intuitionistic) logic and arithmetic. After a detailed exam of the expressive power of F, we present a reducibility argument for strong normalization of F (a result which is the Curry-Howard analogue of consistency for second-order intuitionistic logic and arithmetic). The realizability interpretation of F which stems from this argument is further refined, in order to obtain a non-circular reading of polymorphism (the Curry-Howard analogue of impredicative quantification) of autonomous philosophical interest. Turning attention to higher-order extensions of F, we show how to reformulate a positive solution to Takeuti's conjecture in Curry-Howard style, and how can we go paradoxical by admitting higher-order impredicativity. Particular emphasis is given to an (allegedly) original reformulation of Russell intensional paradox in an intuitionistic setting.
File