decidibilita

decidibilita

decidibilità termine utilizzato nella teoria della calcolabilità per indicare l’esistenza di una procedura algoritmica che permetta di stabilire, in un numero finito di passi, se una data proprietà è verificata o meno. Per esempio, un insieme è decidibile se, dato un oggetto a, è possibile stabilire, tramite un algoritmo se a appartiene o non appartiene all’insieme. L’insieme dei numeri primi è un esempio di insieme decidibile, essendo possibile stabilire algoritmicamente, per ogni numero naturale n, se esso è o meno un numero primo. Qualora invece l’algoritmo sia in grado di identificare tutti gli elementi che appartengono all’insieme, ma non quelli che non gli appartengono, l’insieme è detto semidecidibile. Tutti gli insiemi finiti sono decidibili, mentre un insieme infinito è decidibile se e solo se sono semidecidibili sia esso sia il suo insieme complementare. Nel contesto della teoria della ricorsività, gli insiemi decidibili e semidecidibili corrispondono rispettivamente a quelli ricorsivi e ricorsivamente enumerabili.

Una formula ben formata A, in un calcolo logico, si dice decidibile se è possibile dimostrare formalmente o la formula A stessa oppure la sua negazione ￢A.

A una formula ben formata in cui compare la variabile x, indicata con p(x), è possibile associare una funzione ƒ, detta funzione caratteristica di p(x), definita nel modo seguente:

• ƒ(x) = 1, se la formula p(x) è vera;

• ƒ(x) = 0, altrimenti (cioè se la formula è falsa).

Per esempio: se la formula p(x) rappresenta il predicato «x è un numero pari», allora il valore della funzione associata ƒ è 1 in corrispondenza dei numeri pari, mentre è zero in corrispondenza dei numeri dispari (per esempio ƒ(3) = 0, ƒ(14) = 1, …). Occorre sottolineare che, se la formula p(x) è decidibile, allora la funzione ƒ deve essere una funzione calcolabile; per questo motivo il problema della decidibilità è strettamente collegato al tema della calcolabilità di una funzione.

Un calcolo logico è detto decidibile qualora si disponga di un metodo meccanico per stabilire, per una qualsiasi formula ben formata A, se esiste una dimostrazione di A nel calcolo logico dato; un simile metodo è rappresentato, per esempio nel calcolo degli enunciati, dalle tavole di verità. Non bisogna confondere, però, la decidibilità di una formula con la decidibilità di un calcolo. Per esempio il calcolo degli enunciati è decidibile perché per ogni enunciato è possibile stabilire, tramite le tavole di verità, se esso è una tautologia, e quindi se è dimostrabile. Tuttavia non è vero che ogni enunciato è decidibile: basti pensare per esempio a una lettera proposizionale, la quale rappresenta un enunciato atomico, che può essere vero o falso a seconda del valore di verità che gli si attribuisce. Il teorema di Gödel afferma che l’aritmetica formalizzata come calcolo logico (mediante gli assiomi di Peano) è una teoria indecidibile perché esistono in essa formule vere che non sono dimostrabili.