Decidibilità

Il concetto di decidibilità si trova in logica matematica e in teoria della computabilità con accezioni differenti.

Decidibilità in teoria della computabilitàModifica

 Lo stesso argomento in dettaglio: Insieme ricorsivo.

Nella teoria della computabilità un sottoinsieme A dell'insieme N dei numeri naturali si dice decidibile o ricorsivo se esiste un algoritmo che ricevuto in input un qualsiasi numero naturale termina restituendo in output 0 o 1 a seconda che il numero appartenga o no all'insieme A. Equivalentemente A è decidibile se la sua funzione caratteristica è una funzione ricorsiva.

Decidibilità in logica matematicaModifica

Decidibilità di una formulaModifica

Nella logica matematica una formula ben formata φ di una teoria del primo ordine T si dice decidibile in T se o φ o la sua negazione ¬φ sono dimostrabili in T. In caso contrario (se cioè non sono dimostrabili né φ né ¬φ) la formula si dice indecidibile in T.

Decidibilità di enunciati in una teoriaModifica

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 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 consistenti. I teoremi di incompletezza di Gödel forniscono una procedura con cui data una qualunque teoria consistente 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.

Decidibilità di una teoriaModifica

Nella logica matematica una teoria individuata da un insieme di formule di un 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à). Esempi di teorie non decidibili sono l'aritmetica di Peano, l'aritmetica di Robinson e la Teoria degli insiemi di Zermelo - Fraenkel.