ETD system

Electronic theses and dissertations repository

 

Tesi etd-05032016-104203


Thesis type
Elaborati finali per laurea triennale
Author
GRILLETTI, GIANLUCA
email address
grilletti@mail.dm.unipi.it,grilletti.gianluca@gmail.com
URN
etd-05032016-104203
Title
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&#39;intuizionismo. La differenza principale rispetto alla matematica classica è il concetto di ``verità&#39;&#39;. Mentre da un punto di vista classico il fatto che una proprietà sia ``vera&#39;&#39; è indipendente dal fatto che questa sia dimostrabile o meno, per un matematico intuizionista ``vero&#39;&#39; coincide con ``dimostrabile&#39;&#39;.<br> <br>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&#39;&#39; 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.<br> <br>Nel caso specifico dell&#39;\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))$.<br> <br>Il vantaggio dell&#39;aritmetica intuizionista rispetto a quella classica è quindi dato dal poter tradurre \emph{dimostrazioni} in \emph{algoritmi}.<br> <br>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&#39;aritmetica classica sono \emph{codificati} all&#39;interno di quella intuizionista tramite una opportuna traduzione delle formule, l&#39;\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$.<br><br>Questo ci dice che $HA$ dimostra meno teoremi di $PA$, ma contiene le stesse \emph{informazioni}.<br> <br>Raccogliendo i risultati qui esposti, si possono ricavare informazioni costruttive anche a partire da una dimostrazione di $PA$.<br> <br>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&#39;interpretazione negativa è che $f$ risulta essere un \emph{funzionale ricorsivo di Gödel}, e si ha quindi una stima della sua complessità.
File