Decidibilità: differenze tra le versioni
Contenuto cancellato Contenuto aggiunto
m →Decidibilità in logica matematica: +consistente |
→Decidibilità in logica matematica: espando |
||
Riga 8:
== Decidibilità in logica matematica ==
=== Decidibilità di una teoria ===
Nella [[logica matematica]] una ''teoria'' individuata da un insieme di [[formula ben formata|formule]] di un [[Linguaggio formale (matematica)|linguaggio]] si dice '''decidibile''' se tale insieme di formule è un [[insieme ricorsivo]], cioè esiste un algoritmo che data una qualsiasi formula può stabilire in tempo finito se questa appartiene alla teoria oppure no.
Un esempio di teoria decidibile è la [[logica proposizionale]] (in questo caso l'algoritmo di decisione è quello individuato dalle [[tavole di verità]]).
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]] ¬φ sono [[Teoria del primo ordine#dimostrazioni formali|dimostrabili]] in '''T'''. In caso contrario (se cioè non sono dimostrabili nè φ nè ¬φ) l'enunciato di dice '''indecidibile in T'''.▼
Esempi di teorie non decidibili sono l'[[aritmetica di Peano]], l'[[aritmetica di Robinson]] e la [[ZFC|Teoria degli inziemi di Zermelo - Fraenkel]].
=== 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]] ¬φ sono [[Teoria del primo ordine#dimostrazioni formali|dimostrabili]] in '''T'''. In caso contrario (se cioè non sono dimostrabili nè φ nè ¬φ) l'enunciato di 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.
| |||