Decidibilità: differenze tra le versioni
Contenuto cancellato Contenuto aggiunto
m Bot: Aggiungo: cs:Nezávislé tvrzení, ru:Независимость системы аксиом Tolgo: fr:Indécidabilité |
m WikiCleaner 0.99 - |
||
Riga 15:
=== Decidibilità di una formula in una teoria ===
Nella [[logica matematica]] un enunciato rappresentato da una [[formula ben formata]] φ di una [[teoria del primo ordine]] '''T''' si dice '''decidibile in T''' se o φ o la sua [[negazione (matematica)|negazione]] ¬φ sono [[Teoria del primo ordine#Dimostrazioni formali|dimostrabili]] in '''T'''. In caso contrario (se cioè non sono dimostrabili né φ né ¬φ) l'enunciato si dice '''indecidibile 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 [[consistenza (logica matematica)|consistenti]]. I [[teoremi di incompletezza di Gödel]] forniscono una procedura con cui data una qualunque teoria consistente '''T''' in grado di [[funzione rappresentabile|rappresentare]] le operazioni di addizione e moltiplicazione sui [[numeri naturali]] è possibile costruire enunciati indecidibili da '''T'''. Le [[formula ben formata|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.
| |||