Decidibilità
# Decidibilità

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

## Decidibilità in teoria della computabilità

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 matematica

### Decidibilità di una formula

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 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 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 teoria

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.

