Transcript
DECIDIBILITA' DELLA LOGICA PROPOSIZIONALE E INDECIDIBILITA' DELLA LOGICA DEL PRIMO ORDINE
PER CAPIRE… Nelle lezioni passate abbiamo visto come il teorema di correttezza e completezza permetta di stabilire un ponte tra calcolo logico e semantica, e cioè tra la nozione di conseguenza logica e quella di dimostrabilità. Il teorema di completezza per una logica dimostra che: -
una proposizione φ è conseguenza logica di un insieme di proposizioni Γ sse φ è
dimostrabile (con gli strumenti messi a disposizione dal calcolo scelto) a partire da Γ: Γ ⊨ φ sse Γ ⊢ φ
-
una proposizione (un insieme di proposizioni) è [in]/soddisfacibile sse è [in]/coerente:
Ricordiamo inoltre alcuni teoremi che esplicitano i rapporti incrociati tra soddisfacibilità e conseguenza logica e quindi tra dimostrabilità e coerenza: -
una proposizione φ è conseguenza logica di un insieme di proposizioni Γ sse Γ ∪ {¬φ} è insoddisfacibile
Γ ⊨ φ sse Γ ∪ {¬φ} è insoddisfacibile
-
[SEMANTICA]
una proposizione φ è dimostrabile a partire da un insieme di proposizioni Γ sse {Γ,¬φ} è incoerente (conduce a una contraddizione) Γ ⊢ φ sse {Γ,¬φ} è incoerente
[CALCOLO]
Tenere presente queste relazioni è fondamentale per acquisire dimestichezza con le relazioni tra
tali concetti e il concetto di decidibilità (si riveda anche il rapporto tra verità e conseguenza logica).
Il problema della decidibilità per un predicato P consiste nel chiedersi se esista una procedura
finita, un algoritmo per decidere, dato un elemento arbitrario a del dominio, dell'appartenenza di a all'estensione di P, e cioè se a ∈ P o a ∉ P.
Si noti che, parlare di decidibilità facendo ricorso a concetti come quelli di procedura finita e di
algoritmo significa porre il problema in modo generale e da un punto di vista intuitivo. E' tuttavia possibile richiamare alcune formalizzazioni che sono state date al concetto di algoritmo, ad
esempio, quella di Turing. Assumendo la tesi di Church (secondo la quale ogni algoritmo è una
funzione Turing computabile = ricorsiva = flowchart computabile = ...1) si può dunque far ricadere
le questioni relative alla decidibilità dei predicati all'interno della teoria della ricorsività. Tale passaggio è consentito dal fatto che è possibile studiare i predicati nei termini della loro funzione
caratteristica e le funzioni nei termini dei loro grafi. La funzione caratteristica fc di un predicato p
è la funzione che mi dice quali elementi di un dominio appartengono all'estensione di un predicato ed è definita nel modo seguente:
fc(x) = 1 se x è elemento di P fc(x) = 0 altrimenti
Viceversa il grafo di una funzione (n-aria) è il predicato (n+1-ario) che vale tra gli argomenti della
funzione e i rispettivi valori. Ad esempio per la somma tra due argomenti è la relazione sussistente
tra
tutti
gli
addendi
possibili
{(0,0,0),(0,1,1)...(2,0,2),(2,1,3),(2,2,4)...}.
e
le
rispettive
somme
PREDICATI DECIDIBILI; SEMIDECIDIBILI E INDECIDIBILI Possiamo dunque gettare un ponte tra decidibilità dei predicati (lato intuitivo) e funzioni ricorsive (formalizzazione) andando a vedere che tipo di funzioni sono le funzioni caratteristiche di tali predicati.
Diciamo dunque che un predicato P è decidibile Sse
Sse
Sse
per ogni x del dominio esiste un algoritmo per decidere se x ∈ P o x ∉ P [se cioè ho una
procedura che in un numero finito di passi termina dicendomi se x appartiene a P, o in
caso contrario, che x non appartiene a P]. esiste una funzione ricorsiva tale che
P(x)=1 se x ∈ P e
P(x)=0 se x ∉ P.
(Ma questa funzione è esattamente la funzione caratteristica di P, perciò:)
la sua funzione caratteristica è una funzione ricorsiva2.
Viceversa il grafo di una funzione ricorsiva è un insieme decidibile.
Un predicato è dunque decidibile se posso decidere sia delle istanza positive di tale predicato sia di quelle negative.
E’ invece possibile che si sia in grado di decidere solo delle istanza positive e cioè che si abbia una
algoritmo per determinare che x appartiene a P qualora x ∈ P, mentre invece non sia garantito di
determinare in un numero finito di passi che x non appartiene a P qualora x ∉ P. In questo caso,
se si ha cioè una procedura di semidecisione per P, si dice che P è un predicato semidecidibile.
1
Ricordiamo che la tesi di Church è corroborata dal fatto che diverse formalizzazioni del concetto
intuitivo di algoritmo sono dimostrate essere equivalenti. In particolare quindi se si accetta la tesi di church le funzioni ricorsive coprono la classe delle funzioni computabili. 2
Per correttezza occorre osservare che tale affermazione presuppone la decidibilità dell’identità, e
la numerabilità del dominio. Non approfondiremo oltre la questione dal momento che qui si
vogliono dare solo brevi cenni della teoria della ricorsività. Peraltro per applicazioni standard delle teoria della ricorsività questa assunzione non pone grandi problemi.
Attenzione: la classe dei predicati semidecidibile è soprainsieme di quella dei predicati decidibili,
poiché ogni predicato decidibile è anche semidecidibile. In particolare un predicato è decidibile se
è semidecidibile sia lui sia il suo complemento (il complemento di un insieme P è l’insieme degli elementi che non appartengono a P).
Volendo ricollegarsi alla teoria della ricorsività come si è fatto per la decidibilità, riporteremo le seguenti equivalenze:
un predicato P è semidecidibile sse
Sse
è il dominio di una funzione parziale ricorsiva (tale cioè che ho una procedura per calcolare
il valore per ogni elemento per cui la funzione è definita).
è il codominio di una funzione ricorsiva e cioè se è un insieme ricorsivamente enumerabile (R.E.).
Ovviamente una simile trattazioni di queste nozioni non è sufficiente a dare un quadro ne esauriente ne sufficientemente chiaro dei rapporti tra decidibilità e teoria della ricorsività. Si intende però così dare almeno una spiegazione del perchè nella letteratura nel campo dell’IA,
spessi vengano usati come sinonimi “insieme ricorsivamente enumerabile (r.e.)” e “insieme semidecidibile”. Un predicato è indecidibile se non è decidibile.
DECIDIBILITA’ E LOGICA PROPOSIZIONALE E DEL PRIMO ORDINE Posto il problema generale della decidibilità di un predicato veniamo a capire che senso abbia parlare di decidibilità per una logica. Il passaggio viene fatto prendendo in considerazione la
decidibilità di insiemi come cons(Γ) e teor(Γ) [gli insiemi rispettivamente delle conseguenze logiche
e dei teoremi di Γ], e di sat(L) e coer(L) soddisfacibili e coerenti del linguaggio].
[gli insiemi rispettivamente degli insiemi di formule
Il problema della decidibilità per una logica può essere dunque introdotto come segue: Esiste un algoritmo che mi permetta di decidere, per ogni proposizione φ del linguaggio se φ è valida, se cioè ⊨φ o ⊭φ?
E poiché la nozione di conseguenza logica è indissolubilmente legata a quella di verità, il problema può essere generalizzato3 nel modo seguente:
dato un insieme di proposizioni Γ, esiste per ogni φ un algoritmo per sapere se Γ ⊨ φ o Γ ⊭ φ? Ovvero, dato un insieme anche vuoto di assiomi Γ, cons(Γ) è un insieme decidibile?
La risposta è che mentre la logica preposizionale è decidibile, quella del primo ordine non lo è ma
è soltanto semidecidibile. Questo significa data una proposizione della logica preposizionale A esiste un algoritmo che termina sempre dicendomi se A è vera o meno. Data una proposizione φ
al primo ordine invece, esiste una procedura meccanica π tale che, se φ è vera, π termina in un numero finito di passi attestando la verità di φ, ma se φ invece non è vera non è garantito che π
3
Questa è una generalizzazione perché nel caso in cui Γ sia vuoto si ha il caso precedente.
termini attestandolo. Per la logica del primo ordine dunque, soltanto cons(Γ) è semidecidibile, mentre il suo complemento (l’insieme delle proposizioni che non sono conseguenza logica di Γ)
non lo è. Per questo si usa dire che la logica del primo ordine è indecidibile.
Utilizzando i teoremi riportati all’inizio del capitolo si ottengono i risultati di decidibilità per la soddisfacibilità e la coerenza. In particolare, poiché Γ ⊨ φ sse Γ ∪ {¬φ} è insoddisfacibile
[e quindi
Γ ⊭ φ sse Γ ∪ {¬φ} è soddisfacibile]
se ho un test per la verità di φ (un test per sapere se φ è conseguenza logica di Γ), allora ho un test anche per l’insoddisfacibilità. Viceversa se ho un test per la non verità di φ, ho anche un test per la soddisfacibilità. In particolare, sat(L) e, via completezza, coer(L) sono insiemi decidibili o solo semidecidibili?
Per quanto riguarda la logica preposizionale, essendo essa decidibile e disponendo di un test sia
per la verità che per la non verità delle proposizioni, avremo un test anche per la soddisfacibilità e l’insoddisfacibilità; essendo dunque semidecidibili sia sat(L) e coer(L) sia i loro complementi, sat(L) e coer(L) sono entrambi insiemi decibili.
Per quanto riguarda la logica del primo ordine, invece, le cose stanno diversamente. Qui abbiamo
un test per la verità, ma non un test per la non verità, grazie ai teoremi incrociati di cui sopra, si
ottiene dunque che per la logica predicativa avremo un test per l’insoddisfacibilità mentre non
avremo alcun test per la soddisfacibilità. Dunque, sat(L) è indecidibile mentre il suo complemento è semidecidibile (il medesimo ragionamento è applicabile a coer(L)). Poniamo dunque di voler
chiederci se una formula φ o un insieme di formule Γ è soddisfacibile: se φ (Γ) è insoddisfacibile
esisterà una procedura che terminerà in un numero finito di passi rispondendo negativamente, se φ (Γ) invece è soddisfacibile nulla mi garantisce una risposta positiva entro un numero finito di passi.
Ricapitoliamo i risultati di decidibilità per la logica del primo ordine:
cons(Γ) e –sat(L)4 sono semidecidibili, o, come spesso si trova scritto, sono ricorsivamente
enumerabili (esiste un algoritmo che è in grado di generare tutte le conseguenze logiche di un insieme di proposizioni Γ, e tale algoritmo è precisamente un calcolo corretto e completo!);
-cons(Γ) e sat(L) sono indecidibili, o, come spesso si trova scritto, non sono nemmeno ricorsivamente enumerabili.
Attenzione, questi risultati valgono per teorie arbitrarie del primo ordine. Non significa dunque che ogni teoria del primo ordine sia indecidibile, ma data una specifica teoria del primo ordine, in
generale non se ne può affermare la decidibilità, sebbene si possa cercare di dimostrarla. In realtà, data la fondamentale relazione tra decidibilità e computabilità (attraverso la teoria della ricorsività)
e data l’importanza che la computabilità riveste nell’ambito delle applicazioni della logica in
informatica, molti sforzi sono stati rivolti a dimostrare la decidibilità, non di specifiche teorie, ma
di classi di teorie, ovvero di frammenti della logica del primo ordine. Per esempio limitandosi a
domini finiti5 o riducendo il numero di variabili contenute nelle formule del linguaggio è possibile
dirigersi verso frammenti decidibili della logica del primo ordine. Ad esempio, l’ampio successo che le Description Logics stanno riscuotendo in diversi ambiti dell’informatica è dovuto anche al fatto che esse sfruttano frammenti del primo ordine decidibili. 4 5
Con –cons(Γ) indichiamo il complemento di cons(Γ).
In modo analogo ai vantaggi computazionali che si ottengono nello studio delle funzioni ricorsive
considerando funzioni che contengano unicamente µ operatori limitati.
