Source: http://www.federica.unina.it/smfn/calcolabilita-complessita/decidibilita-teorie-logiche-2/
Timestamp: 2019-02-18 09:48:13+00:00

Document:
Decidibilità delle teorie logiche, Aniello Murano « Calcolabilità e Complessità « Scienze Matematiche Fisiche e Naturali « Federica e-Learning
Aniello Murano » 11.Decidibilità delle teorie logiche
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.
Esempi di affermazioni matematiche
Esempi di affermazioni matematiche sono riportati in figura.
La prima formula asserisce che esistono infiniti numeri primi. Questa affermazione è nota essere vera dal tempo di Euclide (più di 2300 anni fa).
La seconda formula corrisponde all’ultimo teorema di Fermat che è stato dimostrato pochi anni fa ad opera di Andrew Wiles.
La terza formula asserisce che esistono infinite coppie di numeri primi che differiscono di solo due unità. Questa è solo una congettura ed è tuttora non dimostrata ne confutata.
Nota: Spiegheremo formalmente il loro significato nelle prossime diapositive…
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, ∃, R1, …, Rk}
Λ, 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;
R1, …, Rk sono relazioni.
Una formula è una stringa sull’alfabeto dato.
Una stringa della forma Ri(xi, . . ., xj) è 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 xi [f] oppure \forall xi [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.
Formule ben Formate:
R1(x1) Λ R2(x1, x2, x3)
\forall x1[R1(x1) Λ R(x1, x2, x3)]
\forall x1\exists x2 \exists x3[R1(x1) Λ R2(x1, x2, x3)]
Osservazione: solo l’ultima fbf è una sentenza.
L’ultima si legge, per ogni x1 esistono x2 e x3 tali che R1(x1) e R2x1, x2, x3 sono veri.
Logica del primo ordine (segue)
Costruendo tale sistema possiamo ragionare su sentenze del tipo
\forall q, \exists x, y[p>q Λ (x,y>1 → xy ≠ p)]. (infiniti numeri primi)
\forall a, b, c, n[(a,b,c>0 Λ n>2) → an + bn ≠ cn]. (ultimo teorema di Fermat)
\forall q \exists p \forall x, y[p>q Λ (x,y>1 →(xy ≠ p Λ xy ≠ p+2))]. (congettura sui numeri primi gemelli)
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.
sia ∑ = {Λ, V, e ¬, (, ), \forall, \exists, x,R1(· , ·)}.
Un modello per questa logica è M1 = (N,≤), con x → N and R1 →≤.
N è l’universo e la relazione ≤ ε N x N è l’interpretazione per il simbolo di relazione binaria R1.
Data una logica e un modello, possiamo verificare se una particolare sentenza è vera nel modello.
Data la logica ∑ = {Λ, V, e ¬, (, ), \forall, \exists, x,R1(· , ·)}, col modello M1 = (N,≤).
Possiamo chiederci se la sentenza \forall x \exists y[R1(x, y) V R1(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.
Data la logica ∑ = {Λ, V, e ¬, (, ), \forall, \exists, x,R1(· , ·)}, col modello M2 = (N,<).
Possiamo dire che la sentenza \forall x \forall y[R1(x, y) V R1(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.
Data la logica ∑ = {Λ, V, e ¬, (, ), \forall, \exists, x,R1(· , ·)}, col modello M3 = (R,+) e R1 relazione ternaria.
Possiamo dire che la sentenza \forall y \exists x[R1(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.
Premessa alla prova: operazioni con automi
Sia ∑ = { 00, 01, 10, 11} dove la coppia di nuperi ij rappresenta un elemento di una matrice trasposta 2 x 1 di binari.
Si noti che ogni parola costruita su ∑ rappresenta due numeri binari. Per esempio 00 11 10 10 rappresenta i numeri 0111 e 0100.
Sia A = { w ε ∑* | la prima riga sia uguale alla seconda}.
Esempio: 00 11 00 11 11 11 ε A and ¬( 11 00 10 00 11 01 00 ε A )
Premessa alla prova: operazioni con automi (segue)
Sia ∑ = {000, 001, 010, 011, 100, 101, 110, 111}.
Si consideri il seguente linguaggio:
B = { w ε ∑* | la somma delle prime due righe è uguale alla terza};
Per esempio, 001 110 011 ε B, mentre ¬ (001 110 010 001 ε B).
Prova di decidibilità di Th(N,+)
Sia φ=Q1x1 … Qnxn(ψ) una sentenza di Th(N,+), dove
ciascun Qi è un quantificatore esistenziale (∃) o universale (∀)
ψ non ha quantificatori.
Sia inoltre φi = Qixi … Qnxn(ψ). In particolare siano φ0 = φ e φn = ψ.
Sia ∑i l’alfabeto di tutte le parole binarie di lunghezza ì.
Si costruisca An su ∑n che accetti tutte le parole che rendano vera φn = ψ.
…….Si noti che ψ non ha quantificatori e solo operazioni di somma.
Si costruisca Ai a partire da Ai+1, nel seguente modo:
Si assuma che Qi sia esistenziale. Allora costruire Ai in modo da fare una scelta non deterministica sull’i+1-esimo elemento di ∑.
Se Qi è universale, allora a fronte della equivalenza ∀xi+1 φi+i = ¬∃xi+1 ¬φi+i si costruisce prima il complemento di Ai+1 poi si applica il procedimento precedente per Qi esistenziale e poi si complementa l’automa ottenuto.
L’automa A0 accetta qualche input se e solo se φ0 = φ è vera.
Dunque, l’ultimo passo dell’algoritmo è testare il vuoto A0.
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 ATM alla teoria Th(N,+,x).
Teorema: la collezione di sentenze provabili in Th(N,+,x) è Turing-riconoscibile.
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.”

References: sentenza 
 sentenza 
 sentenza 
 sentenza 
 sentenza 
 sentenza 
 sentenza 
 sentenza 
 sentenza 
 sentenza