Download Lógicas Modales Computacionales [.4cm] Clase # 10: Construcción

Lógicas Modales Computacionales
Clase # 10: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera
2do Cuatrimestre 2006,
Buenos Aires, Argentina
Temario de Hoy
I
Resolución de Ejercicios
I
Completitud para la Lógica Híbrida
: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera
Ejercicios
I
Mostrar que la fórmula de Löb
2(2p → p) → 2p
define las propiedades de
I
I
: Construcción de Henkin
transitividad
R− es bien fundada (es decir, no hay caminos infinitos partiendo
de ningún punto; en particular, no hay ciclos).
Carlos Areces / Daniel Gorín / Sergio Mera
Las Lógicas Híbridas
I
Recordemos que la lógica híbrida básica (H(@)) es una
extensión del lenguaje modal básico con el agregado de
nominales y operadores de satisfacción
M, w |= i
M, w |= @i ϕ
sii
sii
w ∈ V(i)
M, v |= ϕ para v ∈ V(i)
donde M es un modelo de Kripke con la restricción de que para
todo nominal i, V(i) es un conjunto unitario.
I
Comencemos por investigar un poco la Teoría de
correspondencia para Lógicas Híbridas.
: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera
Teoría de Correspondencia para H(@)
I
En el lenguaje híbrido tenemos dos formas, intrinsicamente
diferentes, de escribir ciertas propiedades:
33p → 3p
33i → 3i
transitividad
transitividad
I
Notación: Llamaremos fórmula pura a una fórmula sin variables
proposicionales.
I
Proposición: Validez sobre frames de fórmulas puras puede ser
expresado en LPO:
hW, Ri |= ϕ sii hW, Ri |= ∀ī.∀x.STx (ϕ)
: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera
Algunas Propieades de Frames
i → 3i
i → 23i
33i → 3i
3i → 33i
3i → 2i
i → ¬3i
i → ¬33i
no expresable i → 2(3i → i)
3i
en LMB
@j 3i ∨ @j i ∨ @i 3j
@i (¬j ∧ ¬k) → @j k
: Construcción de Henkin
reflexividad
simetría
transitividad
densidad
determinismo
irreflexividad
asimetría
antisimetría
universalidad
tricotomía
a lo sumo 2 estados
Carlos Areces / Daniel Gorín / Sergio Mera
Completitud de H(@)
I
Las fórmulas puras tienen además importancia en relación con
completitud:
I
Teorema: Dada la axiomatización Kh para H(@)sobre la clase
de todos los frames, la axiomatización Kh + ∆, donde ∆ es un
conjunto de fórmulas híbridas puras, es completa para la clase de
frames definida por ∆.
: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera
La Axiomatización Kh
Axiomas
Reglas
PROP
K
K@
Dual
Dual@
Toda tautología proposicional
2(p → q) → (2p → 2q)
@i (p → q) → (@i p → @i q)
3p ↔ ¬2¬p
@i p ↔ ¬@i ¬p
MP
GEN
GEN@
SSUB
Int
Back
i ∧ p → @i p
3@i p → @ip
Ref
Sym
Nom
Agree
@i i
@i j ↔ @j i
@i j ∧ @j p → @i p
@j @i p ↔ @i p
: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera
Kh -MCS
I
I
Podemos definir conjuntos maximales consistentes para Kh de la
misma forma que hicimos para el lenguaje modal básico.
Pedimos que sea:
I
I
I
un conjunto de fórmulas consistente,
maximal en términos de inclusión,
que contenga los axiomas y que este cerrado por las reglas de
inferencia.
I
La construcción de modelo canónico que vimos funciona para
Kh , estableciendo completitud respecto de la clase de todos los
frames.
I
Pero el teorema que probamos aspira a más: queremos demostrar
completitud para Kh +∆ donde ∆ es un conjunto arbitrario de
axiomas puros.
: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera
Modelos Nombrados y un Lema Clave
Definción: Decimos que un modelo M = hW, R, Vi está sii para cada
w ∈ W, existe un nominal i tal que M, w |= i.
Lema: Sea M = hW, R, Vi un modelo nombrado y ϕ una fórmula
pura. Supongamos que para toda instancia ψ de ϕ tenemos
hW, R, Vi |= ψ. Entonces hW, Ri |= ϕ.
Nuestro objetivo entonces es construir un ‘modelo canónico
nombrado’.
: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera
Propiedades de Conjuntos Nombrados
Definición: Decimos que un Kh -MCS Γ esta nombrado si contiene un
nominal. Y todo nominal en Γ es un nombre para Γ.
Proposición: Sea Γ un Kh -MCS. Para todo nominal i, sea
∆ = {ϕ | @i ϕ ∈ Γ} entonces:
i) Para todo nominal i, ∆i es un Kh -MCS que contiene i.
ii) Para todos nominales i, j, si i ∈ ∆j entonces ∆i = ∆j
iii) para todos nominales i, j, @i ϕ ∈ ∆j sii @i ϕ ∈ Γ
iv) Si k es un nombre para Γ, entonces Γ = ∆k .
: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera
Construcción Canónica de Modelos Nombrados
I
Dado que queremos obtener un modelo nombrado, no podemos
tomar como dominio de nuestro modelo el conjunto de todos los
Kh -MCS (es fácil ver que {¬ik | k ∈ IN} es consistente).
I
Podríamos agregar un axioma que forzara que este conjunto
fuera consistente. Pero este axioma no es correcto en la clase de
todos los modelos (justamente, caracteriza a la clase de modelos
nombrados.)
I
Por otro lado, si es fácil mostrar que dado Γ consistente, siempre
podemos encontrar Γ+ Kh -MCS nombrado (posiblemente en un
lenguaje extendido con un nuevo nominal).
: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera
Construcción Canónica de Modelos Nombrados
I
I
Podemos considerar entonces NAMED =
{Γ+ } ∪ {∆i | ∆i obtenido de Γ+ } como nuestro dominio.
Pero nuestro sistema Kh actual, no es suficientemente fuerte para
demostrar un Existence Lemma.
I
I
I
El problema es que una fórmula de tipo 3ϕ en Γ requiere ahora,
no sólo de un MCS Γ0 ‘sincronizado’ con Γ que contenga ϕ,
sino además Γ0 tiene que ser obtenido a partir de Γ+ como alguno
de los ∆i .
Nuevas reglas (K+
h)
NAME
`j→θ
`θ
PASTE
` @i 3j ∧ @j ϕ → θ
` @i 3ϕ → θ
donde j es un nominal diferente de i que no aparece en θ ni en ϕ.
: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera
Lema de Lindenbaum Extendido
Lema: Sea NOM’ un conjunto infinito de nominales disjunto de
NOM, y sea HL0 el lenguaje obtenido al agregar NOM’ a HL.
Entonces todo conjunto de fórmulas Γ K+
h -consistente, puede
+
0
extenderse a un Γ Kh -MCS tal que
i) para algún nóminal i, i ∈ Γ0
ii) si @i 3ϕ ∈ Γ0 entonces @i 3j ∧ @j ϕ ∈ Γ0
: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera
Demo Sketch del Lema de Lindenbaum
0
Sea Γ K+
h -consistente. Definimos Σ = Γ ∪ {k} para k un nominal no
en Γ. Por NAME, Σ0 es consistente.
Enumerar las fórmulas de HL. Sea Σm+1 = Σm si Σm ∪ {ϕm+1 }
inconsistente.
Si Σm ∪ {ϕm+1 } consistente, entonces
i) Σm+1 = Σm ∪ {ϕm+1 } si ϕm+1 no es de la forma @i 3ϕ para
algún i.
ii) Σm+1 = Σm ∪ {ϕm+1 , @i 3j ∧ @j ϕ} si ϕm+1 es de la forma
@i 3ϕ donde j es un nominal nunca utilizado anteriormente. (La
consistencia de este paso esta asegurada por PASTE)
S
Sea Σ+ = n≥o Σn .
: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera
Construction of the Model
I
I
Sea Γ un conjunto K+
h -MCS obtenido a partir del lema de
Lindenbaum extendido.
Definimos MΓ = hW Γ , RΓ , V Γ i tal que
I
I
I
W Γ = {∆i | ∆i obtenido a partir de Γ}
RΓ wv sii {3ϕ | ϕ ∈ v} ⊆ w
V Γ (a) = {w | a ∈ w}
I
Lema: MΓ es un modelo híbrido.
I
Existence Lemma: Si 3ϕ ∈ w, entonces existe v ∈ W Γ tal que
RΓ wv y ϕ ∈ v.
: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera
Completitud
Teorema: Todo conjunto K+
h -consistente de fórmulas es satisfacible
en un modelo nombrado contable.
Además, Si Π es un conjunto de fórmulas puras, y P es la lógica
nomral híbrida obtenida al agregar todas las fórmulas de Π como
axiomas a K+
h , entonces, todo conjunto P-consistente de fórmulas es
satisfacible en un modelo nombrado contable, basado en un frame que
valida todas las fórmulas de P.
: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera
Algunos Comentarios sobre Completitud
I
La construcción de Modelo Canónico (que usamos para
completitud de la lógica modal básica), retorna una única
estructura (de cardinalidad no contable) que satisface todo
conjunto ∆-consistente para ∆ una lógica modal normal.
I
Así, toda lógica modal normal es completa respecto de alguna
clase de modelos, pero no necesariamente respecto de una de
frames.
I
Intuitivamente, el problema es que en esos casos, modelo
canónico satisface nuestros axiomas gracias a nuestra elección
de V ∆ la valuación canónica. Y no se cumple que estos sean
válidos a nivel del frame canónico.
: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera
Algunos Comentarios sobre Completitud
I
En el caso hibrido la situación es similar para fórmulas
arbitrarias, pero un resultado general de completitud puede darse
para el caso de fórmulas puras.
I
Usando la construcción de Henkin, obtenemos diferentes
modelos (contables) para cada conjunto K+
h -consistente.
I
Pero nos aseguramos que estos modelos siempre satisfacen los
axiomas puros a nivel de frames.
: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera
Bibliografía Relevante
I
Capítulo 7 del MLB.
: Construcción de Henkin
Carlos Areces / Daniel Gorín / Sergio Mera