Sistema ETD

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

 

Tesi etd-05032016-104203


Tipo di tesi
Elaborati finali per laurea triennale
Autore
GRILLETTI, GIANLUCA
Indirizzo email
grilletti@mail.dm.unipi.it,grilletti.gianluca@gmail.com
URN
etd-05032016-104203
Titolo
L'interpretazione dialectica di "Gödel"
Struttura
SCIENZE MATEMATICHE, FISICHE E NATURALI
Corso di studi
MATEMATICA
Commissione
relatore Prof. Berarducci, Alessandro
Parole chiave
  • arithmetic of all finite types
  • sistema t
  • t system
  • aritmetica intuizionistica
  • intuitionistic arithmetic
  • aritmetica di Heyting
  • Heyting arithmetic
  • interpretazione negativa
  • negative interpretation
  • aritmetica dei tipi finiti
  • intuitionistic logic
  • logica intuizionistica
  • logica
  • logic
  • finitismo
  • costruttivismo
  • constructivism
  • finitism
Data inizio appello
19/09/2014;
Consultabilità
completa
Riassunto analitico
Nella prima metà del ventesimo secolo nasceva in Europa una nuova corrente della filosofia matematica: l'intuizionismo. La differenza principale rispetto alla matematica classica è il concetto di ``verità''. Mentre da un punto di vista classico il fatto che una proprietà sia ``vera'' è indipendente dal fatto che questa sia dimostrabile o meno, per un matematico intuizionista ``vero'' coincide con ``dimostrabile''.

Quello che si ricava da questo è che non è generalmente valido il \emph{principio de terzo escluso} e che le dimostrazioni intuizioniste risultano essere \emph{costruttive}, a differenza di quanto succede nel caso classico. Ad esempio, mostrare che ``vale la congettura di Goldbach oppure esiste $n$ che faccia da controesempio'' classicamente non ci da nessuna informazione sul fatto che tale congettura sia vera o meno, mentre dimostrarla intuizionisticamente significa \emph{provare} la congettura oppure \emph{fornire} un controesempio ad essa.

Nel caso specifico dell'\emph{aritmetica intuizionista} $HA$ si possono ricavare vari risultati di carattere costruttivo. Tra questi si ha che dalla dimostrazione di una formula $\forall x. \exists y. A(x,y)$, si può estrapolare un \emph{programma} per calcolare una funzione $f$ tale che per ogni $n\in \mathbb{N}$ valga $A(n,f(n))$.

Il vantaggio dell'aritmetica intuizionista rispetto a quella classica è quindi dato dal poter tradurre \emph{dimostrazioni} in \emph{algoritmi}.

Abbiamo inoltre che le dimostrazioni intuizioniste sono classicamente accettabili, ma \emph{non} è generalmente vero il viceversa, quindi $HA$ dimostra \emph{meno} formule rispetto a $PA$. Si ha però che tutti i teoremi dell'aritmetica classica sono \emph{codificati} all'interno di quella intuizionista tramite una opportuna traduzione delle formule, l'\emph{interpretazione negativa}. In particolare possiamo associare ad una formula $\phi$ una formula $\phi^N$ in modo che classicamente le due formule siano equivalenti e $PA$ dimostri $\phi$ se e soltanto se $HA$ dimostra $\phi^N$.

Questo ci dice che $HA$ dimostra meno teoremi di $PA$, ma contiene le stesse \emph{informazioni}.

Raccogliendo i risultati qui esposti, si possono ricavare informazioni costruttive anche a partire da una dimostrazione di $PA$.

In particolare, da una dimostrazione classica di una formula $\forall x. \exists y.\phi(x,y)$ con $\phi$ decidibile, è semplice dedurre che esiste una funzione $f$ \emph{calcolabile} tale che per ogni $n\in \mathbb{N}$ valga $\phi(n,f(n))$, ma quello che si ricava utilizzando l'interpretazione negativa è che $f$ risulta essere un \emph{funzionale ricorsivo di Gödel}, e si ha quindi una stima della sua complessità.
File