• 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

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à.