La logica dinamica è un'estensione della logica modale originariamente definita per il ragionamento di programmi e in seguito applicata a compiti più generali e complessi derivati dalla linguistica, dalla filosofia, dall'intelligenza artificiale e da altri campi.
Linguaggio
La logica modale è caratterizzata dagli operatori modali p (box p), indica che p è necessariamente vero, e p (diamond p) indica che p è possibile. La logica dinamica estende questa possibilità associando ad ogni azione a gli operatori modali [a] e <a>, così da renderla una logica multimodale. Il significato di [a]p è che in seguito all'esecuzione di un'azione a è necessario che valga p, quindi, ad a deve seguire p. Il significato di <a>p è che in seguito all'esecuzione di a è possibile che valga p, quindi, ad a può seguire p. Questi operatori sono correlati con [a]p ≡ ¬<a>¬ p e <a>p ≡ ¬[a]¬ p, analogamente alla relazione tra i quantificatori esistenziali e universali.
La logica dinamica permette di comporre azioni a partire da azioni più piccole. Si potrebbero utilizzare operatori di controllo di base di qualsiasi linguaggio di programmazione per tale scopo; gli operatori delle espressioni regolari di Kleene sono una buona scelta per la logica modale. Date le azioni a e b, l'azione composta a∪b, la scelta, anche scritta come a+b o a|b, è eseguita eseguendo l'azione a o l'azione b. L'azione composta a;b, sequenza, è eseguita eseguendo prima a e successivamente b. L'azione composta a*, iterazione, è eseguita eseguendo a zero o più volte, in sequenza. L'azione costante 0 o BLOCK non effettua nulla e non termina, mentre l'azione 1 o SKIP o NOP definibile con 0*, non effettua nulla ma termina.
Assiomi
Questi operatori possono essere assiomatizzati nella logica dinamica come segue, prendendo come già data una pratica assiomatizzazione di logica modale includendo tali assiomi per gli operatori modali, come l'assioma citato in precedenza [a]p = <a> p e le due regole di inferenza modus ponens (p, p→qq) e la necessità (p [a]p).
A1. p
A2. p ≡ p
A3. [a∪b]p ≡ [a]p ∧ [b]p
A4. [a;b]p ≡ [a][b]p
A5. [a*]p ≡ p ∧ [a][a*]p
A6. p ∧ [a*](p → [a]p) → [a*]p
L'assioma A1 fa la promessa a vuoto che quando BLOCK termina, p varrà, anche se p è la proposizione falso (A1 estrae l'essenza della nozione di congelare l'inferno). A2 dice che [NOP] agisce sulle proposizioni come la funzione identità, ovvero, trasforma p in se stessa. A3 dice che se eseguendo una scelta fra a e b viene causata p, allora sia a sia b' devono causare p. A4 dice che se eseguendo la sequenza composta da a e b si giunge a p, l'esecuzione di a deve condurre a una situazione in cui l'esecuzione di b conduca a p. A5 è l'evidente risultato dell'applicazione di A2, A3 e A4 all'equazione a* = 1?a;a* dell'algebra di Kleene. A6 asserisce che se p vale ora, e indipendentemente da quante volte si esegue a permane il caso che la verità di p dopo tali esecuzioni si mantiene dopo un'ulteriore esecuzione di a, allora p deve rimanere vera indipendentemente dalle esecuzioni di a. A6 è riconoscibile come l'induzione matematica con l'azione n:=n+1 di incrementare n generalizzato dalle arbitrarie azioni a.
Conseguenze
L'assioma modale logico [a]p = <a> p permette la derivazione dei seguenti sei teoremi corrispondenti ai succitati assiomi.
T1. ¬<0>p
T2. <1>p ≡ p
T3. <a∪b>p ≡ <a>p ∨ < b>p
T4. <a;b>p ≡ <a>< b>p
T5. <a*>p ≡ p ∨ <a><a*>p
T6. <a*>p → p ∨ <a*>(¬p ∧ <a>p)
T1 asserisce l'impossibilità di accettare qualsiasi cosa con il verificarsi di BLOCK. T2 afferma ancora che NOP non cambia niente, tenendo a mente che NOP è sia deterministico e termina dove e <1> hanno la stessa forza. T3 dice che se la scelta di a o b può portare a p, allora sia a sia b possono portare a p. T4 è analogo ad A4. T5 si spiega come A5. T6 asserisce che se è possibile causare p eseguendo a sufficientemente a lungo, allora o p è vero ora oppure è possibile eseguire ripetutamente a per causare una situazione in cui p è (ancora) falso ma un'ulteriore esecuzione di a può causare p. Box e diamond sono completamente simmetrici riguardo a quale dei due è preso come primitiva. Un'assiomatizzazione alternativa potrebbe prendere i teoremi T1-T6 come assiomi, dai quali si possono derivare A1-A6 come teoremi. La differenza tra implicazione e inferenza è la stessa nella logica dinamica come in qualsiasi altra logica: laddove l'implicazione p→q asserisce che se p è vero allora lo è anche q, l'inferenza pq afferma che se p è valida lo è anche q. Comunque la natura dinamica della logica dinamica sposta questa distribuzione fuori dal reame delle assiomatizzazioni astratte dentro l'esperienza del senso comune di situazioni concrete. La regola di inferenza p[a]p per esempio è corretta perché la sua premessa afferma che p è sempre vera, quindi non importa dove a può portare, p alla fine sarà vera. L'implicazione p→[a]p invece non è sempre valida perché l'attuale verità di p non garantisce della verità di p dopo l'esecuzione di a. Per esempio p?[a]p sarà vera in qualsiasi situazione dove p è falsa, o in qualsiasi situazione in cui [a]p è vera, ma l'affermazione x=1 → [x:=x+1]x=1 è falsa in qualsiasi situazione dove x ha valore 1, e quindi non è valida.
Regole di inferenza derivate
Come per la logica modale, le regole di inferenza, modus ponens e necessità sono sufficienti anche per la logica dinamica come le sole regole primitive di cui ha bisogno, come osservato prima. Comunque come è d'uso in logica ulteriori regole possono essere derivate da queste con l'aiuto degli assiomi. Un esempio dimostrativo di queste regole derivate in logica dinamica è che prendendo a calci una volta la TV rotta non è possibile aggiustarla, quindi prendendola a calci ripetutamente diviene ancora più impossibile ripararla. Scrivendo k per l'azione del prendere a calci la TV e b per la proposizione che la TV è rotta, la logica dinamica esprime questa inferenza come b?[k]b b→[k*]b, avendosi come premessa b → [k]b e come conclusione b → [k*]b. Il significato di [k]b è che è garantito che dopo aver preso a calci la TV, essa è rotta. Quindi la premessa b → [k]b significa che se la TV è rotta, dopo averla presa un'altra volta a calci essa sarà ancora rotta. k* denota l'azione di prendere a calci la TV zero o più volte. Quindi la conclusione b ?[k*]b che se la TV è rotta, allora dopo averla presa a calci zero o più volte sarà ancora rotta. Se non fosse così, allora dopo il penultimo calcio la TV sarebbe nella condizione in cui dandogli un altro calcio si aggiusterebbe, ma la premessa lo esclude in ogni circostanza.
L'inferenza b→[k]b b→[k*]b è corretta. Comunque l'implicazione (b→[k]b) → (b?[k*]b) non è valida perché possiamo facilmente trovare una situazione in cui b→[k]b vale ma b→[k*]b no. In qualsiasi controesempio di tal genere b deve valere ma [k*]b deve essere falsa, mentre [k]b deve essere comunque vera. Ma questo può avvenire in qualsiasi situazione in cui la TV è rotta ma può essere aggiustata con due calci. L'implicazione fallisce perché richiede solo che b→[k]b valga ora, laddove l'inferenza riesce perché richiede che b→[k]b valga in tutte le situazioni, non solo in quella corrente.
Un esempio di implicazione valida è la proposizione x≥3 → [x:=x+1]x≥4 . Afferma infatti che se x è maggiore o uguale a 3, allora dopo aver incrementato x, xdeve essere maggiore o uguale a 4. Nel caso di azioni deterministiche a per cui è garantita la terminazione, come x:=x+1, deve e dovrebbe hanno la stessa forza, cioè [a] e <a> hanno lo stesso significato. Di conseguenza la precedente proposizione è equivalente a x≥3 → <x:=x+1>x≥4, la quale asserisce che se x è maggiore o uguale a 3 allora dopo aver eseguito x:=x+1, x potrebbe essere maggiore o uguale a 4.
Assegnazione
La forma generale di una dichiarazione di assegnazione è x := e dove x è una variabile ed e è un'espressione costruita tramite costanti e variabili con qualsiasi operazione fornita dal linguaggio, come addizione e moltiplicazione. L'assioma di Hoare per l'assegnazione non è dato come un singolo assioma ma piuttosto come uno schema di assiomi.
A7. [x:=e]Φ(x) ≡ Φ(e)
Questo è uno schema nel senso che Φ(x) può essere istanziata con qualsiasi formulaΦ contenente zero o più istanze della variabile x. Il significato di Φ(e) è Φ con quelle ricorrenze di x che ricorrono liberamente in Φ, cioè non limitate da quantificatori come in ∀x, rimpiazzato da e. Per esempio si può instanziare A7 con [x:=e](x=y²) ≡ e=y², o con [x:=e](b=c+x) ≡ b=c+e. Tale schema assiomatico produce un numero infinito di assiomi di forma comune scritta come un'espressione finita che connoti tale forma.
L'istanza [x:=x+1]x≥4 ≡ x+1 ≥ 4 di A7 ci consente di calcolare meccanicamente che l'esempio [x:=x+1]x≥4 incontrato pochi paragrafi fa è equivalente a x+1 ≥ 4, , che a sua volta è equivalente a x≥3 tramite l'algebra elementare.
Un esempio che illustra l'assegnamento in combinazione con * è la proposizione <(x:=x+1)*>x=7. Qui si afferma che è possibile, incrementando x a sufficienza, fare sì che valga 7. Questo certamente non è sempre vero, per esempio se all'inizio x è 8, o 6,5, segue che questa proposizione non è un teorema di logica dinamica. Se x è comunque di tipo intero, allora questa proposizione è vera se e solo se all'inizio x è al massimo 7, cioè un altro modo per dire x≤7.
L'induzione matematica può essere ottenuta come l'istanza di A6 in cui la proposizione p è istanziata come Φ(n), l'azione a come n:=n+1, e n come 0. Le prime due di queste tre istanziazioni sono immediate, convertendo A6 in (Φ(n) ʌ [(n:=n+1)*] (Φ(n)→[n:=n+1]Φ(n))) → [(n:=n+1)*]Φ(n). Comunque l'apparentemente semplice sostituzione con 0 di n non è così semplice perché porta alla luce la cosiddetta opacità referenziale della logica modale nel caso in cui una modalità può interferire con una sostituzione.
Quando sostituiamo Φ(n) per p, noi stavamo pensando al simbolo proposizionale p come designatore rigido rispetto alla modalità [n:=n+1], il che significa che è la stessa proposizione dopo aver incrementato n come prima, anche se l'incrementare di n può aver impatto sulla verità. Similmente, l'azione a resta la stessa dopo aver incrementato n, anche se tale incremento significa che sarà eseguita in un ambiente differente. Invece n stesso non è un designatore rigido rispetto alla modalità [n:=n+1]; infatti, se prima dell'incremento denota 3, dopo denota 4. Quindi in A6 non possiamo sostituire 0 per n dovunque.
Un modo per gestire l'opacità delle modalità è quello di eliminare queste ultime. A questo fine, si espande [(n:=n+1)*]Φ(n) come una congiunzione infinita [(n:=n+1)0]Φ(n) ʌ [(n:=n+1)1]Φ(n) ʌ [(n:=n+1) 2]Φ(n) ʌ …, cioè la congiunzione su tutte le i di [(n:=n+1) i]Φ(n). Ora, applicando A4 si trasforma [(n:=n+1)i]Φ(n) in [n:=n+1][n:=n+1]…Φ(n) con i modalità. Quindi applicando l'assioma di Hoare i volte si produce Φ(n+i), poi si semplifica questa congiunzione infinita a ∀iΦ(n+i). Questa riduzione completa deve essere applicata a entrambe le istanze di [(n:=n+1)*] in A6, giungendo a (Φ(n) ʌ ∀i(Φ(n+i)→[n:=n+1]Φ(n+i))) → ∀iΦ(n+i). La modalità rimanente può essere ora eliminata con un ulteriore uso dell'assioma di Hoare per ottenere (Φ(n) ʌ ∀i(Φ(n+i)→Φ(n+i+1))) → ∀iΦ(n+i).
Senza modalità opache si può ora sostituire 0 a n nel modo usuale della logica del primo ordine per ottenere il celebre assioma di Giuseppe Peano (Φ(0) ʌ ∀i(Φ(i)→Φ(i+1))) → ∀iΦ(i), che prende il nome di Induzione matematica.