Lógica dinámica (lógica modal)

En lógica , filosofía e informática teórica , la lógica dinámica es una extensión de la lógica modal capaz de codificar propiedades de los programas informáticos .

Un ejemplo sencillo de una declaración en lógica dinámica es:

${\displaystyle {\text{El suelo está seco}}\to [{\text{Llueve}}]{\text{El suelo está mojado}},}$

lo cual establece que si el suelo está seco en ese momento y llueve, entonces después el suelo estará mojado.

La sintaxis de la lógica dinámica contiene un lenguaje de proposiciones (como "el suelo está seco") y un lenguaje de acciones (como "llueve"). Las construcciones modales centrales son:${\displaystyle [a]p}$, que establece que después de realizar la acción a, la proposición p debe cumplirse, y${\displaystyle \langle a\rangle p}$, que establece que después de realizar la acción a es posible que se cumpla p . El lenguaje de acciones admite operaciones${\displaystyle a\mathbin {;} b}$(realizar una acción seguida de otra),${\displaystyle a\cup b}$(realizando una acción u otra), e iteración${\displaystyle a{*}}$(realizar una acción cero o más veces). El lenguaje de proposiciones admite operaciones booleanas (y, o y no). La lógica de acción es lo suficientemente expresiva como para codificar programas. Para un programa arbitrario${\displaystyle P}$, condición previa${\displaystyle \varphi }$y postcondición${\displaystyle \varphi '}$, la declaración de lógica dinámica${\displaystyle \varphi \to [P]\varphi '}$codifica la corrección del programa, lo que hace que la lógica dinámica sea más general que la lógica de Hoare .

Más allá de su uso en la verificación formal de programas, la lógica dinámica se ha aplicado para describir comportamientos complejos que surgen en la lingüística , la filosofía , la inteligencia artificial y otros campos.

La lógica modal se caracteriza por los operadores modales.${\displaystyle \Box p}$(recuadro p) afirmando que${\displaystyle p\,\!}$es necesariamente el caso, y${\displaystyle \Diamond p}$(diamante p) afirmando que${\displaystyle p\,\!}$Es posible que sea así. La lógica dinámica extiende esto asociando a cada acción${\displaystyle a\,\!}$los operadores modales${\displaystyle [a]\,\!}$y${\displaystyle \langle a\rangle \,\!}$, convirtiéndola así en una lógica multimodal . El significado de${\displaystyle [a]p\,\!}$es que después de realizar la acción${\displaystyle a\,\!}$Es necesariamente cierto que${\displaystyle p\,\!}$sostiene, es decir,${\displaystyle a\,\!}$debe provocar${\displaystyle p\,\!}$. El significado de${\displaystyle \langle a\rangle p\,\!}$es que después de realizar${\displaystyle a\,\!}$es posible que${\displaystyle p\,\!}$sostiene, es decir,${\displaystyle a\,\!}$podría provocar${\displaystyle p\,\!}$Estos operadores son duales entre sí, lo que significa que están relacionados por${\displaystyle [a]p\leftrightarrow \neg \langle a\rangle \neg p\,\!}$y${\displaystyle \langle a\rangle p\leftrightarrow \neg [a]\neg p\,\!}$, de forma análoga a la relación entre lo universal (${\displaystyle \forall \,\!}$) y existencial (${\displaystyle \exists \,\!}$) cuantificadores.

La lógica dinámica permite acciones compuestas construidas a partir de acciones más pequeñas. Si bien los operadores de control básicos de cualquier lenguaje de programación podrían usarse para este propósito, los operadores de expresiones regulares de Kleene se adaptan bien a la lógica modal. Acciones dadas${\displaystyle a\,\!}$y${\displaystyle b\,\!}$, la acción compuesta${\displaystyle a\cup b\,\!}$, elección , también escrito${\displaystyle a+b\,\!}$o${\displaystyle a|b\,\!}$, se realiza realizando una de las${\displaystyle a\,\!}$o${\displaystyle b\,\!}$. La acción compuesta${\displaystyle a{\mathbin {;}}b\,\!}$, secuencia , se realiza realizando primero${\displaystyle a\,\!}$y luego${\displaystyle b\,\!}$. La acción compuesta${\displaystyle a{*}\,\!}$, iteración , se realiza mediante la ejecución${\displaystyle a\,\!}$cero o más veces, secuencialmente. La acción constante${\displaystyle 0\,\!}$o BLOQUEAR no hace nada y no termina, mientras que la acción constante${\displaystyle 1\,\!}$o SKIP o NOP , definible como${\displaystyle 0{*}\,\!}$, no hace nada más que terminar.

Estos operadores pueden axiomatizarse en lógica dinámica de la siguiente manera, tomando como ya dada una axiomatización adecuada de la lógica modal que incluye tales axiomas para operadores modales como el axioma mencionado anteriormente.${\displaystyle [a]p\leftrightarrow \neg \langle a\rangle \neg p\,\!}$y las dos reglas de inferencia modus ponens (${\displaystyle \vdash p}$y${\displaystyle \vdash p\to q}$implica${\displaystyle \vdash q\,}$) y necesidad (${\displaystyle \vdash p}$implica${\displaystyle \vdash [a]p\,}$).

A1. ${\displaystyle [0]p\,\!}$

A2. ${\displaystyle [1]p\leftrightarrow p\,\!}$

A3. ${\displaystyle [a\cup b]p\leftrightarrow [a]p\land [b]p\,\!}$

A4. ${\displaystyle [a\mathbin {;} b]p\leftrightarrow [a][b]p\,\!}$

A5. ${\displaystyle [a*]p\leftrightarrow p\land [a][a*]p\,\!}$

A6. ${\displaystyle p\land [a*](p\to [a]p)\to [a*]p\,\!}$

El axioma A1 hace la promesa vacía de que cuando BLOCK termina,${\displaystyle p\,\!}$se mantendrá, incluso si${\displaystyle p\,\!}$¿Es falsa la proposición ? (Por lo tanto, BLOCK abstrae la esencia de la acción de congelar el infierno). A2 dice que NOP actúa como la función identidad en las proposiciones, es decir, transforma${\displaystyle p\,\!}$en sí mismo. A3 dice que si se hace uno de${\displaystyle a\,\!}$o${\displaystyle b\,\!}$debe provocar${\displaystyle p\,\!}$, entonces${\displaystyle a\,\!}$debe provocar${\displaystyle p\,\!}$y asimismo para${\displaystyle b\,\!}$y viceversa. A4 dice que si se hace${\displaystyle a\,\!}$y luego${\displaystyle b\,\!}$debe provocar${\displaystyle p\,\!}$, entonces${\displaystyle a\,\!}$debe generar una situación en la que${\displaystyle b\,\!}$debe provocar${\displaystyle p\,\!}$. A5 es el resultado evidente de aplicar A2, A3 y A4 a la ecuación${\displaystyle a{*}=1\cup a{\mathbin {;}}a{*}\,\!}$del álgebra de Kleene . A6 afirma que si${\displaystyle p\,\!}$se mantiene ahora, y no importa con qué frecuencia lo hagamos${\displaystyle a\,\!}$Sigue siendo cierto que la verdad de${\displaystyle p\,\!}$después de esa actuación implica su verdad después de una actuación más de${\displaystyle a\,\!}$, entonces${\displaystyle p\,\!}$debe seguir siendo cierto sin importar con qué frecuencia lo hagamos${\displaystyle a\,\!}$. A6 es reconocible como inducción matemática con la acción n  := n+1 de incrementar n generalizada a acciones arbitrarias.${\displaystyle a\,\!}$.

El axioma de la lógica modal${\displaystyle [a]p\leftrightarrow \neg \langle a\rangle \neg p\,\!}$permite derivar los siguientes seis teoremas correspondientes a lo anterior:

T1. ${\displaystyle \neg \langle 0\rangle p\,\!}$

T2. ${\displaystyle \langle 1\rangle p\leftrightarrow p\,\!}$

T3. ${\displaystyle \langle a\cup b\rangle p\leftrightarrow \langle a\rangle p\lor \langle b\rangle p\,\!}$

T4. ${\displaystyle \langle a\mathbin {;} b\rangle p\leftrightarrow \langle a\rangle \langle b\rangle p\,\!}$

T5. ${\displaystyle \langle a*\rangle p\leftrightarrow p\lor \langle a\rangle \langle a*\rangle p\,\!}$

T6. ${\displaystyle \langle a*\rangle p\to p\lor \langle a*\rangle (\neg p\land \langle a\rangle p)\,\!}$

T1 afirma la imposibilidad de lograr algo realizando BLOQUEO . T2 señala nuevamente que NOP no cambia nada, teniendo en cuenta que NOP es determinista y terminante, por lo que${\displaystyle [1]\,\!}$y${\displaystyle \langle 1\rangle \,\!}$tienen la misma fuerza. T3 dice que si la elección de${\displaystyle a\,\!}$o${\displaystyle b\,\!}$podría provocar${\displaystyle p\,\!}$, entonces o${\displaystyle a\,\!}$o${\displaystyle b\,\!}$por sí solo podría provocar${\displaystyle p\,\!}$. T4 es igual que A4. T5 se explica igual que para A5. T6 afirma que si es posible provocar${\displaystyle p\,\!}$realizando${\displaystyle a\,\!}$con la suficiente frecuencia, entonces${\displaystyle p\,\!}$es cierto ahora o es posible realizar${\displaystyle a\,\!}$repetidamente para provocar una situación en la que${\displaystyle p\,\!}$es (todavía) falso pero una actuación más de${\displaystyle a\,\!}$podría provocar${\displaystyle p\,\!}$.

La caja y el diamante son completamente simétricos con respecto a cuál se toma como primitivo. Una axiomatización alternativa habría sido tomar los teoremas T1–T6 como axiomas, a partir de los cuales podríamos haber derivado los teoremas A1–A6.

La diferencia entre implicación e inferencia es la misma en la lógica dinámica que en cualquier otra lógica: mientras que la implicación${\displaystyle p\to q\,\!}$afirma que si${\displaystyle p\,\!}$Si es cierto, entonces también lo es.${\displaystyle q\,\!}$, la inferencia${\displaystyle p\vdash q\,\!}$afirma que si${\displaystyle p\,\!}$es válido entonces también lo es${\displaystyle q\,\!}$Sin embargo, la naturaleza dinámica de la lógica dinámica traslada esta distinción del ámbito de la axiomática abstracta a la experiencia del sentido común en situaciones cambiantes. La regla de inferencia${\displaystyle p\vdash [a]p\,\!}$, por ejemplo, es sólida porque su premisa afirma que${\displaystyle p\,\!}$se mantiene en todo momento, de dondequiera que sea${\displaystyle a\,\!}$podría llevarnos,${\displaystyle p\,\!}$será cierto allí. La implicación${\displaystyle p\to [a]p\,\!}$no es válido, sin embargo, porque la verdad de${\displaystyle p\,\!}$en el momento actual no hay garantía de su veracidad después de realizar${\displaystyle a\,\!}$. Por ejemplo,${\displaystyle p\to [a]p\,\!}$será cierto en cualquier situación donde${\displaystyle p\,\!}$es falso, o en cualquier situación donde${\displaystyle [a]p\,\!}$es cierto, pero la afirmación${\displaystyle (x=1)\to [x:=x+1](x=1)\,\!}$es falso en cualquier situación donde${\displaystyle x\,\!}$tiene valor 1 y, por lo tanto, no es válido.

En cuanto a la lógica modal, las reglas de inferencia modus ponens y necessitation bastan también para la lógica dinámica como las únicas reglas primitivas que necesita, como se indicó anteriormente. Sin embargo, como es habitual en lógica, se pueden derivar muchas más reglas a partir de estas con la ayuda de los axiomas. Un ejemplo de una regla derivada de este tipo en lógica dinámica es que si patear un televisor roto una sola vez no puede arreglarlo, entonces patearlo repetidamente tampoco puede arreglarlo.${\displaystyle k\,\!}$por la acción de patear el televisor y${\displaystyle b\,\!}$Para la proposición de que el televisor está roto, la lógica dinámica expresa esta inferencia como${\displaystyle b\to [k]b\vdash b\to [k*]b\,\!}$, teniendo como premisa${\displaystyle b\to [k]b\,\!}$y como conclusión${\displaystyle b\to [k*]b\,\!}$. El significado de${\displaystyle [k]b\,\!}$es que está garantizado que después de patear el televisor, se romperá. De ahí la premisa${\displaystyle b\to [k]b\,\!}$Esto significa que si el televisor está roto, después de darle una patada seguirá roto.${\displaystyle k{*}\,\!}$denota la acción de patear el televisor cero o más veces. Por lo tanto, la conclusión${\displaystyle b\to [k*]b\,\!}$Esto significa que si el televisor está roto, después de patearlo cero o más veces seguirá roto. Porque si no, después de la penúltima patada el televisor estaría en un estado en el que patearlo una vez más lo arreglaría, lo cual, según la premisa, nunca puede ocurrir bajo ninguna circunstancia.

La inferencia${\displaystyle b\to [k]b\vdash b\to [k*]b\,\!}$es sólido. Sin embargo, la implicación${\displaystyle (b\to [k]b)\to (b\to [k*]b)\,\!}$no es válido porque podemos encontrar fácilmente situaciones en las que${\displaystyle b\to [k]b\,\!}$se sostiene pero${\displaystyle b\to [k*]b\,\!}$No lo hace. En cualquier situación de contraejemplo de este tipo,${\displaystyle b\,\!}$debe sostener pero${\displaystyle [k*]b\,\!}$debe ser falso, mientras que${\displaystyle [k]b\,\!}$Sin embargo, debe ser cierto. Pero esto podría ocurrir en cualquier situación en la que el televisor esté roto pero pueda revivir con dos patadas. La implicación falla (no es válida) porque solo requiere que${\displaystyle b\to [k]b\,\!}$ahora se sostiene, mientras que la inferencia tiene éxito (es sólida) porque requiere que${\displaystyle b\to [k]b\,\!}$mantenerlo en todas las situaciones, no solo en la presente.

Un ejemplo de implicación válida es la proposición${\displaystyle (x\geq 3)\to [x:=x+1](x\geq 4)\,\!}$. Esto dice que si${\displaystyle x\,\!}$es mayor o igual a 3, entonces después de incrementar${\displaystyle x\,\!}$,${\displaystyle x\,\!}$debe ser mayor o igual a 4. En el caso de acciones deterministas${\displaystyle a\,\!}$que tienen garantizada su finalización, como por ejemplo:${\displaystyle x:=x+1\,\!}$, deben y podrían tener la misma fuerza, es decir,${\displaystyle [a]\,\!}$y${\displaystyle \langle a\rangle \,\!}$tienen el mismo significado. Por lo tanto, la proposición anterior es equivalente a${\displaystyle (x\geq 3)\to \langle x:=x+1\rangle (x\geq 4)\,\!}$afirmando que si${\displaystyle x\,\!}$es mayor o igual a 3 entonces después de realizar${\displaystyle x:=x+1\,\!}$,${\displaystyle x\,\!}$podría ser mayor o igual a 4.

La forma general de una declaración de asignación es${\displaystyle x:=e\,\!}$dónde${\displaystyle x\,\!}$es una variable y${\displaystyle e\,\!}$es una expresión construida a partir de constantes y variables con las operaciones que proporciona el lenguaje, como la suma y la multiplicación. El axioma de Hoare para la asignación no se presenta como un axioma único, sino como un esquema de axiomas .

A7.${\displaystyle [x:=e]\Phi (x)\leftrightarrow \Phi (e)\,\!}$

Este es un esquema en el sentido de que${\displaystyle \Phi (x)\,\!}$puede instanciarse con cualquier fórmula${\displaystyle \Phi \,\!}$que contiene cero o más instancias de una variable${\displaystyle x\,\!}$. El significado de${\displaystyle \Phi (e)\,\!}$es${\displaystyle \Phi \,\!}$con esos sucesos de${\displaystyle x\,\!}$que ocurren libremente en${\displaystyle \Phi \,\!}$, es decir, no limitado por algún cuantificador como en${\displaystyle \forall x\,\!}$, reemplazado por${\displaystyle e\,\!}$. Por ejemplo, podemos instanciar A7 con${\displaystyle [x:=e](x=y^{2})\leftrightarrow e=y^{2}\,\!}$o con${\displaystyle [x:=e](b=c+x)\leftrightarrow b=c+e\,\!}$Dicho esquema axiomático permite escribir un número infinito de axiomas que tienen una forma común como una expresión finita que denota esa forma.

La instancia${\displaystyle [x:=x+1](x\geq 4)\leftrightarrow x+1\geq 4\,\!}$de A7 nos permite calcular mecánicamente que el ejemplo${\displaystyle [x:=x+1]x\geq 4\,\!}$encontrado hace unos párrafos es equivalente a${\displaystyle x+1\geq 4\,\!}$, lo cual a su vez es equivalente a${\displaystyle x\geq 3\,\!}$por álgebra elemental .

Un ejemplo que ilustra la asignación en combinación con${\displaystyle *\,\!}$es la proposición${\displaystyle \langle (x:=x+1)*\rangle x=7\,\!}$. Esto afirma que es posible, mediante incrementos${\displaystyle x\,\!}$con la suficiente frecuencia como para hacer${\displaystyle x\,\!}$igual a 7. Esto, por supuesto, no siempre es cierto, por ejemplo, si${\displaystyle x\,\!}$es 8 para empezar, o 6.5, por lo que esta proposición no es un teorema de lógica dinámica. Si${\displaystyle x\,\!}$es de tipo entero, sin embargo, entonces esta proposición es verdadera si y solo si${\displaystyle x\,\!}$es como máximo 7 para empezar, es decir, es solo una forma indirecta de decir${\displaystyle x\leq 7\,\!}$.

La inducción matemática se puede obtener como instancia de A6 en la que la proposición${\displaystyle p\,\!}$se instancia como${\displaystyle \Phi (n)\,\!}$, la acción${\displaystyle a\,\!}$como${\displaystyle n:=n+1\,\!}$, y${\displaystyle n\,\!}$como${\displaystyle 0\,\!}$. Las dos primeras de estas tres instancias son sencillas, convirtiendo A6 en${\displaystyle (\Phi (n)\land [(n:=n+1)*](\Phi (n)\to [n:=n+1]\Phi (n)))\to [(n:=n+1)*]\Phi (n)\,\!}$Sin embargo, la sustitución aparentemente simple de${\displaystyle 0\,\!}$para${\displaystyle n\,\!}$no es tan simple, ya que pone de manifiesto la llamada opacidad referencial de la lógica modal en el caso en que una modalidad puede interferir con una sustitución.

Cuando sustituimos${\displaystyle \Phi (n)\,\!}$para${\displaystyle p\,\!}$Estábamos pensando en el símbolo de proposición${\displaystyle p\,\!}$como un designador rígido con respecto a la modalidad${\displaystyle [n:=n+1]\,\!}$, lo que significa que es la misma proposición después de incrementar${\displaystyle n\,\!}$como antes, aunque incrementando${\displaystyle n\,\!}$puede afectar su veracidad. Asimismo, la acción${\displaystyle a\,\!}$sigue siendo la misma acción después del incremento${\displaystyle n\,\!}$, aunque incrementando${\displaystyle n\,\!}$dará como resultado su ejecución en un entorno diferente. Sin embargo,${\displaystyle n\,\!}$en sí mismo no es un designador rígido con respecto a la modalidad.${\displaystyle [n:=n+1]\,\!}$; si denota 3 antes de incrementar${\displaystyle n\,\!}$, denota 4 después. Así que no podemos simplemente sustituir${\displaystyle 0\,\!}$para${\displaystyle n\,\!}$en todas partes en A6.

Una forma de lidiar con la opacidad de las modalidades es eliminarlas. Para ello, expanda${\displaystyle [(n:=n+1)*]\Phi (n)\,\!}$como la conjunción infinita${\displaystyle [(n:=n+1)^{0}]\Phi (n)\land [(n:=n+1)^{1}]\Phi (n)\land [(n:=n+1)^{2}]\Phi (n)\land \ldots \,\!}$, es decir, la conjunción sobre todos${\displaystyle i\,\!}$de${\displaystyle [(n:=n+1)^{i}]\Phi (n)\,\!}$. Ahora aplique A4 para convertir${\displaystyle [(n:=n+1)^{i}]\Phi (n)\,\!}$en${\displaystyle [n:=n+1][n:=n+1]\ldots \Phi (n)\,\!}$, teniendo${\displaystyle i\,\!}$modalidades. Luego aplique el axioma de Hoare.${\displaystyle i\,\!}$tiempos para esto para producir${\displaystyle \Phi (n+i)\,\!}$, luego simplifica esta conjunción infinita a${\displaystyle \forall i\Phi (n+i)\,\!}$. Toda esta reducción debe aplicarse a ambas instancias de${\displaystyle [(n:=n+1)*]\,\!}$en A6, cediendo${\displaystyle (\Phi (n)\land \forall i(\Phi (n+i)\to [n:=n+1]\Phi (n+i)))\to \forall i\Phi (n+i)\,\!}$. La modalidad restante ahora puede eliminarse con un uso más del axioma de Hoare para dar${\displaystyle (\Phi (n)\land \forall i(\Phi (n+i)\to \Phi (n+i+1)))\to \forall i\Phi (n+i)\,\!}$.

Ahora que las modalidades opacas están fuera del camino, podemos sustituir con seguridad${\displaystyle 0\,\!}$para${\displaystyle n\,\!}$de la manera habitual de la lógica de primer orden para obtener el célebre axioma de Peano.${\displaystyle (\Phi (0)\land \forall i(\Phi (i)\to \Phi (i+1)))\to \forall i\Phi (i)\,\!}$, es decir, la inducción matemática.

Una sutileza que pasamos por alto aquí es que${\displaystyle \forall i\,\!}$debe entenderse como abarcando los números naturales, donde${\displaystyle i\,\!}$es el superíndice en la expansión de${\displaystyle a{*}\,\!}$como la unión de${\displaystyle a^{i}\,\!}$sobre todos los números naturales${\displaystyle i\,\!}$La importancia de mantener esta información de escritura en orden se hace evidente si${\displaystyle n\,\!}$habían sido de tipo entero , o incluso real , para cualquiera de los cuales A6 es perfectamente válido como axioma. Como ejemplo, si${\displaystyle n\,\!}$es una variable real y${\displaystyle \Phi (n)\,\!}$es el predicado${\displaystyle n\,\!}$es un número natural , entonces el axioma A6 después de las dos primeras sustituciones, es decir,${\displaystyle (\Phi (n)\land \forall i(\Phi (n+i)\to \Phi (n+i+1)))\to \forall i\Phi (n+i)\,\!}$, es igualmente válido, es decir, verdadero en cada estado independientemente del valor de${\displaystyle n\,\!}$en ese estado, como cuando${\displaystyle n\,\!}$es de tipo número natural . Si en un estado dado${\displaystyle n\,\!}$es un número natural , entonces se cumple el antecedente de la implicación principal de A6, pero entonces${\displaystyle n+i\,\!}$también es un número natural, por lo que el consecuente también se cumple. Si${\displaystyle n\,\!}$no es un número natural, entonces el antecedente es falso y por lo tanto A6 sigue siendo verdadero independientemente de la verdad del consecuente. Podríamos fortalecer A6 a una equivalencia${\displaystyle p\land [a*](p\to [a]p)\leftrightarrow [a*]p\,\!}$sin afectar nada de esto, siendo la otra dirección demostrable a partir de A5, de donde vemos que si el antecedente de A6 resulta ser falso en algún lugar, entonces el consecuente debe ser falso.

La lógica dinámica se asocia a cada proposición.${\displaystyle p\,\!}$una acción${\displaystyle p?\,\!}$llamada prueba. Cuando${\displaystyle p\,\!}$Se mantiene la prueba${\displaystyle p?\,\!}$actúa como una NOP , sin cambiar nada mientras permite que la acción continúe. Cuando${\displaystyle p\,\!}$es falso,${\displaystyle p?\,\!}$actúa como BLOQUE . Las pruebas se pueden axiomatizar de la siguiente manera.

A8.${\displaystyle [p?]q\leftrightarrow (p\to q)\,\!}$

El teorema correspondiente para${\displaystyle \langle p?\rangle \,\!}$es:

T8.${\displaystyle \langle p?\rangle q\leftrightarrow p\land q\,\!}$

La construcción si p entonces a sino b se realiza en lógica dinámica como${\displaystyle (p?\mathbin {;} a)\cup (\neg p?\mathbin {;} b)\,\!}$Esta acción expresa una elección cautelosa: si${\displaystyle p\,\!}$entonces sostiene${\displaystyle p?\mathbin {;} a\,\!}$es equivalente a${\displaystyle a\,\!}$, mientras${\displaystyle \neg p?\mathbin {;} b\,\!}$es equivalente a BLOQUE, y${\displaystyle a\cup 0\,\!}$es equivalente a${\displaystyle a\,\!}$. Por lo tanto, cuando${\displaystyle p\,\!}$es cierto que el que realiza la acción solo puede tomar la rama izquierda, y cuando${\displaystyle p\,\!}$es falso lo correcto.

La construcción mientras p hace a se realiza como${\displaystyle ({p?\mathbin {;} a)*}\mathbin {;} \neg p?\,\!}$Esto realiza${\displaystyle p?\mathbin {;} a\,\!}$cero o más veces y luego realiza${\displaystyle \neg p?\,\!}$. Mientras${\displaystyle p\,\!}$sigue siendo cierto, el${\displaystyle \neg p?\,\!}$al final impide que el intérprete termine la iteración prematuramente, pero tan pronto como se vuelve falso, se producen nuevas iteraciones del cuerpo.${\displaystyle p\,\!}$están bloqueados y el intérprete no tiene más remedio que salir a través de la prueba.${\displaystyle \neg p?\,\!}$.

La declaración de asignación aleatoria${\displaystyle x\mathbin {:=} {?}\,\!}$denota la acción no determinista de establecer${\displaystyle x\,\!}$a un valor arbitrario.${\displaystyle [x\mathbin {:=} {?}]p\,\!}$entonces dice que${\displaystyle p\,\!}$Se mantiene sin importar lo que configures${\displaystyle x\,\!}$a, mientras${\displaystyle \langle x\mathbin {:=} {?}\rangle p\,\!}$dice que es posible establecer${\displaystyle x\,\!}$a un valor que hace${\displaystyle p\,\!}$verdadero.${\displaystyle [x\mathbin {:=} {?}]\,\!}$por lo tanto tiene el mismo significado que el cuantificador universal${\displaystyle \forall x\,\!}$, mientras${\displaystyle \langle x\mathbin {:=} {?}\rangle \,\!}$de manera similar corresponde al cuantificador existencial${\displaystyle \exists x\,\!}$. Es decir, la lógica de primer orden puede entenderse como la lógica dinámica de programas de la forma${\displaystyle x:=?\,\!}$.

Dijkstra afirmó demostrar la imposibilidad de un programa que establezca el valor de una variable.${\displaystyle x}$a un entero positivo arbitrario. ^{[ 1 ]} Sin embargo, en lógica dinámica con asignación y el operador *,${\displaystyle x}$se puede establecer en un entero positivo arbitrario con el programa de lógica dinámica${\displaystyle (x\mathbin {:=} 0)\mathbin {;} (x:=x+1){*}}$Por lo tanto, debemos rechazar el argumento de Dijkstra o sostener que el operador * no es efectivo.

La lógica modal se interpreta comúnmente en términos de semántica de mundos posibles o estructuras de Kripke. Esta semántica se traslada naturalmente a la lógica dinámica al interpretar los mundos como estados de una computadora en la aplicación a la verificación de programas, o estados de nuestro entorno en aplicaciones a la lingüística, la IA, etc. Una función de la semántica de mundos posibles es formalizar las nociones intuitivas de verdad y validez, lo que a su vez permite definir las nociones de solidez y completitud para los sistemas axiomáticos. Una regla de inferencia es sólida cuando la validez de sus premisas implica la validez de su conclusión. Un sistema axiomático es sólido cuando todos sus axiomas son válidos y sus reglas de inferencia son sólidas. Un sistema axiomático es completo cuando toda fórmula válida puede derivarse como un teorema de dicho sistema. Estos conceptos se aplican a todos los sistemas lógicos, incluida la lógica dinámica.

La lógica ordinaria o de primer orden tiene dos tipos de términos, respectivamente, afirmaciones y datos. Como se puede ver en los ejemplos anteriores, la lógica dinámica agrega un tercer tipo de término que denota acciones. La afirmación de la lógica dinámica${\displaystyle [x:=x+1](x\geq 4)\,\!}$contiene los tres tipos:${\displaystyle x\,\!}$,${\displaystyle x+1\,\!}$, y${\displaystyle 4\,\!}$son datos,${\displaystyle x:=x+1\,\!}$es una acción, y${\displaystyle x\geq 4\,\!}$y${\displaystyle [x:=x+1](x\geq 4)\,\!}$son afirmaciones. La lógica proposicional se deriva de la lógica de primer orden omitiendo términos de datos y razonando solo sobre proposiciones abstractas, que pueden ser variables proposicionales simples o átomos o proposiciones compuestas construidas con conectores lógicos como y , o , y no .

La lógica dinámica proposicional, o PDL, fue derivada de la lógica dinámica en 1977 por Michael J. Fischer y Richard Ladner . La PDL combina las ideas de la lógica proposicional y la lógica dinámica al agregar acciones y omitir datos; por lo tanto, los términos de la PDL son acciones y proposiciones. El ejemplo de TV anterior se expresa en PDL, mientras que el siguiente ejemplo involucra${\displaystyle x:=x+1\,\!}$está en lógica dinámica de primer orden. PDL es a la lógica dinámica (de primer orden) como la lógica proposicional es a la lógica de primer orden.

Fischer y Ladner demostraron en su artículo de 1977 que la satisfacibilidad de PDL tenía una complejidad computacional de tiempo exponencial no determinista como máximo y de tiempo exponencial determinista como mínimo en el peor de los casos. Esta brecha se cerró en 1978 gracias a Vaughan Pratt, quien demostró que PDL era decidible en tiempo exponencial determinista. En 1977, Krister Segerberg propuso una axiomatización completa de PDL, concretamente cualquier axiomatización completa de la lógica modal K junto con los axiomas A1-A6 mencionados anteriormente. Gabbay (nota inédita), Parikh (1978), Pratt (1979) y Kozen y Parikh (1981) hallaron pruebas de completitud para los axiomas de Segerberg.

La lógica dinámica fue desarrollada por Vaughan Pratt en 1974 en apuntes para una clase sobre verificación de programas como un enfoque para asignar significado a la lógica de Hoare mediante la expresión de la fórmula de Hoare.${\displaystyle p\{a\}q\,\!}$como${\displaystyle p\to [a]q\,\!}$El enfoque se publicó posteriormente en 1976 como un sistema lógico independiente. El sistema es paralelo al sistema de lógica algorítmica de Andrzej Salwicki ^{[ 2 ]} y a la noción de transformador de predicados de precondición más débil de Edsger Dijkstra.${\displaystyle \operatorname {wp} (a,p)\,\!}$, con${\displaystyle [a]p\,\!}$correspondiente a la de Dijkstra${\displaystyle \operatorname {wlp} (a,p)\,\!}$, la condición previa liberal más débil. Sin embargo, esas lógicas no establecían ninguna conexión con la lógica modal, la semántica de Kripke , las expresiones regulares ni el cálculo de relaciones binarias. Por lo tanto, la lógica dinámica puede considerarse un refinamiento de la lógica algorítmica y los transformadores de predicados que los conecta con la axiomática y la semántica de Kripke de la lógica modal, así como con los cálculos de relaciones binarias y expresiones regulares.

La lógica de Hoare, la lógica algorítmica, las precondiciones más débiles y la lógica dinámica son muy adecuadas para el discurso y el razonamiento sobre el comportamiento secuencial. Sin embargo, extender estas lógicas al comportamiento concurrente ha resultado problemático. Existen varios enfoques, pero todos carecen de la elegancia del caso secuencial. En contraste, el sistema de lógica temporal de Amir Pnueli de 1977 , otra variante de la lógica modal que comparte muchas características con la lógica dinámica, se diferencia de todas las lógicas mencionadas anteriormente por ser lo que Pnueli caracterizó como una lógica "endógena", mientras que las demás son lógicas "exógenas". Con esto, Pnueli quería decir que las afirmaciones de la lógica temporal se interpretan dentro de un marco de comportamiento universal en el que una única situación global cambia con el paso del tiempo, mientras que las afirmaciones de las otras lógicas se hacen externamente a las múltiples acciones de las que hablan. La ventaja del enfoque endógeno es que no hace suposiciones fundamentales sobre qué causa qué a medida que el entorno cambia con el tiempo. En cambio, una fórmula de lógica temporal puede describir dos partes no relacionadas de un sistema que, precisamente por no estar relacionadas, evolucionan tácitamente en paralelo. En efecto, la conjunción lógica ordinaria de aserciones temporales es el operador de composición concurrente de la lógica temporal. La simplicidad de este enfoque de la concurrencia ha hecho que la lógica temporal sea la lógica modal de elección para razonar sobre sistemas concurrentes, con sus aspectos de sincronización, interferencia, independencia, interbloqueo , bloqueo mutuo , equidad, etc.

• David Harel , Dexter Kozen y Jerzy Tiuryn, "Lógica dinámica". MIT Press, 2000 (450 págs.).

• Nicolas Troquard y Philippe Balbiani, "Lógica dinámica proposicional". Enciclopedia de filosofía de Stanford , 2007.

• Vaughan Pratt , "Consideraciones semánticas sobre la lógica de Floyd-Hoare", Actas del 17º Simposio Anual del IEEE sobre Fundamentos de la Informática , 1976, 109-121.
• David Harel , «Lógica dinámica», en D. Gabbay y F. Guenthner (eds.), Manual de lógica filosófica, volumen II: Extensiones de la lógica clásica, capítulo 10, páginas 497-604. Reidel, Dordrecht, 1984.
• David Harel , Dexter Kozen y Jerzy Tiuryn, «Lógica dinámica», en D. Gabbay y F. Guenthner (eds.), Manual de lógica filosófica, volumen 4: páginas 99-217. Kluwer, 2.ª edición, 2002.

• Consideraciones semánticas sobre la lógica de Floyd-Hoare (artículo original sobre lógica dinámica)
• Capítulo 6  : Lógica y acción en el sitio web Logic In Action.
• Apuntes de clase sobre lógica dinámica de André Platzer