Download Frames y Completitud

Lógicas Modales Computacionales
Clase # 9: Frames y Completitud
Carlos Areces / Daniel Gorín / Sergio Mera
2do Cuatrimestre 2006,
Buenos Aires, Argentina
Temario de Hoy
I
Resolución de Ejercicios
I
Frames
I
Relación entre Correctitud y Consistencia
Completitud
I
I
I
I
I
: Frames y Completitud
Teorema de Existencia
Canonicidad
Completitud respecto de Clases de Frames
Lógicas no Fuertemente Completas
Carlos Areces / Daniel Gorín / Sergio Mera
Ejercicios
I
Demostrar la correctitud de:
I
I
I
33p → 3p respecto de la clase de modelos transitivos.
p → 3p respecto de la clase de modelos reflexivos.
Recordar que
R∆ wv sii {3ϕ | ϕ ∈ v} ⊆ w
Mostrar que si R∆ wv entonces
{ϕ | 2ϕ ∈ w} ⊆ v
: Frames y Completitud
Carlos Areces / Daniel Gorín / Sergio Mera
Frames
I
I
I
Vimos que el conjunto de fórmulas válidas en una clase de
modelos no es necesariamente una logica.
Veamos que cuando usamos frames sí obtenemos siempre una
lógica.
Definición:
I
I
I
I
Un frame es una estructura hW, Ri donde W es un conjunto no
vacío y R es una relación binaria sobre R.
Dado un frame F = hW, Ri y una valuación V : PROP → W
entonces hW, R, Vi es un modelo basado en F.
Decimos que F |= ϕ sii M |= ϕ para todo M basado en F.
Proposición: Sea F una clase de frames, entonces
∆F = {ϕ | F |= ϕ para todoF ∈ F}
es una lógica modal normal.
: Frames y Completitud
Carlos Areces / Daniel Gorín / Sergio Mera
Teoría de Correspondencia
I
I
Además, a nivel de frames, ciertas fórmulas modales tienen aún
una relación más fuerte con ciertas formulas de primer orden,
que en el caso de modelos.
Por ejemplo vimos que 33p → 3p es válida en modelos
transitivos y p → 3p es válida en modelos reflexivos. I.e.,
I
I
I
I
I
Si R es transitiva entonces hW, R, Vi, w |= 33p → 3p
Si R es reflexiva entonces hW, R, Vi, w |= p → 3p
Pero hW, R, Vi, w |= 33p → 3p no implica R transitiva.
Tampoco hW, R, Vi |= 33p → 3p implica R transitiva.
A nivel de frames
I
I
: Frames y Completitud
Si hW, Ri |= 33p → 3p implica R transitiva.
Si hW, Ri |= p → 3p implica R reflexiva.
Carlos Areces / Daniel Gorín / Sergio Mera
Validez en Frames y Lógica de Segundo Orden
I
Vimos que distintas fórmulas modales definen propiedades de
primer orden al ser evaluadas sobre frames.
I
En realidad esto no es sorprendente, porque F |= ϕ es una
propiedad de segundo orden
F |= ϕ sii para todo V, hF, Vi |= ϕ
Es decir
F |= ϕ sii ∀P̄.∀x.STx (ϕ)
donde P̄ son las relaciones unarias asociadas a los símbolos de
proposición que aparecen en ϕ.
: Frames y Completitud
Carlos Areces / Daniel Gorín / Sergio Mera
Validez en Frames y Lógica de Segundo Orden
I
Entonces, lo normal es que las fórmulas modales definan
propiedades de segundo orden.
I
Lo sorprendente, en todo caso, es que algunas de ellas definen
propiedades de primer orden.
Es decir, ∀P̄.∀x.STx (ϕ) resulta equivalente a una fórmula de
LPO, ya que la cuantificación de segundo orden puede ser
eliminada.
I
Vamos a ver más adelante un resultado (“Fórmulas de
Sahlqvist”) que caracteriza un conjunto de fórmulas modales que
definen propiedades de primer orden (en realidad vamos a ver
que definen propiedades canónicas).
: Frames y Completitud
Carlos Areces / Daniel Gorín / Sergio Mera
Ejercicio: Validez en Frames
I
Un ejemplo clásico de fórmula modal que define una propiedad
de segundo orden es la formula de Löb:
L 2(2p → p) → 2p
que define las propiedades de:
I
I
I
transitividad
R− es bien fundada (es decir, no hay caminos infinitos partiendo
de ningún punto; en particular, no hay ciclos).
Ejercicio: Mostrar que si hW, Ri |= 2(2p → p) → 2p entonces
R es transitiva y R− es bien fundada.
: Frames y Completitud
Carlos Areces / Daniel Gorín / Sergio Mera
Relación entre Correctitud y Consistencia
“Que fuerte es la tentación de usar la semántica en la
demostración de completitud!”
Daniel Gorín
I
En la demostración del Existence Lemma habíamos llegado a
que para un ∆-MCS Γ qvq. no podía ser que 3ϕ ∈ Γ y 2⊥ ∈ Γ
(queríamos mostrar que en este caso Γ sería inconsistente).
I
Sabíamos además que Γ era un elemento de nuestro modelo
canónico.
I
Podríamos pensar que, como 3ϕ ∈ Γ entonces Γ tiene un
sucesor Γ0 y que esto contradecía que 2⊥ ∈ Γ.
I
Pero esto es justamente lo que estamos intentando probar!
(recuerden que el Existence Lemma es parte del Truth Lemma).
: Frames y Completitud
Carlos Areces / Daniel Gorín / Sergio Mera
Relación enre Correctitud y Consistencia
I
Ni siquiera habiendo ya demostrado Correctitud, podemos usar
información semántica en este caso.
Correctitud: ` ϕ ⇒|= ϕ
I
Correctitud puede usarse para argumentar que algo no es
demostrable:
` ϕ ⇒ |= ϕ
6|= ϕ ⇒ 6` ϕ
sii
Entonces, si M, w |= ¬ϕ ⇒6` ϕ. Es decir, un contraejemplo de
ϕ si nos dice que algo no es demostrable.
: Frames y Completitud
Carlos Areces / Daniel Gorín / Sergio Mera
Completitud
Existence Lemma: Para toda lógica modal normal ∆ y todo estado
w ∈ W ∆ (el dominio del modelo canónico para ∆), si 3ϕ ∈ w
entonces existe un estado v ∈ W ∆ tq. R∆ wv y ϕ ∈ v.
Primero algunas demostraciones:
i) ` 3ϕ → 3>
ii) ` 3> ∧ 2⊥ → ⊥
iii) ` 2(A ∧ B) → (2A ∧ 2B)
: Frames y Completitud
Carlos Areces / Daniel Gorín / Sergio Mera
Dem: Sea 3ϕ ∈ w. Sea v− = {ϕ} ∪ {ψ | 2ψ ∈ w}.
Afirmamos que v− es consistente.VPorque, supongamos que no.
Entonces Γ ⊆ v− finito tal que ` Γ → ⊥.
1) ϕ ∈ Γ : Si no, ` ψ1 ∧ . . . ∧ ψn → ⊥ para 2ψi ∈ w.
Pero ` ψ1 ∧ . . . ψn → ⊥ implica (porque ` 2(A ∧ B) → 2A → 2B)
que ` 2ψ1 ∧ . . . 2ψn → 2⊥
Con n applicaciones de MP tenemos que 2⊥ ∈ w
También 3ϕ ∈ w por lo que 3> ∈ w
Pero como ` 3> ∧ 2⊥ → ⊥, w sería inconsistente.
2) Entonces, tenemos que
` ψ1 ∧ . . . ∧ ψn → ¬ϕ
` 2(ψ1 ∧ . . . ∧ ψn ) → 2¬ϕ
` 2ψ1 ∧ . . . ∧ 2ψn → 2¬ϕ
Otra vez, n applicaciones de MP hacen que 2¬ϕ ∈ w.
Por Dual, ¬3ϕ ∈ w, contradiciendo que 3ϕ ∈ w.
: Frames y Completitud
Carlos Areces / Daniel Gorín / Sergio Mera
Teorema de Canonicidad
Teorema de Canonicidad: Todo lógima modal normal es
fuertemente completa respecto de su modelo canónico.
I
El teorema de Canonicidad es un resultado importante
teóricamente, pero “un tanto abstracto.”
I
Correctitud y Completitud Fuerte establecen sincronía entre `∆
y |=S (donde ∆ es una lógica y S una clase de estructuras)
Γ `∆ ϕ sii Γ |=S ϕ
I
Es decir que acabamos de mostrar que para toda lógica modal
normal tenemos que
Γ `∆ ϕ sii Γ |={M∆ } ϕ
: Frames y Completitud
Carlos Areces / Daniel Gorín / Sergio Mera
Completitud Respecto de Clases Semánticamente Definidas
I
Usualmente nos interesa trabajar con clases de estructuras más
concretas:
I
I
I
La clase de todos frames
La clase de todos frames transitivos
La clase de todos frames transitivos e inversamente bien
fundados.
I
Que tenemos que hacer para mostrar que K es correcto y
completo respecto de la clase de todos los modelos?
I
Nada. Trivialmente, M∆ es una instancia de un miembro de la
clase de todos los frames.
: Frames y Completitud
Carlos Areces / Daniel Gorín / Sergio Mera
Otras clases de Frames
I
Teorema: K4 es fuertemente completa respecto de la clase de
frames transitivos.
I
Teorema: KT es fuertemente completa respecto de la clase de
frames reflexivos.
I
Teorema: KT4 es fuertemente completa respecto de la clase de
frames reflexo-transitivos.
I
Teorema: KL es fuertemente completa respecto de la clase de
frames transitivos e inversamente bien fundados (No!!!).
: Frames y Completitud
Carlos Areces / Daniel Gorín / Sergio Mera
Canonicidad
I
Definición: Una fórmula ϕ es canónica si, para toda lógica
modal normal ∆, ϕ ∈ ∆ implica que ϕ es válida en el frame
canónico para ∆. Una lógica es canónica si su frame canónico es
un frame para ∆.
I
Definición: Decimos que una fórmula ϕ es canónica para la
propiedad P si el frame canónico de toda lógica modal normal ∆
tal que ϕ ∈ ∆ tiene la propiedad P, y ϕ es válida en toda clase
de frames que satisface P.
4 es canónica para transitividad. T es canónica para transitividad.
: Frames y Completitud
Carlos Areces / Daniel Gorín / Sergio Mera
Límites de la Construcción Canónica
I
Vamos a ver que no toda lógica modal normal es canónica.
I
Aún más, existen lógicas modales normales que no son la lógica
de ninguna clase de frames (la noción de lógica y de frames no
matchean exactamente). Es decir, vamos a ver que existen
lógicas consistentes, pero incompletas.
I
Empezamos por mostrar que KL no es canónica.
: Frames y Completitud
Carlos Areces / Daniel Gorín / Sergio Mera
No Canonicidad de KL
Teorema: KL no es correcta y fuertemente completa respecto de
ninguna clase de frames, y por lo tanto no es canónica.
Dem: Sea Γ = {3q1 } ∪ {2(qi → 3qi+1 ) | 1 ≤ i ∈ IN}
Vamos a mostrar que i) Γ es KL-consistente y ii) que ningún modelo
basado en un KL-frame puede satisfacer todas las fórmulas en Γ en
un mismo punto. El teorema se sigue de i) y ii).
: Frames y Completitud
Carlos Areces / Daniel Gorín / Sergio Mera
Bibliografía
I
Teoría de Correspondencia: Capítulo 3 del Modal Logic Book
I
Canonicidad: Capítulo 4 del Modal Logic Book
: Frames y Completitud
Carlos Areces / Daniel Gorín / Sergio Mera