Lógica modal Lógicas multimodales Cálculo µ

Lógica modal Lógicas multimodales Cálculo µ Sintaxis Semántica S. axiomáticos

Lógica modal LÓGICA COMPUTACIONAL LÓGICA MODAL

La lógica modal originalmente intentaba capturar el significado de los operadores “es necesario que. . . ” y “es posible que . . . ” Estos operadores no se pueden definir por medio de funciones booleanas.

Francisco Hernández Quiroz

Otros conceptos también se pueden expresar como operadores modales: temporalidad, acciones, conocimiento, etc.

Departamento de Matemáticas Facultad de Ciencias, UNAM E-mail: [email protected] Página Web: www.matematicas.unam.mx/fhq

La semántica de estos conceptos es similar a la semántica de necesidad y posibilidad. Esto ha permitido aplicar la lógica modal en ámbitos distintos a la filosofía: matemáticas, computación, teoría de juegos, etc.

Facultad de Ciencias

Francisco Hernández Quiroz

Lógica Computacional

Lógica modal

1 / 32

Francisco Hernández Quiroz

Lógica modal Lógicas multimodales Cálculo µ

Lógica modal Lógicas multimodales Cálculo µ

Sintaxis Semántica S. axiomáticos

Sintaxis Semántica S. axiomáticos

Sintaxis de la lógica modal proposicional

F = hW, Ri,

Los últimos dos operadores modales no existen en el cálculo de proposiciones

donde W = {w, w 0 , . . . }

“posiblemente α” “necesariamente α”

es un conjunto de mundos posibles y

Alternativamente, el operador 2 se puede definir en términos de 3 (y viceversa): 2α ≡def ¬3¬α.

Francisco Hernández Quiroz

Lógica Computacional

2 / 32

La semántica de la lógica modal no se puede definir con funciones booleanas. En su lugar se emplean marcos

α ::= pi | qi | ri | ¬α | (α∨α) | (α∧α) | (α ⇒ α) | (α ⇔ α) | 3α | 2α

se leerá se leerá

Lógica modal

Mundos posibles

La sintaxis de la lógica modal proposicional es:

3α 2α

Lógica Computacional

Lógica modal

R⊆W×W es una relación de accesibilidad entre mundos.

3 / 32

Francisco Hernández Quiroz

Lógica Computacional

Lógica modal

4 / 32

Lógica modal Lógicas multimodales Cálculo µ

Lógica modal Lógicas multimodales Cálculo µ

Sintaxis Semántica S. axiomáticos

Sintaxis Semántica S. axiomáticos

Satisfacción y verdad

El caso de los operadores modales

Las proposiciones atómicas no reciben un valor de verdad único, sino uno por cada mundo posible. Sea F = hW, Ri un marco y sea P0 el conjunto de proposiciones atómicas. Una función de evaluación es del tipo

El caso de los operadores modales es obviamente distinto:

e : P0 × W → {V , F }.

Con estas definiciones, la satisfacción se puede generalizar:

F, e, w |= 2α sii ∀v ∈ W . si R(w, v) entonces F, e, v |= α F, e, w |= 3α sii ∃v ∈ W . R(w, v) y F, e, v |= α

F, e |= α

La relación de satisfacción |= es relativa a F, a una evaluación e y a un mundo específico w ∈ W: F, e, w F, e, w F, e, w F, e, w F, e, w F, e, w

|= p |= ¬α |= α ∨ ψ |= α ∧ ψ |= α ⇒ ψ |= α ⇔ ψ

Francisco Hernández Quiroz

sii sii sii sii sii sii

En este caso, diremos que α es verdadera en e. Finalmente, definiremos validez respecto a un marco F:

e(p, w) = V ∀p ∈ P0 F, e, w 6|= α F, e, w |= α o bien F, e, w |= ψ F, e, w |= α y F, e, w |= ψ si F, e, w |= α implica que F, e, w |= ψ F, e, w |= α sii F, e, w |= ψ Lógica Computacional

Lógica modal

F |= α

sii

∀e . F, e |= α,

|= α

sii

∀F . F |= α.

y validez en general

5 / 32

Francisco Hernández Quiroz

Lógica Computacional

Lógica modal Lógicas multimodales Cálculo µ

Lógica modal Lógicas multimodales Cálculo µ

Sintaxis Semántica S. axiomáticos

Sintaxis Semántica S. axiomáticos

Ejemplos

Lógica modal

6 / 32

Un solo marco, dos evaluaciones u

En las siguienes láminas se presentarán los marcos como gráficas dirigidas.

u p

Los vértices corresponden a los mundos posibles u, v y w y las aristas, a la relación de accesibilidad entre mundos.

v

7 / 32

r w

F, e, u |= 3p F, e, u 6|= 2p F, e |= 3(p ∨ q ∨ r)

En la tercera lámina se presenta un caso aparentemente paradójico de un marco con una relación de accesibilidad vacía.

Lógica modal

v q

r w

En todos los casos se presenta dos veces el mismo marco, pero con evaluaciones distintas en cada gráfica.

Lógica Computacional

q

q

Las fórmulas atómicas verdaderas en un mundo se escribirán dentro del círculo correspondiente. Las fórmulas que no aparecen en el círculo son falsas.

Francisco Hernández Quiroz

∀w ∈ W . F, e, w |= α.

sii

Francisco Hernández Quiroz

F, e, u 6|= 3p F, e, w |= 2q F, e 6|= 3(p ∨ r) (falla en w) Lógica Computacional

Lógica modal

8 / 32

Lógica modal Lógicas multimodales Cálculo µ

Lógica modal Lógicas multimodales Cálculo µ

Sintaxis Semántica S. axiomáticos

Sintaxis Semántica S. axiomáticos

Un solo marco, dos evaluaciones y fórmulas válidas u

Un caso en apariencia paradójico

u

u

p

u p

v

v

v

p p w

p

w F, e, u |= 3p F, e, u |= 2p F, e |= 2p ⇒ 3p

w

w

F, e, u |= 3¬p F, e, u |= 2¬p F, e |= 2¬p ⇒ 3¬p

F, e |6 = 3p F, e |= 2p

Lógica Computacional

Lógica modal

9 / 32

Francisco Hernández Quiroz

Lógica modal Lógicas multimodales Cálculo µ

Lógica modal Lógicas multimodales Cálculo µ

Sintaxis Semántica S. axiomáticos

Sintaxis Semántica S. axiomáticos

Propiedades de la relación de accesibilidad

P1 P2 P3 P4 P5 P6

∀u . ∃v . u → v ∀u . u → u ∀u, v . u → v ⇒ v → u ∀u, v, w . u → v ∧ v → w ⇒ u → w ∀u, v, w . u → v ∧ u → w ⇒ v → w ∀u, v, w . u → v ∧ u → w ⇒ v = w

P7 P8 P9 P10

∀u . ∃!v . u → v ∀u, v . u → v ⇒ (∃w . u → w ∧ w → v) ∀u, v, w . u → v ∧ u → w ⇒ v → w ∨ w → v ∨ v = w ∀u, v, w . u → v ∧ u → w ⇒ (∃z . v → z ∧ w → z) Lógica Computacional

Lógica Computacional

Lógica modal

10 / 32

Esquemas modales

En los ejemplos anteriores se pudo apreciar que la validez de una fórmula depende de propiedades abstractas de la relación de accesibilidad. He aquí una lista de propiedades interesantes:

Francisco Hernández Quiroz

F, e |6 = 3¬p F, e |= 2¬p

para toda fórmula α, F |= 2α pero F 6|= 3α

F |= 2p ⇒ 3p Francisco Hernández Quiroz

v

p

Las propiedades anteriores corresponden con los siguientes esquemas de fórmulas válidas:

serial reflexiva simétrica transitiva euclidiana funcional parcial funcional densa débil conexa débil dirigida débil

Lógica modal

11 / 32

S1 S2 S3 S4 S5 S6 S7 S8 S9 S10

2α ⇒ 3α 2α ⇒ α α ⇒ 23α 2α ⇒ 22α 3α ⇒ 23α 3α ⇒ 2α 3α ⇒ 2α 22α ⇒ 2α 2(α ∧ 2α ⇒ β) ∨ 2(β ∧ 2β ⇒ α) 32α ⇒ 23α

Francisco Hernández Quiroz

Lógica Computacional

D(α) T (α) B(α) 4(α) 5(α) Q(α) R(α) G(α)

Lógica modal

12 / 32

Lógica modal Lógicas multimodales Cálculo µ

Lógica modal Lógicas multimodales Cálculo µ

Sintaxis Semántica S. axiomáticos

Sintaxis Semántica S. axiomáticos

Equivalencia entre propiedades de R y esquemas modales

Reglas de inferencia

MP Teorema. Sea F = hW , Ri. Entonces F |= Si

sii

K

2(α ⇒ β) ⇒ (2α ⇒ 2β)

N

α 2α

R satisface Pi .

Demostración. Se procede caso por caso.

EN

Francisco Hernández Quiroz

Lógica Computacional

Lógica modal

13 / 32

α ⇒ β, α β

α⇒β 2α ⇒ 2β

α⇒β 3α ⇒ 3β

Francisco Hernández Quiroz

Lógica Computacional

Lógica modal Lógicas multimodales Cálculo µ

Lógica modal Lógicas multimodales Cálculo µ

Sintaxis Semántica S. axiomáticos

El caso general L. epistémica Lógica temporal

Sistemas axiomáticos particulares

Una lógica multimodal tiene una sintaxis similar a la lógica modal, salvo que ahora se cuenta con un conjunto de etiquetas L. Sea a ∈ L. La sintaxis de una lógica multimodal es α ::= pi | qi | ri | ¬α | · · · | haiα | [a]α | h·iα | [ · ]α.

Los siguientes sistemas reciben un nombre particular

Los símbolos modales anteriores no tienen una lectura universalmente aceptada. Una posibilidad es:

S5 = KT 5.

En adelante, `S designará la relación de deducibilidad en un sistema S. Algunos sistemas son “subsistemas de otros”, es decir, sus teoremas son teoremas de sistemas más poderosos. Por ejemplo `KD5 α

Francisco Hernández Quiroz

implica

14 / 32

Lógicas multimodales

Todos los sistemas axiomáticos para lógica modal incluyen el axioma K y las reglas MP y N. La regla EN puede obtenerse a partir de K , MP y N. Otros sistemas son: KD KT KB K4 K5

S4 = KT 4

Lógica modal

`S5 α

Lógica Computacional

haiα [a]α h·iα [ · ]α

∀α

Lógica modal

15 / 32

se leerá se leerá se leerá se leerá

Francisco Hernández Quiroz

“después de transitar por a, posiblemente α” “después de transitar por a, necesariamente α” “después de cualquier transición, posiblemente α” “después de cualquier transición, necesariamente α”

Lógica Computacional

Lógica modal

16 / 32

Lógica modal Lógicas multimodales Cálculo µ

Lógica modal Lógicas multimodales Cálculo µ

El caso general L. epistémica Lógica temporal

El caso general L. epistémica Lógica temporal

Semántica de las lógicas multimodales

Sistemas axiomáticos

Un marco es una terna F = hW, R, Li, donde L es un conjunto de etiquetas y R ⊆ W × L × W. Sean w, v ∈ W y a ∈ L. Si R(w, a, v) escribiremos

Los siguientes axiomas son versiones multimodales de D, B, 5 y G: [a]α α hai hai[b]α

a

w → v. Finalmente, sea e : P0 × W → {V , F } una evaluación. Entonces F, e, w |= p

sii ... F, e, w |= [a]α sii F, e, w |= haiα sii F, e, w |= [ · ]α sii F, e, w |= h·iα sii Francisco Hernández Quiroz

∀p ∈ P0

e(p, w) = V a

∀v ∈ W . si w → v entonces F, e, v |= α a ∃v ∈ W . w → v y F, e, v |= α a ∀a ∈ L . ∀v ∈ W . si w → v entonces F, e, v |= α a ∃a ∈ L . ∃v ∈ W . w → v y F, e, v |= α Lógica Computacional

Lógica modal

17 / 32

hbiα [a]hbiα [b]hciα [c]hdiα

Sin embargo, los sistemas multimodales suelen tener axiomas específicos relacionados con su dominio de aplicación. Esto se verá en la sección de lógicas especializadas.

Francisco Hernández Quiroz

Lógica modal Lógicas multimodales Cálculo µ

Lógica modal Lógicas multimodales Cálculo µ

El caso general L. epistémica Lógica temporal

El caso general L. epistémica Lógica temporal

Lógicas especializadas

⇒ ⇒ ⇒ ⇒

Lógica Computacional

Lógica modal

18 / 32

Lógica epistémica La lógica epistémica trata de capturar (parte de) la noción de conocimiento. La versión que veremos incluye (a) la existencia de varios agentes cognoscitivos y (b) conocimiento común. Sean U un conjunto de agentes;

En esta ocasión abordaremos lógicas multimodales con axiomas específicos:

A⊆U a ∈ U;

Lógica epistémica

Entonces, la sintaxis de la lógica epistémica es:

Lógica temporal Y, además, veremos el operador no modal µ para fórmulas recursivas.

α ::= pi | qi | ri | ¬α | (α ∨ α) | · · · | Ka α | EA α | CA α Ka α EA α CA α

Francisco Hernández Quiroz

Lógica Computacional

Lógica modal

19 / 32

se leerá como se leerá como se leerá como

Francisco Hernández Quiroz

“el agente a sabe que α” “todos los agentes en A saben que α” “es conocimiento común entre los agentes en A que α” Lógica Computacional

Lógica modal

20 / 32

Lógica modal Lógicas multimodales Cálculo µ

Lógica modal Lógicas multimodales Cálculo µ

El caso general L. epistémica Lógica temporal

El caso general L. epistémica Lógica temporal

Semántica I

Semántica II De nuevo, se tiene un marco F = hW , R, Ai, con R ⊆ W × A × W, A un conjunto de agentes, w ∈ W y una evaluación e : P0 × W → {V , F }. Entonces F, e, w |= p sii e(p, w) = V ∀p ∈ P0 ... a F, e, w |= Ka α sii ∀v ∈ W . si w → v entonces F, e, v |= α a F, e, w |= EA α sii ∀a ∈ A . ∀v ∈ W . si w → v entonces F, e, v |= α

La definición formal de la semántica hace que El operador K sea en realidad un operador de necesidad en lógica multimodal (con una modalidad por agente) Ka α ≡def [a]α. Las fórmulas con el operador E sean abreviaturas (en caso de que A sea finito): ^ EA α ≡def Ka α.

F, e, w |= CA α sii A

La relación →∗ ⊆ W × W se define inductivamente:

a∈A

A

w →0 w sii w ∈ W

Pero el conocimiento común es una noción distinta: CA α ⇒ Ka α ∧ Ka Ka α ∧ · · · ∧ Kb Ka α ∧ · · ·

A

∀v ∈ W . si w →∗ v entonces F, e, v |= α

A

a

w →1 v sii ∃a ∈ A . w → v A

A

A

w →n+1 v sii ∃u ∈ W . w →n u ∧ u →1 v

∀a, b ∈ A.

A

A

w →∗ v sii ∃n ∈ N . w →n v Francisco Hernández Quiroz

Lógica Computacional

Lógica modal

21 / 32

Francisco Hernández Quiroz

Lógica Computacional

Lógica modal Lógicas multimodales Cálculo µ

Lógica modal Lógicas multimodales Cálculo µ

El caso general L. epistémica Lógica temporal

El caso general L. epistémica Lógica temporal

Semántica III

22 / 32

Sistema de demostración

Un sistema axiomático para la lógica epistémica contienen los axiomas de S5 “especializados”:

Nota. Obsérvese la ausencia de un operador análogo a hai. Podría definirse desde luego Pa α ≡def ¬Ka ¬α, pero su interpretación no corresponde claramente con una noción intuitiva de creencia, por ejemplo.

Francisco Hernández Quiroz

Lógica modal

Lógica Computacional

Lógica modal

23 / 32

Francisco Hernández Quiroz

K

Ka (α ⇒ β) ⇒ (Ka α ⇒ Ka β)

T

Ka α ⇒ α

4

Ka α ⇒ Ka Ka α

5

¬Ka α ⇒ Ka ¬Ka α

Lógica Computacional

Lógica modal

24 / 32

Lógica modal Lógicas multimodales Cálculo µ

Lógica modal Lógicas multimodales Cálculo µ

El caso general L. epistémica Lógica temporal

El caso general L. epistémica Lógica temporal

Lógica temporal

Sintaxis de LTL α ::= pi | qi | ri | ¬α | · · · | 3α | 2α | ◦α.

La lógica temporal formaliza una noción de tiempo discreta. Existen al menos dos versiones: LTL

lógica temporal de tiempo lineal;

CTL

lógica temporal de tiempo ramificado.

Los operadores modales se leerán ahora de la siguiente forma: 2α 3α ◦α αUβ

En ambas un estado en el tiempo corresponde a un mundo en un universo de Kripke. La segunda considera la posibilidad de que el tiempo “se ramifique”: puede haber varios futuros posibles y se pueden hacer afirmaciones sobre qué pasa en las otras “ramas” del tiempo. Aquí se abordará sólo la primera lógica, por simplicidad.

Francisco Hernández Quiroz

Lógica Computacional

Lógica modal

“α vale en todos los estados futuros” “α vale en algún estado futuro” “α vale en el siguiente estado” “α vale en este estado y en estados futuros al menos hasta el momento en que β valga” o bien “α vale hasta que β valga”.

Los operadores 2, 3 y ◦ suelen presentarse también como G, F y X, respectivamente. 25 / 32

Francisco Hernández Quiroz

Lógica Computacional

Lógica modal Lógicas multimodales Cálculo µ

Lógica modal Lógicas multimodales Cálculo µ

El caso general L. epistémica Lógica temporal

El caso general L. epistémica Lógica temporal

Semántica de la lógica temporal

F, e, w |= p

e(p, w) = V

F, e, w F, e, w F, e, w F, e, w

∀v ∈ W . si w → v entonces F, e, v |= α ∀v ∈ W . si w →∗ v entonces F, e, v |= α ∃v ∈ W . w →∗ v y F, e, v |= α ∃v ∈ W . w →∗ v y F, e, v |= β y ∀u ∈ W . si w →∗ u y u →∗ v entonces F, e, u |= α

Francisco Hernández Quiroz

Lógica Computacional

26 / 32

Algunas propiedades expresables en LTL

Para definir la semántica, se utilizará un marco de Kripke. → representa la relación de accesibilidad y →∗ , su cerradura transitiva y reflexiva. sii ... |= ◦α sii |= 2α sii |= 3α sii |= α U β sii

Lógica modal

Primero agregaremos una nueva fórmula atómica F con la propiedad de que

∀p ∈ P0

F, e, w 6|= F

Lógica modal

∀w ∈ W .

Entonces halt fin inf

27 / 32

≡def ≡def ≡def

Francisco Hernández Quiroz

◦F 3halt ¬fin

el proceso se detuvo el proceso se detendrá algún día el proceso es infinito

Lógica Computacional

Lógica modal

28 / 32

Lógica modal Lógicas multimodales Cálculo µ

Lógica modal Lógicas multimodales Cálculo µ

El caso general L. epistémica Lógica temporal

Sistemas de demostración para la lógica temporal

Cálculo µ

2(α ⇒ β) ⇒ 2α ⇒ 2β 2(α ∧ β) ⇔ 2α ∧ 2β 3α ⇔ α ∨ ◦3α ◦(α ∨ β) ⇔ ◦α ∨ ◦β ◦(α ∧ β) ⇔ ◦α ∧ ◦β α ∧ 2(α ⇒ ◦α) ⇒ 2α α N 2α

K

Francisco Hernández Quiroz

Lógica Computacional

El cálculo µ permite representar proposiciones recursivas, i.e., que se refieren a sí mismas. Consta de un conjunto de variables X, Y , Z , X0 , . . . proposicionales y un solo operador µ. Las fórmulas recursivas deben cumplir ciertas restricciones sintácticas para que la semántica esté bien definida.

Lógica modal

29 / 32

Lógica modal Lógicas multimodales Cálculo µ

Lógica Computacional

Lógica modal

30 / 32

Lógica modal Lógicas multimodales Cálculo µ

Sintaxis

Semántica Satisfacción, verdad y validez se definen en términos del cálculo de proposiciones (modal). Para el caso del operador µ combinado con lógica modal se tiene:

La sintaxis del cálculo µ proposicional es la siguiente: α ::= pi | qi | ri | ¬α | · · · µX . α(X)

F, e, w |= µX . α(X)

donde X es una variable proposicional. Intuitivamente, si la fórmula α contiene a X como una de sus proposiciones atómicas, µX . α(X) es la fórmula que resulta de sustituir a X en α por µX . α(X). Es posible definir un operador dual

F, e, w |= α[X/µX . α(X )] .

α(X) = p ∨ h·iX β = µX . α(X ) que es satisfecha por un modelo en el que p sea verdadera en el presente o en alguna transición futura. Matemáticamente, la semántica de una fórmula sólo está bien definida si la parte α(x) cumple con la restricción de monotonía: X aparece bajo el alcance de un número par de negaciones.

Pero la semántica de este operador es diferente.

Lógica Computacional

sii

Un ejemplo concreto es:

νX . α(X) ≡def ¬µX . ¬α(¬X).

Francisco Hernández Quiroz

Francisco Hernández Quiroz

Lógica modal

31 / 32

Francisco Hernández Quiroz

Lógica Computacional

Lógica modal

32 / 32