Decidibilità (logica matematica)
Da Wikipedia, l'enciclopedia libera.
Il concetto di decidibilità di un enunciato è proprio della logica matematica.
Un enunciato rappresentato da una formula ben formata φ di una teoria del primo ordine T si dice indecidibile in T se nè φ nè la sua negazione ¬φ sono dimostrabili in T.
Esempi classici di enunciati indecidibili sono dati dal teorema di Goodstein per l'aritmetica di Peano e dall'ipotesi del continuo per la teoria assiomatica degli insiemi. Tali enunciati sono stati dimostrati indecidibili sotto l'ipotesi che le teorie in questione siano consistenti. I teoremi di incompletezza di Gödel forniscono una procedura con cui data una qualunque teoria T in grado di rappresentare le operazioni di addizione e moltiplicazione sui numeri naturali è possibile costruire enunciati indecidibili da T. Le formule associate a tali enunciati tuttavia sono talmente lunghe e complesse che la loro scrittura esplicita nel linguaggio del primo ordine è di fatto impossibile da realizzare sia per un uomo sia per un computer.