teoremi di indecidibilita
teoremi di indecidibilità
In logica matematica, risultati che affermano che una data teoria formalizzata T non è decidibile, vale a dire non ammette un algoritmo in grado di stabilire in modo meccanico per ogni formula del linguaggio se è teorema o meno di T. Prototipo di questi risultati è il teorema di Gödel (1931), il quale afferma che l’aritmetica di Peano del primo ordine è indecidibile. Il risultato si può estendere a teorie molto più deboli dell’aritmetica di Peano – quale il sistema Q di Robinson – e in generale a ogni teoria, di qualunque tipo di linguaggio, presentabile in modo ricorsivo in cui risultino rappresentabili funzioni e predicati ricorsivi e si possa aritmetizzare la sintassi della teoria medesima. Il fatto che Q sia finitamente assiomatizzata ci permette di concludere che la logica elementare è indecidibile – come del resto ogni estensione finita di una teoria indecidibile – e che non esiste calcolo per la logica d’ordine superiore. Mediante il metodo dell’interpretazione, da sistemi aritmetici la indecidibilità si può trasferire a teorie in cui una parte sufficiente dell’aritmetica, per es. Q, si possa interpretare. È questo il caso della teoria dei numeri reali al secondo ordine o anche al secondo ordine debole, la teoria elementare dei reali con la funzione sen, la teoria dei gruppi e così via. Ma la tecnica si può generalizzare e applicare a teorie molto varie e matematicamente interessanti. Su un piano diverso si pongono quei risultati di indecidibilità che non riguardano direttamente teorie formalizzate, per es., il problema della fermata per macchine di Turing, il problema della lambda-convertibilità o quello della derivabilità di parole entro sistemi di Post e così via. Di fatto questi problemi risultano intertraducibili con questioni sull’indecidibilità di frammenti dell’aritmetica, una volta che siano codificati in termini numerici oggetti e procedure. Questo vale anche per problemi di grande interesse matematico come il problema della parola per gruppi finitamente presentati o, più in generale, per algebre finitamente presentate. L’indecidibilità del problema della parola per gruppi è stata dimostrata nel 1955 da Sergeij Novikov e William Boone e successivamente semplificata da una parte da John Britton (1963), dall’altra da Graham Higman (1961). In questo nuovo contesto essa non è che un corollario di un risultato più generale che stabilisce che un gruppo finitamente generato si immerge in un gruppo finitamente presentato se, e soltanto se, l’insieme delle relazioni del gruppo è ricorsivamente enumerabile, rendendo così esplicita l’analogia con i problemi di assiomatizzabilità e decidibilità per teorie. Su un altro versante si pone il teorema dimostrato da Yuri Matijasevic (1968), il quale prova che non esiste un algoritmo in grado di stabilire quando un polinomio a coefficienti interi ha o meno soluzione intera, rispondendo così al decimo problema posto da Hilbert nel 1900. Entrambi i risultati suddetti – assieme a quello di Gödel – non sono che gli esempi più sorprendenti di tutta un’area di ricerca che riguarda tanto le teorie formalizzate che problemi di contenuto più esplicitamente matematico.