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
