# Teorema di Matijasevič

Il teorema di Matijasevič, dimostrato nel 1970 da Jurij Vladimirovič Matijasevič, implica che il decimo problema di Hilbert è irrisolvibile. Il problema richiede la costruzione di un algoritmo generale che sia in grado di stabilire se un dato sistema di equazioni diofantee (polinomi a coefficienti interi) ha soluzioni intere. David Hilbert ha posto il problema durante il suo discorso del 1900 al Congresso Internazionale dei Matematici.

## Descrizione

Un sistema tipico di equazioni diofantee assomiglia a questo:
    $3x^{2}-7y^{2}z^{3}=18$
    $-7y^{2}+8z^{2}=0$
Il problema è stabilire se esistono degli interi x, y e z che soddisfano entrambe le equazioni simultaneamente. Si vede che questo problema è equivalente a quello di stabilire se una singola equazione diofantea in più variabili ha soluzioni nell'insieme dei numeri interi. Ad esempio, il sistema precedente è risolvibile negli interi se e solo se la seguente equazione è risolvibile nell'insieme dei numeri naturali:
    (3(x$_1$ − x$_2$)$^2$ − 7(y$_1$ − y$_2$)$^2$(z$_1$ − z$_2$)$^3$ − 18)$^2$ + (−7(y$_1$ − y$_2$)$^2$ + 8(z$_1$ − z$_2$)$^2$)$^2$ = 0.
Matiyasevich ha usato un trucco ingegnoso che coinvolge i numeri di Fibonacci per mostrare che le soluzioni delle equazioni diofantee possono crescere esponenzialmente. I lavori precedenti di Julia Robinson, Martin Davis e Hilary Putnam hanno mostrato che questo è sufficiente a mostrare che non può esistere nessun algoritmo capace di decidere la risolubilità delle equazioni diofantee.
Lavori successivi hanno mostrato che il problema della risolubilità è indecidibile anche se l'equazione ha solo 9 variabili naturali (Matiyasevich, 1977) o 11 variabili intere (Zhi Wei Sun, 1992).
Il teorema di Matijasevič stesso è molto più forte della insolubilità del Decimo Problema. Infatti dice:
    Ogni insieme ricorsivamente enumerabile è diofanteo.
Un insieme S di interi è ricorsivamente enumerabile se esiste un algoritmo che si comporta nel seguente modo: dato come input un intero n, se n è un elemento di S, allora l'algoritmo alla fine termina; altrimenti non termina mai. questo è equivalente a dire che esiste un algoritmo che non termina mai e che elenca gli elementi di S. Un insieme S è diofanteo se esiste un certo polinomio a coefficienti interi f(n, x$_1$, ..., x$_k$) tale che un intero n è in S se e solo se esistono degli interi x$_1$, ..., x$_k$ tali che f(n, x$_1$, ..., x$_k$) = 0.
Non è difficile vedere che ogni insieme diofanteo è ricorsivamente enumerabile: si consideri una equazione diofantea f(n, x$_1$, ..., x$_k$) = 0. Ora costruiamo un algoritmo che semplicemente prova tutti i possibili valori per n, x$_1$, ..., x$_k$ e scrive n ogni volta che f(n, x$_1$, ..., x$_k$) = 0. Questo algoritmo ovviamente non termina mai ed elenca esattamente gli n per i quali f(n, x$_1$, ..., x$_k$) = 0 ha una soluzione in x$_1$, ..., x$_k$.
Il teorema di Matijasevič, insieme a un risultato scoperto negli anni 1930 implica che la soluzione al decimo problema di Hilbert è impossibile. Il risultato scoperto negli anni 1930 da molti logici si può formulare nel seguente modo: "esistono insiemi ricorsivamente enumerabili non ricorsivi". In questo contesto, un insieme S di interi è detto "ricorsivo" se esiste un algoritmo che, dato come input un intero n, ritorna come output una risposta si/no corretta alla domanda: "n è un elemento di S?" Da questo segue che esistono equazioni diofantee che non possono essere risolte da nessun algoritmo, a meno che non si possa costruire un ipercomputer (Kieu, 2003); comunque questa possibilità è ritenuta generalmente non implausibile fisicamente.
Il teorema di Matijasevič è stato usato successivamente per provare l'insolubilità di molti problemi riguardanti l'analisi e le equazioni differenziali.
Si può anche derivare la seguente forma (più forte) del teorema di incompletezza di Gödel dal risultato di Matijasevič:
    Per ogni assiomatizzazione data della teoria dei numeri è possibile costruire esplicitamente una equazione diofantea priva di soluzioni, ma tale che questo fatto non si può provare all'interno dell'assiomatizzazione data.