Completezza, correttezza e indecidibilità
Ciao, amici! Leggo sul mil libro di logica che il calcolo dei predicati nella logica dei predicati del primo ordine è sia corretto (nel senso che le regole generano solo forme argomentative valide\(^1\) in virtù della semantica dei quantificatori, dei connettivi vero-funzionali e del predicato d'identità) che completo (nel senso che esse generano tutte le forme argomentative valide).
D'altra parte leggo anche che la logica dei predicati è indecidibile, cioè che non esiste alcuna procedura algoritmica che permetta di individuare tutte e sole le forme argomentative valide.
C'è qualcosa che mi sfugge.
Qualcuno saprebbe aiutarmi a vederci più chiaro?
$\infty$ grazie a tutti!!!
\(^1\) che so che significa che hanno conclusione vera per ogni struttura interpretativa in cui le premesse sono vere.
D'altra parte leggo anche che la logica dei predicati è indecidibile, cioè che non esiste alcuna procedura algoritmica che permetta di individuare tutte e sole le forme argomentative valide.
C'è qualcosa che mi sfugge.
Qualcuno saprebbe aiutarmi a vederci più chiaro?
$\infty$ grazie a tutti!!!
\(^1\) che so che significa che hanno conclusione vera per ogni struttura interpretativa in cui le premesse sono vere.
Risposte
Mi pare (vado a memoria ed è da un po' di tempo che non metto le mani sulla logica) che la cosa possa essere messa in questi termini (chiaramente per dire tutto alla buona): esiste potenzialmente un algoritmo in grado di produrre tutte e sole le fbf valide, ma data una formula non esiste un algoritmo che partendo da essa permetta di stabilire se questa sia valida o meno; se il tuo algoritmo "sforna-formule-valide" l'ha prodotta, sei certo che sia valida, puoi essere altrettanto sicuro che se è valida verrà prima o poi prodotta dal tuo algoritmo in un numero finito (eventualmente maggiore dell'età dell'universo espressa in decimi di secondo) di iterazioni, ma questo è ben diverso dall'avere un algoritmo che presa una formula ne restituisca la validità o la non validità. Il criterio "se è stata prodotta dall'algoritmo, allora è valida" non permette in alcun modo di stabilire la non validità di una formula, in quanto dovresti aspettare che l'algoritmo abbia prodotto tutte le fbf prima di poter dire "se non è nell'elenco di quelle valide, allora non è valida", ma essendo le formule infinite questo non è possibile. Chiedo scusa per l'estrema imprecisione nell'esporre l'argomento, ma al momento non sarei in grado di essere più formale; credo comunque che il mio discorso contenga tutte le idee necessarie a formalizzare dovutamente la questione (sempre che io ricordi bene).
Per le regole di inferenza del calcolo dei predicati credo, ma soprattutto spero, di esserci.
Per quanto riguarda per esempio per il metodo degli alberi di refutazione, in cui si nega la conclusione per dimostrare che non si dà il caso che le premesse siano vere ed essa falsa, so che una data forma argomentativa oggetto di verifica è valida se e solo se ogni cammino si chiude. In tutti e soli i casi in cui non è valida succede invece che si termina un cammino che rimane aperto o ci si trova da "continuare all'infinito". Qui si tratta di applicare un insieme di regole che resituiscono la validità o l'invalidità di una forma piuttosto che di generare forme.
È a causa della possibile situazione in cui ci si trova a dover continuare all'infinito -cosa di cui però un essere umano (non so una macchina di Turing, di cui ho solo un'idea intuitiva, ma che so che si cita per definire l'indecidibilità) si accorge e conclude che la forma è invalida- che si ha indecidibilità?
Un'esempio di un albero infinito è quello che ci si può trovare costretti a costruire per verificare la validità di \(\forall x\exists y Rxy\vdash Raa\), infatti:
1 \(\quad\quad\forall x\exists y Rxy\)
2 \(\quad\quad\lnot Raa\)
3 \(\checkmark\quad\exists y Ray\) applico la regola* \(\forall\) per $a$ a 1
4\(\quad\quad Rab\) applico la regola** \(\exists\) a 3 introducendo $b$ e spunto la 3
5\(\checkmark\quad\exists y Rby\) applico la regola \(\forall\) per $b$ a 1
6\(\quad\quad Rbc\) applico la regola \(\exists\) a 5 introducendo $c$ e spunto la 5
7\(\checkmark\quad\exists y Rcy\) applico la regola \(\forall\) per $c$ a 1
8\(\quad \quad Rcd\) applico la regola \(\exists\) a 7 introducendo $d$ e spunto la 7
\(\vdots\)
$\infty$ grazie ancora!!!
*Per cui si sostituisce alla variabile quantificata universalmente una costante già presente.
**Per cui si sostituisce alla variabile quantificata esistenzialmente una costante non presente.
Per quanto riguarda per esempio per il metodo degli alberi di refutazione, in cui si nega la conclusione per dimostrare che non si dà il caso che le premesse siano vere ed essa falsa, so che una data forma argomentativa oggetto di verifica è valida se e solo se ogni cammino si chiude. In tutti e soli i casi in cui non è valida succede invece che si termina un cammino che rimane aperto o ci si trova da "continuare all'infinito". Qui si tratta di applicare un insieme di regole che resituiscono la validità o l'invalidità di una forma piuttosto che di generare forme.
È a causa della possibile situazione in cui ci si trova a dover continuare all'infinito -cosa di cui però un essere umano (non so una macchina di Turing, di cui ho solo un'idea intuitiva, ma che so che si cita per definire l'indecidibilità) si accorge e conclude che la forma è invalida- che si ha indecidibilità?
Un'esempio di un albero infinito è quello che ci si può trovare costretti a costruire per verificare la validità di \(\forall x\exists y Rxy\vdash Raa\), infatti:
1 \(\quad\quad\forall x\exists y Rxy\)
2 \(\quad\quad\lnot Raa\)
3 \(\checkmark\quad\exists y Ray\) applico la regola* \(\forall\) per $a$ a 1
4\(\quad\quad Rab\) applico la regola** \(\exists\) a 3 introducendo $b$ e spunto la 3
5\(\checkmark\quad\exists y Rby\) applico la regola \(\forall\) per $b$ a 1
6\(\quad\quad Rbc\) applico la regola \(\exists\) a 5 introducendo $c$ e spunto la 5
7\(\checkmark\quad\exists y Rcy\) applico la regola \(\forall\) per $c$ a 1
8\(\quad \quad Rcd\) applico la regola \(\exists\) a 7 introducendo $d$ e spunto la 7
\(\vdots\)
$\infty$ grazie ancora!!!
*Per cui si sostituisce alla variabile quantificata universalmente una costante già presente.
**Per cui si sostituisce alla variabile quantificata esistenzialmente una costante non presente.
Hai ragione. Ricordavo male, anche se non del tutto. Riporto da Odifreddi - Il diavolo in cattedra (ero troppo a digiuno per rispolverare testi più seri in breve tempo 
):
):[...] La logica predicativa è semidecidibile. Di una formula valida, infatti, possiamo sempre determinare la validità, perché l'albero semantico ha tutti i rami contraddittori ed è finito. Di una formula non valida, invece, non sempre possiamo determinare la non validità, perché qualche ramo non contraddittorio dell'albero semantico può essere infinito. In altre parole, è possibile determinare tutte le risposte positive, ma non tutte quelle negative.
Grazie di cuore! Mi rimane però un dubbio: ho letto in rete che la decidibilità non implica la completezza: dice la Wikipedia che la teoria dei campi algebricamente chiusi è decidibile, ma non completa...
Come può un sistema in grado di verificare in un numero finito di passi la validità di ogni formula (se questa è la decidibilità) non essre in grado di verificare la validità di ogni formula (se questa è la completezza)? Ovviamente c'è qualcosa che ho travisato...
Come può un sistema in grado di verificare in un numero finito di passi la validità di ogni formula (se questa è la decidibilità) non essre in grado di verificare la validità di ogni formula (se questa è la completezza)? Ovviamente c'è qualcosa che ho travisato...
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo