Teorema di Church
Il teorema di Church, dimostrato dal matematico Alonzo Church, nel 1936, afferma che la logica predicativa è indecidibile. In realtà, è quasi un corollario della soluzione di Alan Turing al problema della fermata, uno dei 23 problemi di Hilbert.
Enunciato: Non esiste nessuna macchina di Turing in grado di determinare se una formula della logica predicativa è valida oppure no.
Dimostrazione: Procediamo per assurdo. Se una tale macchina esistesse, potrebbe dimostrare che
- «esistono C ed r tali che C è il calcolo del risultato r a partire dai dati d e dal programma p»
Il tutto perché possiamo esprimere dati e programmi in logica predicativa. Più precisamente
- la n-esima cifra binaria di un dato viene codificata come il valore di verità della n-esima lettera proposizionale di una lista associata al dato in questione;
- un'istruzione si codifica in un'implicazione relativa alle lettere che codificano le cifre dei dati;
- un programma è una congiunzione di istruzioni;
- una configurazione è una congiunzione di dati; e
- un calcolo è una congiunzione di configurazioni, di cui la prima è l'input del programma, e ciascuna delle altre è ottenuta dalla precedente mediante l'applicazione di un'istruzione e l'ultima è l'output del programma, ossia r
Avremmo dunque una macchina che nega il teorema di Turing, e quindi un assurdo. Dunque la logica predicativa è indecidibile.
Un'altra prova dell'indecidibilità della logica predicativa può venire direttamente dal primo teorema di Gödel (ponendolo nello stesso ruolo del teorema di Turing nella dimostrazione soprastante). Infatti, poiché Gödel asserisce che una teoria sufficientemente potente deve contenere un predicato indecidibile, basta applicare questo risultato all'Aritmetica di Robinson, che ha finiti assiomi A1,A2,...,A6. Sia infatti A la congiunzione di questi assiomi (A1∧A2∧A3∧A4∧A5∧A6) e sia B il nostro predicato indecidibile (la cui esistenza è garantita dal teorema di Gödel). Se la logica predicativa potesse dimostrare da sola che A⇒B, ne seguirebbe (per il teorema di deduzione) che nell'aritmetica di Robinson si potrebbe dimostrare B; ma abbiamo definito B proprio come predicato indecidibile. Da qui, l'assurdo e quindi l'indecidibilità della logica predicativa.
Per inciso, la logica predicativa monadica, che comprende anche i sillogismi, è decidibile, come ha dimostrato Löwenhweim nel 1915. Inoltre, si può vedere facilmente che la logica predicativa, in generale, è semidecidibile: è sempre possibile dimostrare la validità di una formula valida, perché l'albero semantico contiene tutti i rami contraddittori ed è finito. Per una formula non valida, invece, qualche ramo non contraddittorio può essere infinito. Possiamo dunque determinare tutte le risposte positive, ma non tutte quelle negative.
Bibliografia[modifica | modifica wikitesto]
- Church, A., A note on the Entscheidungsproblem, «Journal of Symbolic Logic», n° 1, 1936, pag. 40-41
- Turing, A.M., "On Computable Numbers, with an Application to the Entscheidungsproblem", «Proceedings of the London Mathematical Society», Series 2, 42, (1936-37), pp. 230–265.
