IA simbolica: logica epistemica

Una logica per ragionare su conoscenza e opinione

Questa parte si basa su un paio di testi:

  1. Hans van Ditmarsch, Joseph Y. Halpern, Wiebe van der Hoek, Barteld Kooi. An Introduction to Logics of Knowledge and Belief. Capitolo 1 di Handbook of Epistemic Logic, 2015.

  2. Rasmus Rendsvig, John Symons, and Yanjing Wang. Epistemic Logic, The Stanford Encyclopedia of Philosophy, Edward N. Zalta & Uri Nodelman (eds.), 2023.

La logica epistemica studia la nozione di conoscenza (knowledge in inglese; episteme in greco) e la logica doxastica studia la nozione di credenza (belief in Inglese; in greco antico doxa significa opinione). In senso più ampio, queste logiche studiano la nozione di informazione.

Il ragionamento sulla conoscenza presenta sottigliezze che vanno oltre quelle che si presentano nella logica proposizionale o dei predicati. Prendiamo, ad esempio, la legge del terzo escluso nella logica classica, che dice che per qualsiasi proposizione pp, deve valere o pp o ¬p\neg p (la negazione di pp); formalmente, p¬pp \vee \neg p.

Nel linguaggio della logica epistemica, scriviamo KapK_a p per dire che "l'agente aa conosce pp" e intuitivamente intendiamo che "in tutti i possibili mondi accessibili dall'agente aa la proposizione pp è vera".

Qui un mondo è intuitivamente uno stato di conoscenza. Ad esempio se Alice si sta chiedendo se Bob arriverà puntuale o in ritardo, i possibili mondi sono due: quello in cui Bob arriva in orario e quello in cui Bob arriva in ritardo.

Questa semplice aggiunta al linguaggio ci permette di porre nuove questioni. Ad esempio, che tipo di situazioni descrivono le seguenti formule? Quali di loro dovrebbero essere valide?

  1. Kap¬KapK_a p \vee \neg K_a p: l'agente aa conosce pp o l'agente aa non conosce pp

  2. KapKa¬pK_a p \vee K_a \neg p: l'agente aa conosce pp o l'agente aa conosce la sua negazione ¬p\neg p

  3. Ka(p¬p)K_a (p \vee \neg p): l'agente aa conosce pp o la sua negazione ¬p\neg p

  4. Kap¬Ka¬pK_a p \vee \neg K_a \neg p: l'agente aa conosce pp o l'agente aa non conosce la sua negazione ¬p\neg p

Abbiamo che, data la semantica che ci interessa, solo la prima e la terza formula sono valide, in quanto sono riformulazioni epistemiche di tautologie proposizionali. La seconda non è valida in quanto l'agente aa potrebbe non conoscere pp e neppure la sua negata, ovvero avere incertezza su pp. Anche la quarta formula non è valida in quanto afferma che l'agente aa conosce pp oppure considera pp possibile, ma potrebbe darsi che l'agente aa conosca la negazione di pp (ovvero ¬p\neg p sia vera in tutti i mondi accessibili dall'agente aa), rendendo falsa la formula.

Una delle caratteristiche interessanti della logica epistemica è che va oltre la conoscenza fattuale che gli agenti hanno. La conoscenza può riguardare la conoscenza stessa, quindi possiamo scrivere espressioni come Ka(KapKaq)K_a(K_a p \rightarrow K_a q): l'agente aa sa che se conosce pp allora consce anche qq (i verbi sapere e conoscere sono usati come sinonimi in questo testo). Le affermazioni sulla conoscenza fattuale vengono anche chiamate di prim'ordine, quelle sulla conoscenza della conoscenza vengono dette di ordine superiore.

Ancora più interessante è la possibilità di modellare la conoscenza degli altri, un aspetto importante quando si ragiona sui protocolli di comunicazione. Supponiamo che Anna conosca un fatto mm: "Sono incinta". Quindi abbiamo KamK_a m.

Supponiamo che Anna invii questo messaggio via e-mail a Baldo (il padre del bambino) e che Baldo lo legga. Abbiamo quindi KamKbmKbKamK_a m \wedge K_b m \wedge K_b K_a m.

Naturalmente sia Anna che Baldo sanno di sapere, ovvero KaKamKbKbmK_a K_a m \wedge K_b K_b m. Abbiamo anche KaKbmK_a K_b m? A meno che Anna non abbia informazioni sul fatto che Baldo abbia effettivamente letto il messaggio, non può presumere che l'abbia fatto, quindi abbiamo ¬KaKbm¬Ka¬Kbm\neg K_a K_b m \wedge \neg K_a \neg K_b m.

Essendo un gentiluomo, Baldo potrebbe rispondere ad Anna dicendo di aver letto il messaggio. A questo punto vale KaKbmK_a K_b m. Abbiamo anche KaKbKamK_a K_b K_a m (Anna sa che Baldo sa che lei sa, perché Baldo ha risposto a Anna) ma, poiché Baldo non può presumere che Anna abbia letto la conferma, non abbiamo ancora KbKaKbmK_b K_a K_b m.

A questo punto Anna e Baldo potrebbero prendere il telefono e parlarsi! L'uso del telefono è un buon protocollo che garantisce la conoscenza comune tra Anna e Baldo, ovvero:

KamKbm Ka(KamKbm)Kb(KbmKam) Ka(Ka(KamKbm)Kb(KbmKam))Kb(Ka(KamKbm) Kb(KbmKam))\begin{array}{l} K_a m \wedge K_b m \ \wedge \\ K_a (K_a m \wedge K_b m) \wedge K_b (K_b m \wedge K_a m) \ \wedge \\ K_a (K_a (K_a m \wedge K_b m) \wedge K_b (K_b m \wedge K_a m)) \wedge \\ K_b (K_a (K_a m \wedge K_b m) \ \wedge K_b (K_b m \wedge K_a m)) \wedge \ldots \end{array}

Si noti che la formula della conoscenza comune è infinita e la sua lunghezza cresce in modo esponenziale al crescere dell'ordine della conoscenza. Sviluppando la formula abbiamo 2 congiunzioni al prim'ordine, 4 al second'ordine, 8 al terz'ordine, e in generale 2n2^n all'ordine nn.

Sintassi

La logica modale epistemica estende la logica proposizionale. Il linguaggio della logica proposizionale presuppone un insieme AtAt di proposizioni primitive (o atomiche), tipicamente indicate con p,q,p, q, \ldots. Esse si riferiscono tipicamente ad affermazioni considerate elementari, cioè prive di struttura logica, come "piove" o "Anna è incinta".

La logica proposizionale utilizza gli operatori booleani, come ¬\neg ("non"), \wedge ("e"), \vee, ("o"), \rightarrow ("implica") e \leftrightarrow ("se e solo se"), per costruire formule più complesse. Gli unici operatori necessari sono ¬\nege \wedge , infatti:

  • αβ\alpha \vee \beta è uguale a ¬(¬α¬β)\neg(\neg \alpha \wedge \neg \beta)

  • αβ\alpha \rightarrow \beta è uguale a ¬αβ\neg \alpha \vee \beta

  • αβ\alpha \leftrightarrow \beta equivale a (αβ)(βα)(\alpha \rightarrow \beta) \wedge (\beta \rightarrow \alpha)

Inoltre, definiamo il simbolo vero \top come p¬pp \vee \neg p e il simbolo falso \bot come ¬\neg \top, ovvero p¬pp \wedge \neg p.

Quando ragioniamo sulla conoscenza, dobbiamo poter fare riferimento al soggetto, cioè all'agente di cui stiamo parlando. Un agente è un'entità umana o artificiale. Per fare ciò, assumiamo un insieme finito Ag di agenti. Per ragionare sulla conoscenza, aggiungiamo al linguaggio della logica proposizionale gli operatori KaK_a, dove KaφK_a \varphi denota "l'agente aa conosce φ\varphi". Sia Op={Ka  aAg}Op = \{K_a \ |\ a \in Ag\} l'insieme degli operatori di conoscenza per ogni agente. Il duale dell'operatore di conoscenza è MaφM_a \varphi e denota "l'agente aa considera possibile φ\varphi"; è definito come:

Maφ=¬Ka¬φM_a \varphi = \neg K_a \neg \varphi

Siamo pronti a definire il linguaggio della logica modale epistemica L(At,Ag,Op)L(At, Ag, Op) con la seguente grammatica BNF (Backus-Naur Form):

φ:=p  ¬φ  (φφ)  Kaφ\varphi := p \ | \ \neg \varphi \ | \ (\varphi \wedge \varphi) \ | \ K_a \varphi

dove pAtp \in At e aAga \in Ag.

Si noti che una formula è illimitata ma finita. Inoltre, il linguaggio della logica proposizionale è L(At,,)=L(At)L(At, \emptyset, \emptyset) = L(At) e il linguaggio della logica (uni-)modale è L(At,{a},{ka})L(At, \{a\}, \{k_a\}); nel caso della logica uni-modale KaK_a è indicato come \Box e MaM_a è indicato come \Diamond. Quando c'è più di un agente si parla di logica multimodale.

Semantica

Definiamo ora un modo per determinare sistematicamente il valore di verità di una formula, cioè di dare una semantica al linguaggio modale epistemico. Nella logica proposizionale, il fatto che una proposizione pp sia vera o meno dipende dalla situazione in cui ci troviamo. Le situazioni rilevanti sono formalizzate utilizzando le valutazioni, dove una valutazione è una funzione V : At{vero,falso}V \ : \ At \rightarrow \{vero, falso\} che determina il valore di verità delle proposizioni primitive.

Una valutazione può essere estesa in modo da determinare la verità di tutte le formule, utilizzando una semplice definizione induttiva:

  • φψ\varphi \wedge \psi è vera in VV sse sia φ\varphi che ψ\psi sono vere in VV;

  • ¬φ\neg \varphi è vera in VV sse φ\varphi è falsa in VV.

Per modellare la conoscenza utilizziamo idee che risalgono al filosofo finlandese Jaakko Hintikka.

Pensiamo a un agente che considera possibili un certo numero di situazioni diverse, chiamate mondi o stati, che sono coerenti con le informazioni di cui l'agente dispone.

Per esempio, se l'agente sa che oggi è un giorno di fine settimana, allora in un mondo possibile oggi è sabato e in un altro mondo possibile oggi è domenica, ma non esiste un mondo in cui oggi è lunedì.

Quindi ogni agente ha la sua relazione di accessibilità che dice quali mondi sono accessibili (considerati possibili) a partire da un dato mondo.

Diremo che un agente conosce una formula in un mondo se la formula è vera in tutti i mondi che l'agente considera possibili a partire da quel mondo.

Quindi, piuttosto che usare una singola situazione per dare significato alle formule modali, come nella logica proposizionale, usiamo un insieme di tali situazioni; inoltre, in ogni situazione, consideriamo, per ogni agente, quali altre situazioni l'agente considera possibili.

La struttura risultante è un grafo etichettato, chiamato modello di Kripke, dove i nodi sono i mondi e gli archi sono i collegamenti di accessibilità per gli agenti:

  • ogni mondo è etichettato con le proposizioni atomiche vere in quel mondo;

  • ogni arco è etichettato con un insieme non vuoto di agenti che usano quel collegamento nella propria relazione di accessibilità.

Segue un esempio con 4 mondi {v,w,s,u}\{v, w, s, u\} e due agenti (aa e bb).

Un modello di Kripke con 4 mondi e 2 agenti.

Formalmente, dato un insieme AtAt di proposizioni primitive e un insieme AgAg di agenti, un modello di Kripke è una struttura M=(S,R,V)M = (S, R, V), dove:

  • SS \neq \emptyset è un insieme di stati (o mondi);

  • R : AgP(S×S)R \ : \ Ag \rightarrow {\cal P}(S \times S) è una funzione che per ogni agente aAga \in Ag restituisce una relazione di accessibilità RaS×SR_a \subseteq S \times S (un insieme di coppie di stati);

  • V : S(At{vero,falso})V \ : \ S \rightarrow (At \rightarrow \{vero, falso\}) è una funzione che per ogni stato sSs \in S restituisce una valutazione delle proposizioni nello stato ss.

La classe di tutti i modelli di Kripke è indicata con K\cal K. Una struttura di Kripke F=(S,R)F = (S, R) si concentra solo sul grafo sottostante un modello, senza considerare la valutazione.

Siamo pronti a definire la verità di una formula in un modello di Kripke e uno stato del modello. Dato un modello M=(S,R,V)M = (S, R, V) e un mondo sSs \in S, definiamo cosa significa che una formula φ\varphi è vera in (M,s)(M, s), scritto M,sφM, s \vDash \varphi, induttivamente come segue:

  • M,spM, s \vDash p sse V(s)(p)=veroV(s)(p) = vero per pAtp \in At

  • M,sφψM, s \vDash \varphi \wedge \psi sse M,sφM, s \vDash \varphi e M,sψM, s \vDash \psi

  • M,s¬φM, s \vDash \neg \varphi sse non vale M,sφM, s \vDash \varphi (scritto anche come M,s⊭φM, s \not\vDash \varphi)

  • M,sKaφM, s \vDash K_a \varphi sse M,tφM, t \vDash \varphi per ogni tt tale che (s,t)Ra(s,t) \in R_a (scritto anche come RastR_a st)

Si ricordi che Maφ:=¬Ka¬φM_a \varphi := \neg K_a \neg \varphi; segue facilmente che:

  • M,sMaφM, s \vDash M_a \varphi sse M,tφM, t \vDash \varphi per qualche tt tale che (s,t)Ra(s,t) \in R_a

Quindi l'operatore modale KK corrisponde ad una quantificazione universale del tipo x.φ(x)\forall x. \varphi(x) e il suo duale MM corrisponde ad una quantificazione esistenziale del tipo x.φ(x)\exists x. \varphi(x).

Infine scriveremo MφM \vDash \varphi se M,sφM, s \vDash \varphi per ogni mondo sSs \in S.

Vediamo un esempio. Anna e Baldo si sono dati appuntamento per la prima volta per un aperitivo, ma, essendo la prima uscita, nessuno sa il numero di telefono dell'altro. Ognuno sa quanto tempo serve per arrivare da casa al luogo dell'incontro, quindi, assumendo che entrambi abbiano un orologio, ognuno è consapevole se sarà puntuale o in ritardo all'appuntamento, ma non potendo comunicare con l'altro, non ha questa informazione per l'altro. Possiamo modellare questa situazione con il modello di Kripke rappresentato in figura, dove le etichette aa e bb sugli archi indicano rispettivamente la relazione di accessibilità di Anna e Baldo e le proposizioni tat_a e tbt_b indicano rispettivamente che Anna e Baldo sono puntuali (quindi ¬ta\neg t_a indica che Anna è in ritardo e similmente per Baldo).

La rappresentazione epistemica dell'appuntamento tra Anna e Baldo.

Si noti che, per esempio, se Anna sa di essere puntuale (mondi ww e vv), i mondi possibili per Anna sono quelli in cui Baldo è puntuale (ww) o in ritardo (vv). Similmente per Baldo. Inoltre, se Anna sa di essere in ritardo (mondi ss e uu), i mondi possibili per Anna sono quelli in cui Baldo è puntuale (ss) o in ritardo (uu). Similmente per Baldo. Ognuno dei quattro mondi rappresenta una delle possibili situazioni di puntualità e ritardo per Anna e Baldo. Si noti che i mondi ww e uu, ad esempio, non sono mutuamente accessibili né per Anna né per Baldo. Infatti, se Anna sa si essere puntuale nel mondo ww, è inconcepibile per lei il mondo uu in cui è in ritardo; d'altronde se Anna sa di essere in ritardo nel mondo uu non potrà essere puntuale nel mondo ww; lo stesso per Baldo.

Valgono le seguenti:

  1. M,wtatbM, w \vDash t_a \wedge t_b: nel mondo ww sia Anna che Baldo sono puntuali

  2. M,wKataKbtbM, w \vDash K_a t_a \wedge K_b t_b: nel mondo ww sia Anna che Baldo sanno che saranno puntuali

  3. M,w¬Kbta¬KatbM, w \vDash \neg K_b t_a \wedge \neg K_a t_b: nel mondo ww sia Anna che Baldo non sanno se l'altro sarà puntuale. Equivalentemente possiamo scrivere M,wMb¬taMa¬tbM, w \vDash M_b \neg t_a \wedge M_a \neg t_b, ovvero nel mondo ww sia Anna che Baldo ritengono possibile che l'altro sia in ritardo

  4. M(KataKa¬ta)(KbtbKb¬tb)M \vDash (K_a t_a \vee K_a \neg t_a) \wedge (K_b t_b \vee K_b \neg t_b): in ogni mondo Anna sa se sarà puntuale o in ritardo (in quanto ha un orologio) e lo stesso vale per Baldo

  5. MKata¬KataM \vDash K_a t_a \vee \neg K_a t_a: in tutti i mondi Anna sa di essere puntuale oppure non sa di esserlo. Si noti che questa è una tautologia, quindi è vera indipendentemente dal modello

Ricordiamo che K\cal{K} è la classe di tutti i modelli. Sia XK\cal{X} \subseteq \cal{K} una classe di modelli e φ\varphi una formula. Diremo che:

  • φ\varphi è valida in X\cal X, e scriveremo Xφ\cal{X} \vDash \varphi, se MφM \vDash \varphi per ogni modello MXM \in \cal{X};

  • φ\varphi è soddisfacibile in X\cal X se M,sφM, s \vDash \varphi per qualche modello MXM \in \cal{X} e stato ss del modello.

Ad esempio, come abbiamo osservato sopra, KataMa¬taK_a t_a \vee M_a \neg t_a è una formula valida. Inoltre KbtbKb¬tbK_b t_b \vee K_b \neg t_b è soddisfacibile (basta prendere il modello di sopra e un qualunque stato del modello), ma non è valida in K\cal K, la classe di tutti i modelli. E' facile costruire un modello MM in cui esiste un mondo ww tale che tbt_b è vera in alcuni mondi raggiungibili da ww e falsa in altri, dunque non è vero che tbt_b è sempre vera o sempre falsa in tali mondi, dunque K⊭φ\cal{K} \not\vDash \varphi. D'altronde se scegliamo XK\cal{X} \subseteq \cal{K} come la classe dei modelli lineari, ovvero in cui ogni mondo ha esattamente un successore, allora Xφ\cal{X} \vDash \varphi, cioè φ\varphi è valida in X\cal X.

Definiamo infine una serie di classi di modelli in termini di proprietà delle relazioni di accessibilità in tali modelli. Poiché dipendono solo dalla relazione di accessibilità, avremmo potuto definirle anche per le strutture sottostanti; infatti, le proprietà sono talvolta chiamate proprietà delle strutture.

Sia RR una relazione di accessibilità su un dominio di stati SS:

  1. Se RR non ha alcuna proprietà particolare, indicheremo la relativa classe dei modelli di Kripke con K\cal K.

  2. RR è riflessiva se per tutti gli xx si ha RxxRxx. La classe dei modelli di Kripke riflessivi è indicata con KT\cal KT.

  3. RR è simmetrica se per tutti gli x,yx, y, se RxyRxy allora RyxRyx. La classe dei modelli di Kripke simmetrici è indicata con KB\cal KB.

  4. RR è transitiva se per tutti x,y,zx, y, z, se RxyRxy e RyzRyz allora RxzRxz. La classe dei modelli di Kripke transitivi è indicata con K4\cal K4.

  5. RR è seriale se per tutti gli xx esiste un yy tale che RxyRxy. La classe dei modelli di Kripke seriali è indicata con KD\cal KD.

  6. RR è Euclidea se per tutti gli x,y,zx, y, z, se RxyRxy e RxzRxz allora RyzRyz. La classe dei modelli di Kripke euclidei è indicata con K5\cal K5.

  7. RR è una relazione di equivalenza se RR è riflessiva, simmetrica e transitiva. La classe dei modelli di Kripke in cui le relazioni sono relazioni di equivalenza è denotata con KTB4\cal KTB4 e più spesso con S5\cal S5.

Vale che una relazione di equivalenza partiziona l'insieme dei mondi in insiemi non vuoti, disgiunti e la cui unione restituisce l'intero insieme dei mondi.

  1. Mostrare che una relazione riflessiva e Euclidea è una relazione di equivalenza e viceversa. In altri termini, mostrare che S5=KT5\cal{S5} = \cal{KT5}.

  2. Mostrare che una relazione riflessiva è anche seriale.

Proprietà logiche della conoscenza e della credenza

La classe S5\cal S5 dei modelli associati a relazioni di equivalenza è stata tipicamente usata per modellare la conoscenza. In tal caso la relazione di accessibilità è anche detta relazione di indistinguibilità, in quanto due mondi associati dalla relazione sono indistinguibili in base all'informazione che l'agente ha a disposizione. Ad esempio, se ho la sola informazione che è un giorno del fine settimana, il mondo del Sabato e della Domenica sono indistinguibili.

Vediamo quali sono le formula valide che contraddistinguono la classe dei modelli S5\cal S5 e i sui sovrainsiemi fino alla classe K\cal K di tutti i modelli.

Regola della sostituzione delle istanze delle tautologie proposizionali

Se φ\varphi è una istanza modale di una tautologia proposizionale, allora Kφ{\cal K} \vDash \varphi.

Ad esempio, dato che p¬pp \vee \neg p e p(qp)p \rightarrow (q \rightarrow p) sono tautologie proposizionali, allora anche le seguenti formule sono sempre valide: Kp¬KpKp \vee \neg Kp e K(pq)(KrK(pq))K(p \vee q) \rightarrow (Kr \rightarrow K(p \vee q)).

Regola del modus ponens

Se Kφ{\cal K} \vDash \varphi e Kφψ{\cal K} \vDash \varphi \rightarrow \psi allora Kψ{\cal K} \vDash \psi.

Una delle regole classiche del ragionamento, la storia del modus ponens risale all'antichità: il primo a descriverla esplicitamente fu Teofrasto (371 circa – 287 circa a.C.).

Regola della generalizzazione della conoscenza

Se Kφ{\cal K} \vDash \varphi allora KKφ{\cal K} \vDash K \varphi

Ovvero, gli agenti conoscono tutte le formule valide. Questa regola è anche chiamata regola della necessità (necessitation rule). E' valida per la classe K{\cal K} di tutti i modelli.

Assioma di distribuzione della conoscenza

K(KφK(φψ))Kψ{\cal K} \vDash (K \varphi \wedge K (\varphi \rightarrow \psi)) \rightarrow K \psi

Questo assioma, tradizionalmente conosciuto come K, stabilisce il modus ponens come regola di inferenza a livello epistemico. E' valido per la classe K{\cal K} di tutti i modelli.

Assioma della consistenza

KDKφMφ{\cal KD} \vDash K \varphi \rightarrow M \varphi

Ovvero, se conosco qualcosa, lo ritengo anche possibile. L'assioma di consistenza, noto come D, è valido per la classe dei modelli seriali KD{\cal KD}.

L'assioma D è equivalente a Kφ¬K¬φK \varphi \rightarrow \neg K \neg \varphi: se conosco qualcosa, non posso conoscere anche il suo contrario. Ovvero sono consistente. Esso è anche equivalente a ¬K\neg K \bot, cioè non conosco il falso, o equivalentemente MM \top, cioè credo nel vero.

Mostrare che:

  1. se un modello è seriale, allora D è vero in tutti i suoi mondi

  2. se un modello non è seriale, allora D non è vero in almeno un mondo (più precisamente, dato un frame F=(S,R)F = (S,R) non seriale esiste una valutazione VVtale che D non è vero in almeno un mondo del modello M=(S,R,V)M = (S, R, V))

Assioma della verità

KTKφφ{\cal KT} \vDash K \varphi \rightarrow \varphi

Questo assioma, noto anche come T, dice che se un agente conosce dei fatti, questi devono essere veri (nel mondo corrente). L'assioma T è valido per la classe dei modelli riflessivi KT{\cal KT}.

Questo assioma può essere espresso anche nella sua contrapposizione: φ¬K¬φ\varphi \rightarrow \neg K \neg \varphi, ovvero se qualcosa è vero nel mondo corrente non posso conoscere il suo contrario.

L'assioma di verità è spesso considerato la principale caratteristica che distingue la conoscenza (knowledge) dalla credenza (belief). Come vedremo, nella logica doxastica l'assioma di verità T è sostituito dall'assioma di coerenza D.

Mostrare che:

  1. se un modello è riflessivo, allora T è vero in tutti i suoi mondi

  2. se un modello non è riflessivo, allora T non è vero in almeno un mondo

L'assioma di introspezione positiva

K4KφKKφ{\cal K4} \vDash K \varphi \rightarrow KK\varphi

L'assioma dell'introspezione positiva, noto come 4, afferma che se un agente conosce qualcosa, allora sa di saperlo.

Equivalentemente, questo assioma dice che se non so di sapere allora non so: ¬KKφ¬Kφ\neg K K \varphi \rightarrow \neg K\varphi

Questo assioma è valido per la classe dei modelli transitivi K4{\cal K4}.

Mostrare che:

  1. se un modello è transitivo, allora 4 è vero in tutti i suoi mondi

  2. se un modello non è transitivo, allora 4 non è vero in almeno un mondo

L'assioma di introspezione negativa

K5¬KφK¬Kφ{\cal K5} \vDash \neg K \varphi \rightarrow K \neg K\varphi

L'assioma dell'introspezione negativa, noto anche come assioma 5, dice che se un agente non conosce qualcosa, allora sa di non saperlo.

Equivalentemente, questo assioma dice che se non so di non sapere allora so: ¬K¬KφKφ\neg K \neg K \varphi \rightarrow K\varphi

Questo assioma è valido per la classe dei modelli euclidei K5{\cal K5}.

Mostrare che:

  1. se un modello è euclideo, allora 5 è vero in tutti i suoi mondi

  2. se un modello non è euclideo, allora 5 non è vero in almeno un mondo

Ragionare in logica epistemica con i chatbot

Ho provato a chiedere ai modelli di ragionamento di ChatGPT (o3-mini-high), Google (Gemini 2.0 Flash Thinking), Claude (3.5 Haiku), Grok 3 e DeepSeek (R1) i seguenti ragionamenti:

  1. In logica modale epistemica, l'assioma di introspezione negativa, noto anche come assioma 5, dice che se un agente non conosce qualcosa, allora sa di non saperlo: ¬KφK¬Kφ\neg K \varphi \rightarrow K \neg K\varphi. Dimostrami che questo assioma è valido su tutti i modelli euclidei, dove una modello è euclideo se la sua relazione di raggiungibilità R ha la seguente proprietà: per ogni x, y e z, se Rxy e Rxz allora Ryz.

  2. Prendiamo un modello con tre mondi, xx, yy e zz e relazione di accessibilità RR tale che: RxyRxy, RxzRxz, RyzRyz e RzyRzy. Supponiamo che in yy valga la proposizione pp e in zz non valga la proposizione pp. Allora ho che ¬Kp\neg K p vale nel mondo xx. Ma K¬KpK \neg K p non vale in xx. Infatti, prendiamo il mondo zz raggiungibile da xx. In tale mondo zz vale KpK p (in quanto yy è l'unico mondo raggiungibile da zz e in yy vale pp). Dunque non è vero che in tutti i mondi raggiungibili da xx non vale KpKp. Quindi K¬KpK \neg K p non vale in xx. Dove sbaglio?

Le risposte sono state le seguenti:

  1. ChatGPT e Gemini hanno prodotto una ragionevole dimostrazione del primo punto e trovato l'errore del ragionamento del secondo. Gemini ha pensato più a lungo.

  2. Claude ha prodotto una elegante dimostrazione per assurdo del primo punto ma non ha risolto il secondo punto, sconfessando di fatto la dimostrazione data e affermando che l'assioma di introspezione negativa non caratterizza i modelli Euclidei (sbagliando dunque).

  3. Grok ha trovato una dimostrazione per il primo punto (pensando molto a lungo) ma non ha saputo controbattere il controesempio del secondo punto. A questo punto, in modo impreciso, ha sostenuto che in logica epistemica i modelli sono euclidei e riflessivi (ovvero relazioni di equivalenza), e in tal caso l'assioma è valido. Non è falso, ma impreciso, dato che il mio modello non presuppone la riflessività.

  4. DeepSeek ha pensato molto a lungo (11 minuti) e ha fornito una prova elegante del primo punto. Al secondo punto ha risposto: The server is busy. Please try again later.

L'assioma della simmetria

KBφKMφ{\cal KB} \vDash \varphi \rightarrow K M \varphi

L'assioma di simmetria, noto anche come assioma B, dice che se qualcosa è vero, allora un agente sa di ritenerlo possibile.

Equivalentemente, questo assioma dice che se un agente ritene possibile di conoscere qualcosa, allora quel qualcosa è vero: MKφφM K \varphi \rightarrow \varphi

Questo assioma è valido per la classe dei modelli simmetrici KB{\cal KB}.

Mostrare che:

  1. se un modello è simmetrico, allora B è vero in tutti i suoi mondi

  2. se un modello non è simmetrico, allora B non è vero in almeno un mondo

Si noti che se X\cal{X} e Y\cal{Y} sono insiemi di modelli e XY\cal{X} \subseteq \cal{Y}, allora Yφ{\cal Y} \vDash \varphi implica Xφ{\cal X} \vDash \varphi. Dato che una relazione di equivalenza è per definizione riflessiva, simmetrica e transitiva, e inoltre è Euclidea e seriale, allora la classe di modelli S5{\cal S5}, eredita tutti gli assiomi elencati in questa sezione, che quindi potremmo definire gli assiomi della conoscenza.

Conoscenza e credenza

S5=KT45{\cal S5} = \cal{KT45} è spesso definita la logica della conoscenza, caratterizzata da:

  1. l'assioma della verità T (che cattura la riflessività dei modelli)

  2. l'assioma dell'introspezione positiva 4 (che cattura la transitività dei modelli)

  3. l'assioma dell'introspezione negativa 5 (che cattura l'essere Euclideo dei modelli)

Come abbiamo detto, 4 è ridondante in S5\cal S5 dato che una relazione riflessiva e Euclidea è anche transitiva.

La logica della credenza, detta anche logica doxastica, è invece spesso rappresentata da KD45\cal KD45 ed è quindi caratterizzata da:

  1. l'assioma della coerenza D (che cattura la serialità dei modelli)

  2. l'assioma dell'introspezione positiva 4 (che cattura la transitività dei modelli)

  3. l'assioma dell'introspezione negativa 5 (che cattura l'essere Euclideo dei modelli)

In questo caso l'assioma 4 è necessario. La differenza tra credere e conoscere sta dunque nell'assioma della verità T, presente nella conoscenza, che è sostituito con quello della coerenza D per catturare la credenza.

Dato che una relazione rilessiva è anche seriale, accettare l'assioma della verità implica accettare anche quello della coerenza. In altri termini sia la conoscenza che la credenza sono coerenti, ovvero non posso conoscere e non posso credere in una contraddizione (il falso). Inoltre, la conoscenza è più forte della credenza: se conosco un fatto allora credo in quel fatto. Ma non vale il viceversa: posso credere in qualcosa che non conosco (purché non conosca il suo contrario).

Tipicamente la conoscenza si associa al rigore (scientifico o matematico). Ad esempio conosco che la terra è sferica o che esistono infiniti numeri primi. La credenza è una modalità più debole e in generale posso credere in qualsiasi cosa che non sia una palese contraddizione. Ad esempio posso credere nell'esistenza della materia oscura o nel fatto che ogni numero pari maggiore di 2 sia la somma di due numeri primi (congettura di Goldbach), anche se non ho le prove scientifiche o matematiche di tali affermazioni. Ma non posso credere che la terra sia piatta o che esista un numero primo maggiore di tutti gli altri primi, dato che queste affermazioni non sono valide scientificamente (la terra è sferica) o matematicamente (i numeri primi sono infiniti).

Se volessimo rappresentare entrambe le modalità, conoscenza KaK_a e credenza BaB_a per ogni agente aa nello stesso linguaggio modale, occorre fare attenzione a come costruire i modelli di Kripke. Come abbiamo visto, le relazioni di accessibilità RaKR_{a}^{K} associate alla conoscenza e RaBR_{a}^{B} associate alla credenza hanno proprietà strutturali diverse (per esempio una è riflessiva e l'altra solo seriale), dunque vanno tenute distinte. Fissata la modalità, ovvero conoscenza o credenza, le relazioni di accessibilità per ogni agente hanno invece le stesse proprietà strutturali (godono degli stessi assiomi).

Conoscenza di gruppo

Nella vita ordinaria, ragioniamo su ciò che gli altri sanno. In particolare, ci preoccupiamo di ciò che gli altri sanno (o credono) di noi, e spesso in modo specifico di ciò che loro sanno di ciò che noi sappiamo.

Anna sa che Baldo sa che lei è incinta? Baldo sa questo?

La logica epistemica può rivelare interessanti caratteristiche epistemiche dei sistemi che coinvolgono gruppi di agenti. In alcuni casi, ad esempio, i fenomeni sociali emergenti dipendono dal fatto che gli agenti ragionano in modi particolari sulla conoscenza e sulle credenze di altri agenti.

Ad esempio, gli automobilisti sanno che un semaforo rosso indica che devono fermarsi a un incrocio. Tuttavia, affinché la convenzione dei semafori funzioni, è necessario che gli automobilisti sappiano che anche gli altri automobilisti sanno che il rosso significa stop. Il ruolo convenzionale dei semafori si basa sul fatto che tutti gli automobilisti sanno che tutti gli automobilisti conoscono la regola, ovvero che la regola è un elemento di conoscenza comune.

Vi sono tre tipi di conoscenza di gruppo: distribuita, mutua e comune. Facciamo un esempio. Il docente mantiene un canale Telegram dove partecipano gli studenti del corso. Per premiare gli studenti per il loro impegno ha deciso di creare un wallet bitcoin, depositare alcuni fondi, e condividere con gli studenti la relativa seed phrase (SP) del wallet. Può condividere la SP in diversi modi:

  1. suddivide la stringa della SP in tanti pezzi quanti sono gli studenti e invia in privato un pezzo ad ogni studente;

  2. confida ad ogni studente in privato l'intera SP;

  3. pubblica la SP sul canale in modo che tutti la vedano.

Le tre conoscenze sono diverse:

  • nel primo caso la SP è conoscenza distribuita. Ovvero se tutti gli studenti mettono assieme la loro conoscenza, ottengono la chiave d'accesso. Ma nessuno individualmente conosce la SP. Una volta prelevati i fondi, possono decidere come spartirseli (ad esempio in parti uguali o sorteggiando un vincitore);

  • nel secondo caso la SP è conoscenza mutua. Ogni studente conosce interamente la SP, ma non sa che gli altri la conoscono. Ad esempio, se la ricompensa andasse solo al primo che riesce ad accedere al wallet prelevando i fondi, in tal caso gli studenti non avrebbero fretta di prelevare i fondi, non sapendo di essere in competizione;

  • nel terzo caso la SP è conoscenza comune. Tutti sanno la SP e tutti sanno che tutti sanno la SP e così via all'infinito. Nel caso di competizione per la ricompensa, gli studenti si affretterebbero a prelevare i fondi, sapendo di essere in competizione con gli altri.

Si noti che la conoscenza mutua implica quella distribuita: se un agente del gruppo conosce qualcosa allora lo può distribuire al gruppo. Inoltre, la conoscenza comune implica quella mutua: se il gruppo ricorsivamente conosce qualcosa allora ogni agente del gruppo la conosce direttamente.

Conoscenza distribuita

La conoscenza distribuita è la conoscenza che un gruppo di agenti avrebbe se condividesse l'informazione che ognuno possiede. Gli agenti di un gruppo GG conoscono in modo distribuito φ\varphi se un ipotetico agente saggio che avesse tutta la conoscenza degli agenti del gruppo conosce φ\varphi.

Definiamo il nuovo operatore modale DGD_G per la conoscenza distribuita. La formula DGφD_G \varphi si legge: φ\varphi è conoscenza distribuita tra il gruppo di agenti in GG.

L'operatore DGD_G ha semantica sull'intersezione delle relazioni di accessibilità degli agenti in GG. L'idea è che se anche solo uno degli agenti esclude che un mondo sia accessibile dal mondo corrente, allora tale sarà per l'intero gruppo. Sia dunque:

RGD=aGRaR_{G}^{D} = \bigcap_{a \in G} R_a

Consideriamo l'esempio in figura:

Nell'esempio di sopra, solo i tre cappi sui nodi appartengono alla relazione RGDR_{G}^{D}, con G={a,b}G = \{a,b\}.

La semantica dell'operatore DGD_G è quindi:

M,sDGφM, s \vDash D_G \varphi sse M,tφM, t \vDash \varphi per ogni tt tale che (s,t)RGD(s, t) \in R_{G}^{D}

Nell'esempio di sopra, vale che w1DGpw_1 \vDash D_G \, p e w2DGpw_2 \vDash D_G \, p con G={a,b}G = \{a,b\}.

Conoscenza mutua

Gli agenti di un gruppo GG conoscono in modo mutuo φ\varphi se tutti gli agenti del gruppo conoscono singolarmente φ\varphi. La conoscenza mutua è un sottoinsieme di quella distribuita: conoscere mutuamente qualcosa implica che la si conosce anche in modo distribuito ma non vale il viceversa.

Possiamo quindi definire un nuovo operatore di conoscenza mutua EGE_G (everybody knows) definito nel seguente modo:

EGφ:=aGKaφE_G \varphi := \bigwedge_{a \in G} K_a \varphi

La formula EGφE_G \varphi is legge: φ\varphi è mutuamente conosciuta da tutti gli agenti del gruppo GG. Nell'esempio di sopra, se G={a,b}G = \{a,b\}, allora vale che w1EGpw_1 \vDash E_G \, p ma w2⊭EGpw_2 \not\vDash E_G \, p, in quanto w2⊭Kapw_2 \not\vDash K_a \, p.

Conoscenza comune

Il fatto che tutti gli agenti di un gruppo conoscano un fatto in prim'ordine non significa the conoscano quel fatto con un ordine superiore di conoscenza. Gli agenti di un gruppo GG conoscono in modo comune φ\varphi se ognuno conosce φ\varphi e ognuno sa che sé stesso e gli altri agenti conoscono φ\varphi e così via ab infinitum. In altri termini, usando una definizione ricorsiva:

φ\varphi è conoscenza comune se tutti gli agenti conoscono φ\varphi e tutti gli agenti ricorsivamente sanno che φ\varphi è conoscenza comune.

La conoscenza comune è dunque la più restrittiva tra quelle analizzate ed in particolare è un sottoinsieme di quella mutua (e quindi anche di quella distribuita). Nell'esempio di sopra, vale che w1KapKbpw_1 \vDash K_a p \wedge K_b p ma w1⊭KbKapw_1 \not\vDash K_b K_a p.

Potremmo pensare di definire l'operatore modale di conoscenza comune CGC_G in termini di quello di conoscenza mutua EGE_G come segue:

CGφ:=k0EGkφC_G \varphi := \bigwedge_{k \geq 0} E_{G}^{k} \varphi

dove EGkE_{G}^{k} indica kk applicazioni di EGE_{G}, ovvero:

  • EG0φ=φE_{G}^{0} \varphi = \varphi

  • per k>0k > 0, EGkφ=EGEGk1φE_{G}^{k} \varphi = E_G E_{G}^{k-1}\varphi

Ad esempio, se G={a,b}G = \{a,b\}, allora:

EG2φ=EGEGφ=EG(KaφKbφ)=Ka(KaφKbφ)Kb(KaφKbφ)=KaKaφKaKbφKbKaφKbKbφ\begin{array}{l} E_{G}^{2} \,\varphi = E_{G} E_{G} \varphi = E_G (K_a \varphi \wedge K_b \varphi) = \\ K_a (K_a \varphi \wedge K_b \varphi) \wedge K_b (K_a \varphi \wedge K_b \varphi) = \\ K_a K_a \varphi \wedge K_a K_b \varphi \wedge K_b K_a \varphi \wedge K_b K_b \varphi \end{array}

dove nell'ultimo passaggio abbiamo usato la proprietà distributiva del quantificatore universale KK rispetto alla congiunzione \wedge.

Questa definizione di conoscenza comune è però problematica, in quanto la formula con cui abbiamo definito CGφC_G \varphi è infinita, mentre il nostro linguaggio modale contiene solo formule finite. Procediamo dunque in modo diverso. Definiamo una nuova relazione di accessibilità per la conoscenza comune come la chiusura riflessiva e transitiva dell'unione delle relazioni di accessibilità degli agenti del gruppo, ovvero:

RGC=(aGRa)R_{G}^{C} = (\bigcup_{a \in G} R_a)^*

Data una relazione RR, la sua chiusura riflessiva e transitiva

R=k0RkR^* = \bigcup_{k \geq 0} R^k

dove:

  • (s,t)R0(s, t) \in R^0 sse s=ts = t

  • per k>0k > 0, abbiamo che (s,t)Rk(s, t) \in R^{k} sse esiste rr tale che (s,r)R(s, r) \in R e (r,t)Rk1(r, t) \in R^{k-1}

In termini topologici, RkR^{k} rappresenta la relazione cammino di lunghezza kk e RGCR_{G}^{C} è la relazione cammino di lunghezza arbitraria sul grafo che contiene l'unione delle relazioni degli agenti nel gruppo GG, ovvero un mondo tt è accessibile da un mondo ss attraverso RGCR_{G}^{C} se esiste un cammino - una sequenza di nodi uniti da archi - di lunghezza finita (possibilmente nulla) da ss a tt sul grafo formato dalle relazioni degli agenti nel gruppo GG.

La semantica dell'operatore CGC_G è quindi:

M,sCGφM, s \vDash C_G \varphi sse M,tφM, t \vDash \varphi per ogni tt tale che (s,t)RGC(s, t) \in R_{G}^{C}

Nell'esempio di sopra, vale che w1⊭CGpw_1 \not\vDash C_G p dato che w3w_3 è raggiungibile da w1w_1 attraverso un cammino di lunghezza 2 che passa prima per un arco di bb e poi un arco di aa; inoltre in w3w_3 non vale pp. In altri termini, w1⊭KbKapw_1 \not\vDash K_b K_a p.

E' facile mostrare che la seguente formula, che caratterizza la gerarchia tra le conoscenze di gruppo, è valida in tutti i modelli per ogni agente aGa \in G e formula φ\varphi:

(CGφEGφ)(EGφKaφ)(KaφDGφ)(C_G \varphi \rightarrow E_G \varphi) \wedge (E_G \varphi \rightarrow K_a \varphi) \wedge (K_a \varphi \rightarrow D_G \varphi)

Assiomatizzazione

Finora la formalizzazione del ragionamento è stata definita in base alla nozione di verità: Xφ{\cal X} \vDash \varphi significa che φ\varphi è vera in tutti i modelli di X\cal X.

In questa sezione, discutiamo una forma di ragionamento in cui una conclusione è inferita puramente sulla base della sua forma sintattica. Sebbene esistano diversi modi per farlo, nella logica epistemica il modo più diffuso per definire l'inferenza deduttiva è la definizione di un sistema di assiomi alla Hilbert. Tali sistemi forniscono una nozione molto semplice di prova formale. Alcune formule sono valide a priori solo perché hanno una certa forma sintattica. Questi sono gli assiomi del sistema. Le regole del sistema dicono che si può concludere che una formula è un valida perché altre formule sono valide.

Cominciamo col definire un sistema assiomatico di base chiamato K su un linguaggio modale L=L(At,Op,Ag)L = L(At, Op, Ag) con Op={Ka  aAg}Op = \{K_a \ | \ a \in Ag\}.

  1. Assioma 1. Tutte le istanze di sostituzione delle tautologie proposizionali

  2. Assioma K. (KaφKa(φψ))Kaψ(K_a \varphi \wedge K_a (\varphi \rightarrow \psi)) \rightarrow K_a \psi per ogni aAga \in Ag

  3. Regola MP (modus ponens). Da φ\varphi e φψ\varphi \rightarrow \psi deriva ψ\psi

  4. Regola Nec (regola della necessità). Da φ\varphi deriva KaφK_a \varphi per ogni aAga \in Ag

Una prova formale (detta anche dimostrazione o derivazione) è un elenco di formule, dove ogni formula è un assioma del sistema o può essere ottenuta applicando una regola di inferenza del sistema alle formule che si trovano prima nell'elenco. Una prova di φ\varphi è una derivazione la cui ultima formula è φ\varphi. Se esiste una prova di φ\varphi nel sistema di assiomi K diremo che φ\varphi è un teorema di K e scriveremo Kφ\mathbf{K} \vdash \varphi.

La seguente figura mostra un esempio di prova in K per il seguente teorema:

KKa(φψ)(KaφKaψ)\mathbf{K} \vdash K_a (\varphi \wedge \psi) \rightarrow (K_a \varphi \wedge K_a \psi)
La dimostrazione del teorema

Si noti che la tautologia al passo 9 è della forma: (αβ)((αγ)(α(βγ)))(\alpha \rightarrow \beta) \rightarrow ((\alpha \rightarrow \gamma) \rightarrow (\alpha \rightarrow (\beta \wedge γ))). Questo teorema può essere usato, assieme agli assiomi e alle regole del sistema logico, per dimostrarne altri. Osserviamo che questo teorema è anche una formula valida nella classe X\cal X di tutti i modelli di Kripke. Infatti, la quantificazione universale KaK_a distribuisce rispetto alla congiunzione \wedge: se in ogni mondo accessibile valgono entrambe φ\varphi e ψ\psi, allora in ogni mondo accessibile vale φ\varphi e inoltre in ogni mondo accessibile vale ψ\psi. Quindi possiamo anche scrivere:

KKa(φψ)(KaφKaψ)\cal{K} \vDash K_a (\varphi \wedge \psi) \rightarrow (K_a \varphi \wedge K_a \psi)

Questa corrispondenza tra sintassi e semantica, ovvero tra derivabilità (mediante una prova, o proof-theoretic) e validità (su una classe di modelli, o model-theoretic), è una delle proprietà fondamentali di un sistema logico. In particolare, se LL è un linguaggio, X\cal X una classe di modelli, e X un sistema di assiomi, diremo che:

  1. X è corretto (sound in Inglese) rispetto a X\cal X e LL se ogni teorema in X è una formula valida in X\cal X, ovvero Xφ\mathbf{X} \vdash \varphi implica Xφ\cal{X} \vDash \varphi;

  2. X è completo (complete in Inglese) rispetto a X\cal X e LL se ogni formula valida in X\cal X è un teorema in X, ovvero Xφ\cal{X} \vDash \varphi implica Xφ\mathbf{X} \vdash \varphi.

Possiamo estendere il sistema logico K con altri assiomi per la conoscenza e la credenza, in particolare:

  1. T: KaφφK_a \varphi \rightarrow \varphi (riflessività)

  2. D: MaM_a \top (serialità)

  3. B: φKaMaφ\varphi \rightarrow K_a M_a \varphi (simmetria)

  4. 4: KaφKaKaφK_a \varphi \rightarrow K_a K_a \varphi (transitività)

  5. 5: ¬KaφKa¬Kaφ\neg K_a \varphi \rightarrow K_a \neg K_a \varphi (proprietà Euclidea)

Ad esempio, indicheremo con KT il sistema logico che estende K con T e KT5 il sistema logico che estende K con T e 5.

Fissato il linguaggio della logica epistemica L=L(At,Op,Ag)L = L(At, Op, Ag) con Op={Ka  aAg}Op = \{K_a \ | \ a \in Ag\} vale che:

  1. K è corretto e completo rispetto a K\cal K (qualsiasi modello)

  2. KT è corretto e completo rispetto a KT\cal KT (modelli riflessivi)

  3. KD è corretto e completo rispetto a KD\cal KD (modelli seriali)

  4. KB è corretto e completo rispetto a KB\cal KB (modelli simmetrici)

  5. K4 è corretto e completo rispetto a K4\cal K4 (modelli transitivi)

  6. K5 è corretto e completo rispetto a K5\cal K5 (modelli Euclidei)

Questi risultati si estendono ad ogni combinazione di assiomi, ad esempio il sistema S5, ovvero KT5, è corretto e completo rispetto ai modelli con relazione di equivalenza S5\cal S5.

La dimostrazione della correttezza è semplice: basta dimostrare che gli assiomi del sistema logico sono validi e poi per induzione che il processo di dimostrazione che usa le regole logiche preserva la validità. Dimostrare la completezza è un po' più difficile. Esistono diversi approcci, ma quello comune consiste nel dimostrare che se una formula non è dimostrabile, allora esiste un modello in cui è falsa. Esiste un modello speciale, chiamato modello canonico, che lo dimostra simultaneamente per tutte le formule.

Possiamo anche definire assiomi per la conoscenza di gruppo, ovvero per i due operatori CGC_G (conoscenza comune) e DGD_G (conoscenza distribuita) per cui abbiamo dovuto introdurre nuove relazioni di accessibilità.

Per quanto riguarda la conoscenza distribuita basta introdurre come minimo un assioma che afferma che la conoscenza dei singoli agenti è conoscenza distribuita: KaφDGφK_a \varphi \rightarrow D_G \varphi per ogni aGa \in G. Altri assiomi, ad esempio quello della riflessività, possono essere introdotti per caratterizzare ulteriormente la relazione di accessibilità.

Per la conoscenza comune, occorre aggiungere un assioma e una regola:

  1. Assioma Fix: CGφEG(φCGφ)C_G \varphi \rightarrow E_G(\varphi \wedge C_G \varphi)

  2. Regola Ind: Da φEG(φ)\varphi \rightarrow E_G (\varphi) segue φCGφ\varphi \rightarrow C_G \varphi

L'assioma del punto fisso Fix dice che la conoscenza comune può essere vista come il punto fisso di un'equazione: la conoscenza comune di φ\varphi è valida se tutti sanno sia che φ\varphi è valida sia che φ\varphi è, ricorsivamente, una conoscenza comune.

Ind è chiamata regola di induzione e può essere utilizzata per derivare la conoscenza comune induttivamente. Se è vero che φ\varphi è "evidente", nel senso che se è vera, allora tutti la conoscono (ad esempio perché la scriviamo in un posto dove tutti la possono leggere), allora possiamo dimostrare per induzione che se φ\varphi è vera, allora lo è anche EGk(φ)E_{G}^{k} (\varphi) per tutti i k0k \geq 0, ma questo significa che CGφC_G \varphi è vera. Sebbene la conoscenza comune sia stata definita come un operatore infinito, un po' sorprendentemente questi assiomi e regole finite la caratterizzano completamente.

Problemi logici e relativa complessità

Dato un linguaggio LL e una classe di modelli X\cal X, possiamo indagare almeno i seguenti problemi:

  1. Soddisfacibilità: Data una formula φL\varphi \in L, verificare se esiste un modello MXM \in \cal{X} e un mondo ww del modello MM tale che M,wφM, w \vDash \varphi

  2. Validità: Data una formula φL\varphi \in L, verificare se per tutti i modelli MXM \in \cal{X} e per ogni mondo ww del modello MM vale che M,wφM, w \vDash \varphi

  3. Verifica di modello (model checking): Data una formula φL\varphi \in L, un modello MXM \in \cal{X} e un mondo ww del modello MM, verificare se M,wφM, w \vDash \varphi

Il campo della complessità computazionale si occupa della questione della quantità di risorse necessarie per risolvere un problema specifico. Le risorse di maggiore interesse sono il tempo di calcolo e lo spazio di memoria. La complessità computazionale pone quindi domande del tipo: se il mio input aumentasse di dimensione, quanto spazio e tempo in più sarebbero necessari per calcolare la risposta? Formulare la domanda in questo modo presuppone già che il problema in questione possa essere risolto in tempo finito con un algoritmo, cioè che il problema sia decidibile (si noti che esistono problemi indecidibili). Fortunatamente, questo è il caso dei problemi elencati sopra.

Per ragionare sulla complessità di un algoritmo, distinguiamo varie classi di complessità. Se un algoritmo deterministico può risolvere un problema in un tempo polinomiale rispetto alla dimensione dell'input, si dice che il problema è in P. E' possibile mostrare che il problema del model checking per la logica modale epistemica (con molti agenti) è polinomiale.

La classe NP è la classe dei problemi risolvibili da un algoritmo non deterministico in tempo polinomiale. Un algoritmo non deterministico è in un certo senso molto più potente di uno deterministico, perché può indagare in parallelo una pluralità di possibili scelte. Se immaginiamo queste scelte rappresentate da una struttura ad albero, un algoritmo deterministico deve percorrere una dopo l'altro, ovvero sequenzialmente, i cammini di scelta, mentre un algoritmo non deterministico li elabora in modo parallelo.

La soddisfacibilità della logica proposizionale è un esempio di problema in NP: un algoritmo non deterministico di soddisfacibilità prima sceglie una tra le tante assegnazioni di verità per le proposizioni primitive e poi verifica che la formula sia effettivamente vera sotto questa assegnazione di verità.

Un problema che è difficile almeno come qualsiasi problema in NP è detto NP-hard. Un problema è NP-completo se è sia in NP che NP-hard; è noto che il problema della soddisfacibilità per la logica proposizionale è NP-completo. Queste definizioni si generalizzano a tutte le classi di complessità.

Nessuno ha ancora dimostrato se P = NP o meno. La congettura corrente è che P sia un sottoinsieme stretto di NP (si noti infatti che ogni problema polinomiale in modo deterministico è anche polinomiale in maniera non deterministica). I problemi NP-completi sono dunque considerati problemi difficili da risolvere, ovvero con complessità più che polinomiale e tipicamente utilizzano un tempo esponenziale rispetto alla dimensione dell'input.

Infine, PSPACE è la classe dei problemi risolvibili usando spazio polinomiale rispetto alla dimensione dell'input e EXPTIME è la classe dei problemi risolvibili in un tempo esponenziale rispetto alla dimensione dell'input. Si sa che:

PNPPSPACEEXPTIME

Abbiamo che:

  1. Il problema della soddisfacibilità per le logiche della conoscenza e della credenza per un solo agente, S5\cal S5 e KD45\cal KD45, è esattamente difficile come il problema della soddisfacibilità per la logica proposizionale, ovvero NP-completo;

  2. Il caso generale multi-agente (senza conoscenza comune) è PSPACE-completo;

  3. Il caso generale multi-agente con conoscenza comune è EXPTIME-completo.

La complessità del problema della validità è equivalente a quella della soddisfacibilità.

Mostriamo infine che il problema del model checking per la logica epistemica ha complessità polinomiale, in particolare lineare nel prodotto della lunghezza della formula da verificare e la dimensione del modello. La seguente procedura implementa un model checker per la logica epistemica multi-agente. L'idea è di etichettare ogni mondo del modello con le sotto-formule della formula da verificare che sono vere in quel mondo, partendo dalle variabili proposizionali e incrementando progressivamente la dimensione della sotto-formula fino ad arrivare alla formula da verificare.

Sia n=Sn = |S| il numero di mondi del modello, m=aRam = |\bigcup_a R_a| il numero di archi del modello e kk la lunghezza della formula α\alpha, ovvero il numero di operatori più il numero di proposizioni presenti della formula. Si noti che il numero di sottoformule in Sub(α)Sub(\alpha) è kk. Quindi, il ciclo principale della procedura viene eseguito per kk volte. I casi booleani costano O(n)O(n) e il caso modale costa O(n+m)O(n + m). Pertanto, la complessità del model checking risulta O(k(n+m))O(k \cdot (n + m)) nel caso peggiore. La complessità è dunque lineare nel prodotto della lunghezza della formula e della dimensione del modello.

Si consideri il modello su un solo agente anonimo M=(S,R,V)M = (S, R, V) con:

  • S={a,b,c,d}S = \{a,b,c,d\}

  • R={(a,b),(b,a),(b,c),(c,b),(c,d),(d,c),(d,a),(a,d)}R = \{(a,b), (b,a), (b,c), (c,b), (c,d), (d,c), (d,a), (a,d)\} (un quadrato simmetrico)

  • V(a)=V(a) = \emptyset, V(b)={p}V(b) = \{p\}, V(c)={q}V(c) = \{q\}, V(d)={p,q}V(d) = \{p,q\}.

Si consideri inoltre la formula α=KpM¬q\alpha = K p \wedge M \neg q. Usando l'algoritmo del model checking, etichettare ogni stato del modello con le sottoformule di α\alpha vere in quello stato e infine identificare gli stati in cui α\alpha è vera.

Limiti dell'approccio logico

L'approccio logico ha dei limiti pratici e concettuali. Come abbiamo visto, ragionare con la logica epistemica è un problema computazionalmente difficile, in particolare se deve essere affrontato in tempo reale. Solo la verifica di modello, infatti, è un problema trattabile computazionalmente. Viceversa, verificare se un formula è un teorema (è valida) ha complessità esponenziale nella lunghezza della formula. Se la formula è moderatamente lunga, o peggio se è dinamica e cresce in lunghezza nel tempo, la complessità del ragionamento logico diventa proibitiva.

Da un punto di vista concettuale, occorre tenere presente che gli assiomi della conoscenza sono idealizzazioni e, in effetti, i logici non sostengono che siano validi per tutte le possibili interpretazioni della conoscenza. Vediamo alcune criticità.

È umano affermare un giorno di conoscere un certo fatto, per poi ritrovarsi ad ammettere il giorno dopo di essersi sbagliati, il che mette in crisi l'assioma T - KφφK \varphi \rightarrow \varphi - che afferma che se un agente conosce un fatto allora questo è vero. Ad esempio, alcuni teoremi matematici sono stati creduti veri per un lasso di tempo, salvo poi riscontrare che non lo erano, ovvero trovare un errore nella dimostrazione. Allo stesso modo, alcune teorie scientifiche sono state invalidate col tempo.

Anche l'introspezione positiva è stata considerata problematica. L'assioma 4 - KφKKφK \varphi \rightarrow KK\varphi - afferma che se un agente sa un fatto allora sa di saperlo. Ma, ad esempio, si consideri un allievo a cui viene posta una domanda di cui non conosce la risposta. Può darsi che, ponendo altre domande, l'allievo sia in grado di rispondere prima o poi alla domanda originale. A quanto pare, l'allievo conosceva la risposta, ma non era consapevole di saperlo, quindi non sapeva di conoscere la risposta (si parla di memoria inconsapevole).

L'assioma più discutibile è quello dell'introspezione negativa, ovvero 5 - ¬KφK¬Kφ\neg K \varphi \rightarrow K \neg K\varphi - che afferma che se non conosco un fatto, so di non saperlo. È possibile che un lettore di questo corso non sappia (ancora) cos'è una rete neurale ricorrente, perché non l'ha mai sentita nominare, ma prima di leggere questa frase sapeva di non saperlo?

L'effetto Dunning-Kruger è un fenomeno psicologico secondo cui le persone inesperte o poco competenti in un determinato ambito tendono a sovrastimare notevolmente le proprie abilità e conoscenze. Al contrario, le persone esperte o molto competenti tendono a sottostimare la propria competenza. Ad esempio, una persona sta iniziando a investire in borsa e pensa erroneamente di conoscere tutti i concetti necessari, ma in realtà ignora fondamentali aspetti tecnici. In generale, chi ha poche informazioni su temi complessi tende spesso ad avere opinioni più radicali e a considerarle più affidabili rispetto a chi è molto informato e consapevole della complessità.

Questi esempi suggeriscono che una ragione dell'ignoranza può essere la mancanza di consapevolezza.

Si potrebbe sostenere che gli assiomi "problematici" per la conoscenza dovrebbero essere semplicemente omessi, o forse indeboliti, per ottenere un sistema appropriato per la conoscenza. Ma che dire dei principi fondamentali della logica modale, l'assioma K e la regola di inferenza Nec? Quanto sono accettabili per la conoscenza? Come ci si potrebbe aspettare, non dobbiamo dare nulla per scontato.

L'assioma K di distribuzione della conoscenza - (KφK(φψ))Kψ(K \varphi \wedge K (\varphi \rightarrow \psi)) \rightarrow K \psi - presuppone ragionatori perfetti, in grado di inferire le conseguenze logiche della loro conoscenza. Può accadere di conoscere dei fatti ma di non averli messi in relazione, e quindi di non aver dedotto una conseguenza. Per esempio, questo assioma implica che un agente sa che giorno della settimana sarà il 26 luglio 5018, assumendo che l'agente conosca la data e il giorno della settimana di oggi e conosca le regole del calendario.

La regola Nec della necessità afferma che se φ\varphi è valida allora lo è anche KφK \varphi. La necessità presuppone che gli agenti possano inferire tutti i teoremi del sistema logico. Poiché dire se una formula è valida è computazionalmente difficile, questo non sembra così plausibile. Questa idealizzazione è spesso riassunta come onniscienza logica: il nostro agente conoscerebbe tutto ciò che è logicamente deducibile.

In sostanza, il problema è che agenti finiti, biologici o artificiali, sono vincolati da limiti alle loro capacità cognitive e di ragionamento. L'approccio della logica epistemica e doxastica sembra invece implicare abilità sovrumane come la conoscenza di tutte le tautologie. Pertanto, la preoccupazione è che queste logiche siano semplicemente inadatte a catturare la conoscenza e la credenza reali, così come queste nozioni figurano nella vita umana ordinaria.

Curiosamente, il fatto che, nella realtà, gli agenti non siano ragionatori ideali, né logicamente onniscienti, è talvolta una caratteristica sfruttata dai sistemi computazionali. La crittografia, ad esempio, è utile perché gli intrusi artificiali o umani, a causa delle loro capacità limitate, non sono in grado di calcolare i fattori primi di un grande numero in un tempo ragionevole.

Nonostante questi problemi, le proprietà della logica della conoscenza si sono dimostrate essere un'utile idealizzazione della conoscenza per molte applicazioni nel campo dei sistemi distribuiti e dell'economia.

Last updated

Was this helpful?