Aniello Murano » 11.Decidibilità delle teorie logiche

Prefazione

Nelle lezioni precedenti abbiamo trattato il concetto di decidibilià e indecidibilità nella teoria della computabilità.
In questo contesto, possiamo dire che un insieme A è detto decidibile o ricorsivo se esiste un algoritmo che ricevuto in input un qualsiasi elemento, termina restituendo in output 0 o 1 a seconda che il valore appartenga o no all’insieme A.
In questa lezione tratteremo la decidibilità e l’indecidibilità di teorie nella logica matematica.
In particolare, concentreremo la nostra attenzione sul problema di determinare se affermazioni matematiche sono vere o false e investigheremo la decidibilità di questo problema.
Si vedrà che la decidibilità dipende dal particolare dominio matematico in cui le affermazioni sono descritte.

Dalle logiche ai linguaggi

Al fine di automatizzare il processo di determinazione di verità delle affermazioni matematiche è utile considerare queste affermazioni come stringhe e definire un linguaggio formato da tutte le affermazioni vere.
Il problema della determinazione di verità delle affermazioni si riduce a alla decidibilità di questo linguaggio.

Definizione del linguaggio

Per la definizione del linguaggio si consideri il seguente alfabeto: {Λ, V, ¬, (,), ∀, x, ∃, R₁, …, R_k}

• Λ, V, e ¬, corrispondo alle operazioni booleane and,or e not;
• “(” e “)” sono le parentesi;
• \forall ed \exists sono i quantificatori universale ed esistenziale;
• x denota variabili;
• R₁, …, R_k sono relazioni.

Una formula è una stringa sull’alfabeto dato.
Una stringa della forma R_i(x_i, . . ., x_j) è una formula atomica. Il valore j è l’arità della relazione Ri.
Una formula (ben formata), (in breve fbf)

• è una formula atomica,
• è una combinazione booleana di altre formule più piccole,
• è una quantificazione su altre formule f del tipo \exist x_i [f] oppure \forall x_i [f].

Nota:I quantificatori legano le variabili all’interno del loro “scope” (parentesi quadre). Se una variabile non è legata in una formula allora la variabile è chiamata libera. Le formule senza variabili libere sono chiamate sentenze o statements.

Logica del primo ordine

Formule ben Formate:

• R₁(x1) Λ R₂(x1, x2, x3)
• \forall x₁[R₁(x₁) Λ R(x₁, x₂, x₃)]
• \forall x₁\exists x₂ \exists x₃[R₁(x₁) Λ R₂(x₁, x₂, x₃)]

Osservazione: solo l’ultima fbf è una sentenza.
L’ultima si legge, per ogni x₁ esistono x₂ e x₃ tali che R₁(x₁) e R₂x₁, x₂, x₃ sono veri.

Logica del primo ordine (segue)

Costruendo tale sistema possiamo ragionare su sentenze del tipo

1. \forall q, \exists x, y[p>q Λ (x,y>1 → xy ≠ p)]. (infiniti numeri primi)
2. \forall a, b, c, n[(a,b,c>0 Λ n>2) → an + bn ≠ cn]. (ultimo teorema di Fermat)
3. \forall q \exists p \forall x, y[p>q Λ (x,y>1 →(xy ≠ p Λ xy ≠ p+2))]. (congettura sui numeri primi gemelli)

Logica del primo ordine (segue)

Per avere senso, una logica ha bisogno che le venga assegnato un significato. Per fare questo, abbiamo bisogno di assegnare la sintassi a uno specifico costrutto matematico, chiamato modello.

Un modello è composto da un universo e un insieme di relazioni, una per ogni simbolo di relazione nella logica.

Esempio:

• sia ∑ = {Λ, V, e ¬, (, ), \forall, \exists, x,R₁(· , ·)}.
• Un modello per questa logica è M₁ = (N,≤), con x → N and R1 →≤.
• N è l’universo e la relazione ≤ ε N x N è l’interpretazione per il simbolo di relazione binaria R₁.

Logica del primo ordine (segue)

Data una logica e un modello, possiamo verificare se una particolare sentenza è vera nel modello.

Esempio 1:
Data la logica ∑ = {Λ, V, e ¬, (, ), \forall, \exists, x,R₁(· , ·)}, col modello M₁ = (N,≤).
Possiamo chiederci se la sentenza \forall x \exists y[R₁(x, y) V R₁(y, x)] è vera.
Chiaramente la sentenza è vera, visto che per ogni assegnamento x → a e y → b per a, b ε N, abbiamo che a ≤ b or b ≤ a.

Esempio 2:
Data la logica ∑ = {Λ, V, e ¬, (, ), \forall, \exists, x,R₁(· , ·)}, col modello M₂ = (N,<).
Possiamo dire che la sentenza \forall x \forall y[R₁(x, y) V R₁(y, x)] non è vera. Questo perché per l’assegnamento x → a e y → a con a ε N abbiamo a < a or a < a, che è chiaramente falso.

Esempio 3:
Data la logica ∑ = {Λ, V, e ¬, (, ), \forall, \exists, x,R₁(· , ·)}, col modello M₃ = (R,+) e R₁ relazione ternaria.
Possiamo dire che la sentenza \forall y \exists x[R₁(x, x, y)] è vera. Infatti per ogni assegnamento x → a e y → b con a, b ε R abbiamo che +(a, a, b), o nella classica notazione matematica b = a + a, è vera. Falso se il dominio è N.

Una teoria decidibile

Sia M un modello. Diremo che la collezione di tutte le sentenze vere sotto quel modello è la teoria del modello e scriveremo Th(M).

Teorema: la teoria Th(N,+) è decidibile.

Cosa significa che una teoria è decidibile? Significa che noi possiamo decidere se una particolare sentenza appartiene alla teoria o no. Quindi possiamo trattare la teoria Th(N,+) come un linguaggio e possiamo costruire un decisore per questo linguaggio.
Consideriamo la sentenza \forall x \exists y[y = x + x]. Questa sentenza è vera ed è anche un elemento della teoria Th(N,+).
Consideriamo ora \exists x \forall y[y = x + x]. Questa sentenza è falsa è quindi non è un membro della teoria.
È possibile mostrare la decidibilità della teoria Th(N,+) costruendo un automa finito che decide il linguaggio.

Prova di decidibilità di Th(N,+)

Sia φ=Q₁x₁ … Q_nx_n(ψ) una sentenza di Th(N,+), dove

• ciascun Q_i è un quantificatore esistenziale (∃) o universale (∀)
• ψ non ha quantificatori.

Sia inoltre φ_i = Q_ix_i … Q_nx_n(ψ). In particolare siano φ₀ = φ e φ_n = ψ.
Sia ∑_i l’alfabeto di tutte le parole binarie di lunghezza ì.
Si costruisca A_n su ∑_n che accetti tutte le parole che rendano vera φ_n = ψ.
…….Si noti che ψ non ha quantificatori e solo operazioni di somma.
Si costruisca A_i a partire da A_i+1, nel seguente modo:
Si assuma che Q_i sia esistenziale. Allora costruire A_i in modo da fare una scelta non deterministica sull’i+1-esimo elemento di ∑.
Se Q_i è universale, allora a fronte della equivalenza ∀x_i+1 φ_i+i = ¬∃x_i+1 ¬φ_i+i si costruisce prima il complemento di A_i+1 poi si applica il procedimento precedente per Q_i esistenziale e poi si complementa l’automa ottenuto.
L’automa A₀ accetta qualche input se e solo se φ₀ = φ è vera.
Dunque, l’ultimo passo dell’algoritmo è testare il vuoto A₀.

Una teoria non decidibile

Il seguente teorema ha delle conseguenze filosofiche molto profonde.
Esso mostra che la matematica non può essere “meccanizzata”.
Mostra inoltre che alcuni problemi nella teoria dei numeri non sono algoritmici, cosa che provocò una grande sorpresa nei matematici all’inizio del 1900.
Allora infatti si credeva che tutti i problemi matematici potessero essere risolti algoritmicamente e che bisognasse solo trovare l’algoritmo per risolvere un dato problema.

Teorema: la teoria Th(N,+,x) è indecidibile.

Questo significa che non esiste un algoritmo che si ferma su tutte le sentenze φ sull’alfabeto appropriato. Quello che più sorprende è la semplicità della struttura di questa logica indecidibile.
Questo vuol dire che ci sono delle fondamentali limitazioni algoritmiche nella matematica.
La dimostrazione si ottiene tramite una riduzione del problema A_TM alla teoria Th(N,+,x).

Teorema di incompletezza

Teorema: la collezione di sentenze provabili in Th(N,+,x) è Turing-riconoscibile.

Dimostrazione:

• il seguente algoritmo P accetta il suo input φ se e solo se φ è dimostrabile.
• L’algoritmo P prova tutte le possibili stringhe come candidate per una prova π di φ usando un “proof checker” (verificatore della prova).
• Se viene trovata una stringa che è una prova, allora l’algoritmo accetta.

Teorema di incompletezza (segue)

Teorema (di incompletezza di Kurt Gödels): alcune sentenze vere in Th(N,+,x) non sono dimostrabili.

Con qualche semplificazione, questo teorema afferma che:
“In ogni formalizzazione coerente della matematica che sia sufficientemente potente da poter assiomatizzare la teoria elementare dei numeri naturali — vale a dire, sufficientemente potente da definire la struttura dei numeri naturali dotati delle operazioni di somma e prodotto — è possibile costruire una proposizione sintatticamente corretta che non può essere né dimostrata né confutata all’interno dello stesso sistema.”