decisione, problema della

decisione, problema della

In logica matematica, la ricerca di un procedimento effettivo che consenta di stabilire se una certa proprietà o relazione convenga o no a certi enti. Procedimento ‘effettivo’ significa che esso si deve svolgere in un numero finito di passi ognuno dei quali deve essere descritto in maniera precisa e deve potersi applicare a tutti i problemi dello stesso tipo; per es., quando eseguiamo un’ordinaria moltiplicazione applichiamo un procedimento effettivo. Si chiama poi insieme decidibile un insieme I quando esiste un procedimento effettivo, nel senso sopra detto, per stabilire se un qualunque elemento appartenga o no a I. S’intende per predicato decidibile ogni predicato (cioè ogni proprietà che può convenire o meno a un individuo, oppure una relazione che può sussistere o no tra n individui, e allora si parla di predicato n-adico) quando esiste un procedimento effettivo per stabilire se il predicato conviene o no a ciascun individuo, oppure a ciascun gruppo di n individui. Il requisito di effettività del procedimento è equivalente a quello di eseguibilità con un computer. Per i sistemi formali deduttivi della logica matematica il problema della d. può essere posto sotto due diversi aspetti: (1) se sia decidibile l’insieme degli assiomi, e in questo caso la teoria è più comunemente detta teoria assiomatica; (2) se sia decidibile l’insieme dei teoremi, e in questo caso si parla di teoria decidibile (altrimenti essa si dice indecidibile). Risulta da un fondamentale teorema di Church del 1936 che l’insieme dei teoremi della logica classica del primo ordine (o calcolo dei predicati) è indecidibile; data una qualunque espressione E del linguaggio della logica del primo ordine, non si è in grado di stabilire, in un numero finito di passi, se E sia o no un teorema. In conclusione, data una qualsiasi espressione logica, non sempre si può stabilire con un procedimento effettivo se essa sia conseguenza degli assiomi della teoria del primo ordine a cui si riferisce.