Dynamic Hypersequents for Public Announcement Logic

Sintesi Tecnica: Ipersequenze Dinamiche per la Logica dell'Annuncio Pubblico

Enunciato del Problema
La Logica Epistemica Dinamica (DEL), e in particolare la Logica dell'Annuncio Pubblico (PAL), modella l'evoluzione della conoscenza attraverso aggiornamenti informativi. Sebbene la semantica della PAL sia ben compresa come trasformazione di modelli di Kripke (dove un annuncio restringe l'insieme dei mondi possibili), i quadri esistenti di teoria della dimostrazione faticano a catturare questa dinamicità a livello sintattico. I tentativi precedenti, inclusi i metodi dei tableaux e vari calcoli dei sequenti (etichettati e non etichettati), spesso falliscono nel raggiungere simultaneamente una genuina proprietà del sottoformula, l'ammissibilità di tutte le regole strutturali (inclusa la contrazione) e l'eliminazione sintattica del taglio. Molti sistemi esistenti si basano su assiomi di riduzione che traducono formule dinamiche in formule statiche, oscurando così la natura dinamica della logica all'interno del sistema di dimostrazione stesso.

Metodologia
Gli autori propongono un nuovo quadro di teoria della dimostrazione basato su ipersequenze dinamiche. Questo approccio estende il calcolo delle ipersequenze per S5 (introdotto in [15, 16]) incorporando un meccanismo per modellare le transizioni tra modelli epistemici indotte da annunci pubblici.

1. Sequenze Dinamiche: Una sequenza dinamica è definita come una sequenza di sequenti standard etichettati da sequenze finite distinte di annunci (ad esempio, $\alpha_1 \Gamma_1 | \dots | \alpha_n \Gamma_n$). Intuitivamente, una sequenza dinamica rappresenta un mondo specifico $w$ in un modello iniziale $M$ e le sue "copie" in modelli aggiornati successivamente $M_{\alpha}$.
2. Ipersequenze Dinamiche (DHS): Un'ipersequenza dinamica è una collezione di sequenze dinamiche. Questa struttura rappresenta sintatticamente un intero modello epistemico e i suoi aggiornamenti successivi simultaneamente. Gli autori interpretano una DHS come una disgiunzione di formule incassate, dove ogni componente corrisponde a un mondo nel modello o ai suoi aggiornamenti.
3. Il Calcolo ($DHSPAL$): Gli autori definiscono un calcolo $DHSPAL$ comprendente:
   • Regole Proposizionali e Modali: Adattate dai calcoli standard delle ipersequenze per S5.
   • Regole di Annuncio: Regole $(L[\cdot])$ e $(R[\cdot])$ che decompongono le formule di annuncio pubblico $[A]B$. Queste regole gestiscono esplicitamente la transizione da uno stato corrente a uno stato aggiornato introducendo nuove sequenze dinamiche etichettate con la sequenza di annunci estesa $\alpha \cdot A$.
   • Regole Strutturali Dinamiche: Regole specifiche come $(Lat)$e$(Rat)$ (Permanenza Atomica), $(New)$ (assicurando che i mondi nei modelli aggiornati esistano in quelli precedenti) e $(Recall)$ (assicurando che la formula annunciata valga nel modello precedente).
   • Regola Modale Dinamica: Una regola specializzata $(L\Box_3)$ che gestisce l'interazione tra conoscenza ($\Box$) e sequenze di annunci, distinguendo tra i mondi che sopravvivono a un aggiornamento e quelli che non lo fanno.

Contributi e Risultati Chiave
Il documento stabilisce che $DHSPAL$ è un sistema di dimostrazione robusto per la PAL, raggiungendo diverse proprietà che i sistemi precedenti non possedevano simultaneamente:

• Ammissibilità delle Regole Strutturali: Gli autori dimostrano l'ammissibilità hp (che preserva l'altezza) dell'indebolimento, della contrazione e di una regola di unione. Crucialmente, ciò include la contrazione, che è spesso difficile da ottenere nelle logiche dinamiche senza perdere l'analiticità.
• Invertibilità delle Regole Logiche: Tutte le regole logiche nel calcolo sono mostrate essere hp-invertibili. Questa proprietà è essenziale per la ricerca di dimostrazioni e per stabilire l'eliminazione del taglio.
• Eliminazione Sintattica del Taglio: Il documento fornisce una prova dell'ammissibilità della regola del Taglio. La prova si basa su una doppia induzione: una sulla complessità DHS della formula di taglio (una misura di complessità relativa alla sequenza di annunci) e un'altra sulla somma delle altezze delle derivazioni delle premesse.
• Correttezza e Completezza: Il calcolo è dimostrato corretto e completo rispetto alla semantica standard di Kripke della PAL. La prova di completezza comporta la derivazione di tutti gli assiomi in stile Hilbert della PAL, inclusi gli assiomi di riduzione, all'interno del quadro delle ipersequenze dinamiche.
• Proprietà del Sottoformula: Come conseguenza dell'eliminazione del taglio, il calcolo gode della proprietà del sottoformula, garantendo che qualsiasi formula in una derivazione sia un sottoformula del sequente finale o di un annuncio che vi si verifica.

Significato e Affermazioni
Gli autori affermano che questo lavoro rappresenta un passo significativo verso la colmatura del divario tra la dinamicità semantica della PAL e la sua teoria della dimostrazione sintattica. Utilizzando le ipersequenze dinamiche, il sistema cattura il carattere dinamico della logica attraverso mezzi puramente strutturali, evitando la necessità di elementi semantici espliciti (come etichette per i mondi) o la riduzione alla logica statica.

Il documento afferma che, per quanto ne sappiano, $DHSPAL$ è il primo calcolo per la PAL che soddisfa simultaneamente:

1. Ammissibilità di tutte le regole strutturali (inclusa la contrazione).
2. Invertibilità di tutte le regole logiche.
3. Eliminazione sintattica del taglio.
4. Una genuina proprietà del sottoformula.

Gli autori concludono che il quadro delle ipersequenze dinamiche è sufficientemente espressivo e robusto da servire come fondamento per lo sviluppo di calcoli dei sequenti per classi più ampie di logiche epistemiche dinamiche che coinvolgono diversi tipi di aggiornamenti informativi. Suggeriscono che un lavoro futuro potrebbe esplorare la decidibilità, l'interpolazione e l'analisi della complessità all'interno di questo quadro.