Download Lógica modal computacional Completitud

Lógica modal computacional
Completitud
Carlos Areces
1er Cuatrimestre 2012
Bibliografía
I
Capítulo 4 del Modal Logic Book, de Blackburn, Venema y de
Rijke.
: Lógica modal computacional, Completitud
Carlos Areces
Introducción
I
Al principio del curso habíamos visto que una lógica se puede
especificar tanto semántica como sintácticamente.
: Lógica modal computacional, Completitud
Carlos Areces
Introducción
I
Al principio del curso habíamos visto que una lógica se puede
especificar tanto semántica como sintácticamente.
I
El enfoque semántico se corresponde con la noción de
satisfacibilidad de una fórmula (o validez)
: Lógica modal computacional, Completitud
Carlos Areces
Introducción
I
Al principio del curso habíamos visto que una lógica se puede
especificar tanto semántica como sintácticamente.
I
El enfoque semántico se corresponde con la noción de
satisfacibilidad de una fórmula (o validez)
I
El enfoque sintáctico se corresponde con la noción de teorema.
: Lógica modal computacional, Completitud
Carlos Areces
Introducción
I
Al principio del curso habíamos visto que una lógica se puede
especificar tanto semántica como sintácticamente.
I
El enfoque semántico se corresponde con la noción de
satisfacibilidad de una fórmula (o validez)
I
El enfoque sintáctico se corresponde con la noción de teorema.
I
A partir de esto, surgía la pregunta de cuándo estas dos
alternativas estaban definiendo efectivamente la misma lógica.
: Lógica modal computacional, Completitud
Carlos Areces
Introducción
I
Al principio del curso habíamos visto que una lógica se puede
especificar tanto semántica como sintácticamente.
I
El enfoque semántico se corresponde con la noción de
satisfacibilidad de una fórmula (o validez)
I
El enfoque sintáctico se corresponde con la noción de teorema.
I
A partir de esto, surgía la pregunta de cuándo estas dos
alternativas estaban definiendo efectivamente la misma lógica.
I
Más precisamente, nos interesa ver si el conjunto de fórmulas
válidas es exactamente el mismo que el conjunto de teoremas.
: Lógica modal computacional, Completitud
Carlos Areces
Introducción
I
Al principio del curso habíamos visto que una lógica se puede
especificar tanto semántica como sintácticamente.
I
El enfoque semántico se corresponde con la noción de
satisfacibilidad de una fórmula (o validez)
I
El enfoque sintáctico se corresponde con la noción de teorema.
I
A partir de esto, surgía la pregunta de cuándo estas dos
alternativas estaban definiendo efectivamente la misma lógica.
I
Más precisamente, nos interesa ver si el conjunto de fórmulas
válidas es exactamente el mismo que el conjunto de teoremas.
I
Para responder a esta pregunta, tenemos que probar la
correctitud y completitud de nuestra lógica.
: Lógica modal computacional, Completitud
Carlos Areces
Introducción
Dado que vamos a trabajar con una variedad de lógicas modales,
veamos con más precisión qué lógicas vamos a considerar.
I
Una lógica modal ∆ es un conjunto de fórmulas modales que
contienen a todas las tautologías proposicionales y está cerrado
por:
I.
II .
modus ponens: Si ϕ ∈ ∆ y ϕ → ψ ∈ ∆ entonces ψ ∈ ∆.
sustitución uniforme: Si ϕ ∈ ∆ entonces también pertenece
cualquier substitución, que consiste en reemplazar
uniformemente cualquier proposición por una fórmula arbitraria.
: Lógica modal computacional, Completitud
Carlos Areces
Introducción
Dado que vamos a trabajar con una variedad de lógicas modales,
veamos con más precisión qué lógicas vamos a considerar.
I
Una lógica modal ∆ es un conjunto de fórmulas modales que
contienen a todas las tautologías proposicionales y está cerrado
por:
I.
II .
I
modus ponens: Si ϕ ∈ ∆ y ϕ → ψ ∈ ∆ entonces ψ ∈ ∆.
sustitución uniforme: Si ϕ ∈ ∆ entonces también pertenece
cualquier substitución, que consiste en reemplazar
uniformemente cualquier proposición por una fórmula arbitraria.
Si ϕ ∈ ∆ decimos que ϕ es un teorema de ∆, y lo notamos
como `∆ ϕ.
: Lógica modal computacional, Completitud
Carlos Areces
Introducción
Dado que vamos a trabajar con una variedad de lógicas modales,
veamos con más precisión qué lógicas vamos a considerar.
I
Una lógica modal ∆ es un conjunto de fórmulas modales que
contienen a todas las tautologías proposicionales y está cerrado
por:
I.
II .
modus ponens: Si ϕ ∈ ∆ y ϕ → ψ ∈ ∆ entonces ψ ∈ ∆.
sustitución uniforme: Si ϕ ∈ ∆ entonces también pertenece
cualquier substitución, que consiste en reemplazar
uniformemente cualquier proposición por una fórmula arbitraria.
I
Si ϕ ∈ ∆ decimos que ϕ es un teorema de ∆, y lo notamos
como `∆ ϕ.
I
Si ∆1 y ∆2 son lógicas modales tales que ∆1 ⊆ ∆2 decimos que
∆2 es una extensión de ∆1
: Lógica modal computacional, Completitud
Carlos Areces
Algunos ejemplos
I)
La colección de todas las fórmulas es una lógica. La lógica
inconsistente.
: Lógica modal computacional, Completitud
Carlos Areces
Algunos ejemplos
I)
La colección de todas las fórmulas es una lógica. La lógica
inconsistente.
T
II ) Si {∆i | i ∈ I} es una colección de lógicas, entonces i∈I ∆i es
una lógica.
: Lógica modal computacional, Completitud
Carlos Areces
Algunos ejemplos
I)
La colección de todas las fórmulas es una lógica. La lógica
inconsistente.
T
II ) Si {∆i | i ∈ I} es una colección de lógicas, entonces i∈I ∆i es
una lógica.
III )
Si M es una clase de modelos, entonces el conjunto ∆M de
fórmulas válidas en M no necesariamente es una lógica. Pensar
un contraejemplo!
: Lógica modal computacional, Completitud
Carlos Areces
Algunos ejemplos
I)
La colección de todas las fórmulas es una lógica. La lógica
inconsistente.
T
II ) Si {∆i | i ∈ I} es una colección de lógicas, entonces i∈I ∆i es
una lógica.
III )
Si M es una clase de modelos, entonces el conjunto ∆M de
fórmulas válidas en M no necesariamente es una lógica. Pensar
un contraejemplo!
Existe una lógica mínima que contiene a cualquier conjunto de
fórmulas Γ. La llamamos la lógica generada por Γ.
: Lógica modal computacional, Completitud
Carlos Areces
Algunos ejemplos
I)
La colección de todas las fórmulas es una lógica. La lógica
inconsistente.
T
II ) Si {∆i | i ∈ I} es una colección de lógicas, entonces i∈I ∆i es
una lógica.
III )
Si M es una clase de modelos, entonces el conjunto ∆M de
fórmulas válidas en M no necesariamente es una lógica. Pensar
un contraejemplo!
Existe una lógica mínima que contiene a cualquier conjunto de
fórmulas Γ. La llamamos la lógica generada por Γ.
I
Por ejemplo, la lógica generada por el conjunto vacío contiene a
todas las instancias de tautologías proposicionales y nada más.
La llamaremos PC.
: Lógica modal computacional, Completitud
Carlos Areces
Repaso de definiciones
I
Sean ψ1 , . . . , ψn , ϕ fórmulas modales. Decimos que ϕ es
deducible en el cálculo proposicional asumiendo ψ1 , . . . , ψn si
(ψ1 ∧ · · · ∧ ψn ) → ϕ es una tautología.
: Lógica modal computacional, Completitud
Carlos Areces
Repaso de definiciones
I
Sean ψ1 , . . . , ψn , ϕ fórmulas modales. Decimos que ϕ es
deducible en el cálculo proposicional asumiendo ψ1 , . . . , ψn si
(ψ1 ∧ · · · ∧ ψn ) → ϕ es una tautología.
Como todas las lógicas están cerradas bajo deducción en el cálculo
proposicional, si ϕ es deducible en el cálculo proposicional
asumiendo ψ1 , . . . , ψn , entonces `∆ ψ1 · · · `∆ ψn implica `∆ ϕ.
: Lógica modal computacional, Completitud
Carlos Areces
Repaso de definiciones
I
Sean ψ1 , . . . , ψn , ϕ fórmulas modales. Decimos que ϕ es
deducible en el cálculo proposicional asumiendo ψ1 , . . . , ψn si
(ψ1 ∧ · · · ∧ ψn ) → ϕ es una tautología.
Como todas las lógicas están cerradas bajo deducción en el cálculo
proposicional, si ϕ es deducible en el cálculo proposicional
asumiendo ψ1 , . . . , ψn , entonces `∆ ψ1 · · · `∆ ψn implica `∆ ϕ.
I
Si Γ ∪ {ϕ} es un conjunto de fórmulas, entonces ϕ es deducible
en ∆ a partir de Γ si `∆ ϕ o hay fórmulas ψ1 , . . . , ψn ∈ Γ tal que
`∆ (ψ1 ∧ · · · ∧ ψn ) → ϕ
: Lógica modal computacional, Completitud
Carlos Areces
Repaso de definiciones
I
Sean ψ1 , . . . , ψn , ϕ fórmulas modales. Decimos que ϕ es
deducible en el cálculo proposicional asumiendo ψ1 , . . . , ψn si
(ψ1 ∧ · · · ∧ ψn ) → ϕ es una tautología.
Como todas las lógicas están cerradas bajo deducción en el cálculo
proposicional, si ϕ es deducible en el cálculo proposicional
asumiendo ψ1 , . . . , ψn , entonces `∆ ψ1 · · · `∆ ψn implica `∆ ϕ.
I
Si Γ ∪ {ϕ} es un conjunto de fórmulas, entonces ϕ es deducible
en ∆ a partir de Γ si `∆ ϕ o hay fórmulas ψ1 , . . . , ψn ∈ Γ tal que
`∆ (ψ1 ∧ · · · ∧ ψn ) → ϕ
Si ese es el caso, escribimos Γ `∆ ϕ. Un conjunto de fórmulas Γ es
∆-consistente si Γ 6`∆ ⊥. Una fórmula ϕ es ∆-consistente si {ϕ} lo
es.
: Lógica modal computacional, Completitud
Carlos Areces
Lógica modal normal
I
La idea anterior estaba generalizando conceptos del cálculo
proposicional a los lenguajes modales
: Lógica modal computacional, Completitud
Carlos Areces
Lógica modal normal
I
La idea anterior estaba generalizando conceptos del cálculo
proposicional a los lenguajes modales
I
Ahora vamos a ver un concepto que es exclusivamente modal:
lógicas modales normales.
: Lógica modal computacional, Completitud
Carlos Areces
Lógica modal normal
I
La idea anterior estaba generalizando conceptos del cálculo
proposicional a los lenguajes modales
I
Ahora vamos a ver un concepto que es exclusivamente modal:
lógicas modales normales.
I
Una lógica modal ∆ es normal si contiene a la fórmula:
(K)
2(p → q) → (2p → 2q)
y está cerrada por la regla de generalización
(Nec) Si `∆ ϕ entonces `∆ 2ϕ
: Lógica modal computacional, Completitud
Carlos Areces
Ejemplos
I)
La lógica inconsistente es una lógica normal
: Lógica modal computacional, Completitud
Carlos Areces
Ejemplos
I)
II )
La lógica inconsistente es una lógica normal
Si {∆i | i ∈ I} es una colección de lógicas normales, entonces
T
i∈I ∆i es una lógica normal.
: Lógica modal computacional, Completitud
Carlos Areces
Ejemplos
I)
II )
III )
La lógica inconsistente es una lógica normal
Si {∆i | i ∈ I} es una colección de lógicas normales, entonces
T
i∈I ∆i es una lógica normal.
PC no es una lógica normal.
: Lógica modal computacional, Completitud
Carlos Areces
Ejemplos
I)
II )
III )
La lógica inconsistente es una lógica normal
Si {∆i | i ∈ I} es una colección de lógicas normales, entonces
T
i∈I ∆i es una lógica normal.
PC no es una lógica normal.
Existe una lógica normal mínima que contiene a cualquier conjunto de
fórmulas Γ. La llamamos la lógica generada por Γ.
: Lógica modal computacional, Completitud
Carlos Areces
Ejemplos
I)
II )
III )
La lógica inconsistente es una lógica normal
Si {∆i | i ∈ I} es una colección de lógicas normales, entonces
T
i∈I ∆i es una lógica normal.
PC no es una lógica normal.
Existe una lógica normal mínima que contiene a cualquier conjunto de
fórmulas Γ. La llamamos la lógica generada por Γ.
I
La lógica generada por el conjunto vacío es llamada K, y es la
mínima lógica normal. Si Γ es no vacío, muchas veces se denota
a la lógica normal generada por Γ como KΓ.
: Lógica modal computacional, Completitud
Carlos Areces
Ejemplos
I)
II )
III )
La lógica inconsistente es una lógica normal
Si {∆i | i ∈ I} es una colección de lógicas normales, entonces
T
i∈I ∆i es una lógica normal.
PC no es una lógica normal.
Existe una lógica normal mínima que contiene a cualquier conjunto de
fórmulas Γ. La llamamos la lógica generada por Γ.
I
La lógica generada por el conjunto vacío es llamada K, y es la
mínima lógica normal. Si Γ es no vacío, muchas veces se denota
a la lógica normal generada por Γ como KΓ.
También es usual llamar a Γ axiomas, y decir que la lógica es
generada usando las reglas de inferencia modus ponens, sustitución
uniforme y generalización.
: Lógica modal computacional, Completitud
Carlos Areces
Consequencia Semántica
Dada una clase de modelos S y un conjunto de fórmulas Γ ∪ {ϕ}
existen diferentes formas en que podemos definir la nocion de
consequencia semántica en S:
: Lógica modal computacional, Completitud
Carlos Areces
Consequencia Semántica
Dada una clase de modelos S y un conjunto de fórmulas Γ ∪ {ϕ}
existen diferentes formas en que podemos definir la nocion de
consequencia semántica en S:
I
Consequencia Local: Γ |=lS ϕ ssi
∀M ∈ S ∀w (M, w |= Γ =⇒ M, w |= ϕ)
: Lógica modal computacional, Completitud
Carlos Areces
Consequencia Semántica
Dada una clase de modelos S y un conjunto de fórmulas Γ ∪ {ϕ}
existen diferentes formas en que podemos definir la nocion de
consequencia semántica en S:
I
Consequencia Local: Γ |=lS ϕ ssi
∀M ∈ S ∀w (M, w |= Γ =⇒ M, w |= ϕ)
I
Consequencia Global: Γ |=gS ϕ ssi
∀M ∈ S (M |= Γ =⇒ M |= ϕ)
: Lógica modal computacional, Completitud
Carlos Areces
Consequencia Semántica
Dada una clase de modelos S y un conjunto de fórmulas Γ ∪ {ϕ}
existen diferentes formas en que podemos definir la nocion de
consequencia semántica en S:
I
Consequencia Local: Γ |=lS ϕ ssi
∀M ∈ S ∀w (M, w |= Γ =⇒ M, w |= ϕ)
I
Consequencia Global: Γ |=gS ϕ ssi
∀M ∈ S (M |= Γ =⇒ M |= ϕ)
La noción de consequencia local es la mas fuerte, en el sentido de si
Γ |=l ϕ entonces Γ |=g ϕ. Demostrar!. En el resto de la clase cuando
escribamos Γ |=S ϕ estamos hablando de Γ |=lϕ .
: Lógica modal computacional, Completitud
Carlos Areces
Soundness & Completeness
Repasemos las definiciones:
I
Una lógica ∆ es correcta con respecto a una clase de modelos S
si para toda fórmula ϕ y todo modelo M ∈ S, si `∆ ϕ entonces
M |= ϕ.
: Lógica modal computacional, Completitud
Carlos Areces
Soundness & Completeness
Repasemos las definiciones:
I
Una lógica ∆ es correcta con respecto a una clase de modelos S
si para toda fórmula ϕ y todo modelo M ∈ S, si `∆ ϕ entonces
M |= ϕ.
I
Una lógica ∆ es fuertemente completa con respecto a una clase
de modelos S si para cualquier conjunto de fórmulas Γ ∪ {ϕ}, si
Γ |=s ϕ entonces Γ `∆ ϕ.
: Lógica modal computacional, Completitud
Carlos Areces
Soundness & Completeness
La noción de completitud se puede reformular en término de consistencia.
: Lógica modal computacional, Completitud
Carlos Areces
Soundness & Completeness
La noción de completitud se puede reformular en término de consistencia.
I
Si Γ |=S ϕ entonces Γ `∆ ϕ
: Lógica modal computacional, Completitud
Carlos Areces
Soundness & Completeness
La noción de completitud se puede reformular en término de consistencia.
I
Si Γ |=S ϕ entonces Γ `∆ ϕ
I
Si Γ 6`∆ ϕ entonces Γ 6|=S ϕ
: Lógica modal computacional, Completitud
Carlos Areces
Soundness & Completeness
La noción de completitud se puede reformular en término de consistencia.
I
Si Γ |=S ϕ entonces Γ `∆ ϕ
I
Si Γ 6`∆ ϕ entonces Γ 6|=S ϕ
I
Si Γ 6`∆ ¬ϕ → ⊥ entonces Γ 6|=S ϕ
: Lógica modal computacional, Completitud
Carlos Areces
Soundness & Completeness
La noción de completitud se puede reformular en término de consistencia.
I
Si Γ |=S ϕ entonces Γ `∆ ϕ
I
Si Γ 6`∆ ϕ entonces Γ 6|=S ϕ
I
Si Γ 6`∆ ¬ϕ → ⊥ entonces Γ 6|=S ϕ
I
Si Γ ∪ {¬ϕ} 6`∆ ⊥ entonces Γ 6|=S ϕ
: Lógica modal computacional, Completitud
Carlos Areces
Soundness & Completeness
La noción de completitud se puede reformular en término de consistencia.
I
Si Γ |=S ϕ entonces Γ `∆ ϕ
I
Si Γ 6`∆ ϕ entonces Γ 6|=S ϕ
I
Si Γ 6`∆ ¬ϕ → ⊥ entonces Γ 6|=S ϕ
I
Si Γ ∪ {¬ϕ} 6`∆ ⊥ entonces Γ 6|=S ϕ
I
Si Γ ∪ {¬ϕ} es ∆-consistente entonces Γ 6|=S ϕ
: Lógica modal computacional, Completitud
Carlos Areces
Soundness & Completeness
La noción de completitud se puede reformular en término de consistencia.
I
Si Γ |=S ϕ entonces Γ `∆ ϕ
I
Si Γ 6`∆ ϕ entonces Γ 6|=S ϕ
I
Si Γ 6`∆ ¬ϕ → ⊥ entonces Γ 6|=S ϕ
I
Si Γ ∪ {¬ϕ} 6`∆ ⊥ entonces Γ 6|=S ϕ
I
Si Γ ∪ {¬ϕ} es ∆-consistente entonces Γ 6|=S ϕ
I
Si Γ ∪ {¬ϕ} es ∆-consistente entonces ∃M ∈ S t.q. M, w |= Γ ∪ {¬ϕ}
: Lógica modal computacional, Completitud
Carlos Areces
Soundness & Completeness
La noción de completitud se puede reformular en término de consistencia.
I
Si Γ |=S ϕ entonces Γ `∆ ϕ
I
Si Γ 6`∆ ϕ entonces Γ 6|=S ϕ
I
Si Γ 6`∆ ¬ϕ → ⊥ entonces Γ 6|=S ϕ
I
Si Γ ∪ {¬ϕ} 6`∆ ⊥ entonces Γ 6|=S ϕ
I
Si Γ ∪ {¬ϕ} es ∆-consistente entonces Γ 6|=S ϕ
I
Si Γ ∪ {¬ϕ} es ∆-consistente entonces ∃M ∈ S t.q. M, w |= Γ ∪ {¬ϕ}
: Lógica modal computacional, Completitud
Carlos Areces
Soundness & Completeness
La noción de completitud se puede reformular en término de consistencia.
I
Si Γ |=S ϕ entonces Γ `∆ ϕ
I
Si Γ 6`∆ ϕ entonces Γ 6|=S ϕ
I
Si Γ 6`∆ ¬ϕ → ⊥ entonces Γ 6|=S ϕ
I
Si Γ ∪ {¬ϕ} 6`∆ ⊥ entonces Γ 6|=S ϕ
I
Si Γ ∪ {¬ϕ} es ∆-consistente entonces Γ 6|=S ϕ
I
Si Γ ∪ {¬ϕ} es ∆-consistente entonces ∃M ∈ S t.q. M, w |= Γ ∪ {¬ϕ}
Es decir:
I
Una lógica modal normal ∆ es fuertemente completa con respecto a una
clase S sii cada conjunto ∆-consistente de fórmulas es satisfacible en
algún modelo M ∈ S.
: Lógica modal computacional, Completitud
Carlos Areces
Modelo canónico
I
Generalmente, demostrar correctitud con respecto a una clase S
es fácil.
I
I
Hay que ver que los axiomas son universalmente válidos en S
Hay que ver que las reglas de inferencia preservan verdad en S
: Lógica modal computacional, Completitud
Carlos Areces
Modelo canónico
I
Generalmente, demostrar correctitud con respecto a una clase S
es fácil.
I
I
I
Hay que ver que los axiomas son universalmente válidos en S
Hay que ver que las reglas de inferencia preservan verdad en S
Nos vamos a concentrar en demostrar completitud, y para eso
tenemos que ver cómo hacer para encontrar un modelo que
satisfaga a cada conjunto consistente de fórmulas.
: Lógica modal computacional, Completitud
Carlos Areces
Modelo canónico
I
Generalmente, demostrar correctitud con respecto a una clase S
es fácil.
I
I
I
I
Hay que ver que los axiomas son universalmente válidos en S
Hay que ver que las reglas de inferencia preservan verdad en S
Nos vamos a concentrar en demostrar completitud, y para eso
tenemos que ver cómo hacer para encontrar un modelo que
satisfaga a cada conjunto consistente de fórmulas.
Y las “piezas” que vamos a usar van a ser conjuntos maximales
consistentes.
: Lógica modal computacional, Completitud
Carlos Areces
Modelo canónico
I
Generalmente, demostrar correctitud con respecto a una clase S
es fácil.
I
I
I
I
Hay que ver que los axiomas son universalmente válidos en S
Hay que ver que las reglas de inferencia preservan verdad en S
Nos vamos a concentrar en demostrar completitud, y para eso
tenemos que ver cómo hacer para encontrar un modelo que
satisfaga a cada conjunto consistente de fórmulas.
Y las “piezas” que vamos a usar van a ser conjuntos maximales
consistentes.
Un conjunto de fórmulas Γ es maximal ∆-consistente si Γ es
∆-consistente y cualquier conjunto de fórmulas que contiene
propiamente a Γ es ∆-inconsistente.
I
Si Γ es un conjunto maximal ∆-consistente decimos que es un
∆-MCS.
: Lógica modal computacional, Completitud
Carlos Areces
Modelo canónico
¿Cuál es la intuición de usar MCSs en la prueba de completitud para
lógicas modales?
I
Observar que cada punto w en cada modelo M para una lógica ∆
está asociado con un conjunto de fórmulas {ϕ | M, w |= ϕ}.
: Lógica modal computacional, Completitud
Carlos Areces
Modelo canónico
¿Cuál es la intuición de usar MCSs en la prueba de completitud para
lógicas modales?
I
Observar que cada punto w en cada modelo M para una lógica ∆
está asociado con un conjunto de fórmulas {ϕ | M, w |= ϕ}.
I
No es difícil ver que este conjunto de fórmulas es efectivamente
un ∆-MCS. Y esto significa que si ϕ es verdadera en un modelo
para una lógica ∆, entonces ϕ pertenece a un ∆-MCS.
: Lógica modal computacional, Completitud
Carlos Areces
Modelo canónico
¿Cuál es la intuición de usar MCSs en la prueba de completitud para
lógicas modales?
I
Observar que cada punto w en cada modelo M para una lógica ∆
está asociado con un conjunto de fórmulas {ϕ | M, w |= ϕ}.
I
No es difícil ver que este conjunto de fórmulas es efectivamente
un ∆-MCS. Y esto significa que si ϕ es verdadera en un modelo
para una lógica ∆, entonces ϕ pertenece a un ∆-MCS.
I
Además, si w está relacionado con w0 en algún modelo M,
entonces la información de cada uno de los MCSs asociados a w
y w0 tienen que estar “coherentemente relacionada”.
: Lógica modal computacional, Completitud
Carlos Areces
Modelo canónico
La idea es trabajar con colecciones de MCSs coherentemente
relacionados para construir el modelo buscado. El objetivo es probar
el truth lemma, que nos dice que ‘ϕ pertenece a un MCS’ es
equivalente a ‘ϕ es verdadera en un modelo’.
I
Los mundos del modelo canónico van a ser todos los MCSs de la
lógica en la que estemos trabajando.
: Lógica modal computacional, Completitud
Carlos Areces
Modelo canónico
La idea es trabajar con colecciones de MCSs coherentemente
relacionados para construir el modelo buscado. El objetivo es probar
el truth lemma, que nos dice que ‘ϕ pertenece a un MCS’ es
equivalente a ‘ϕ es verdadera en un modelo’.
I
Los mundos del modelo canónico van a ser todos los MCSs de la
lógica en la que estemos trabajando.
I
Vamos a ver qué significa que la información de los MCSs esté
‘coherentemente relacionada’, y vamos a usar esa noción para
definir la relación de accesibilidad.
: Lógica modal computacional, Completitud
Carlos Areces
Propiedades de MCSs
Para llevar a cabo eso, veamos algunas propiedades que tienen los
MCSs. Si ∆ es una lógica y Γ es un ∆-MCS entonces:
I
∆ ⊆ Γ.
: Lógica modal computacional, Completitud
Carlos Areces
Propiedades de MCSs
Para llevar a cabo eso, veamos algunas propiedades que tienen los
MCSs. Si ∆ es una lógica y Γ es un ∆-MCS entonces:
I
∆ ⊆ Γ.
I
Γ está cerrado bajo modus ponens.
: Lógica modal computacional, Completitud
Carlos Areces
Propiedades de MCSs
Para llevar a cabo eso, veamos algunas propiedades que tienen los
MCSs. Si ∆ es una lógica y Γ es un ∆-MCS entonces:
I
∆ ⊆ Γ.
I
Γ está cerrado bajo modus ponens.
I
Para toda fórmula ϕ, ϕ ∈ Γ ó ¬ϕ ∈ Γ.
: Lógica modal computacional, Completitud
Carlos Areces
Propiedades de MCSs
Para llevar a cabo eso, veamos algunas propiedades que tienen los
MCSs. Si ∆ es una lógica y Γ es un ∆-MCS entonces:
I
∆ ⊆ Γ.
I
Γ está cerrado bajo modus ponens.
I
Para toda fórmula ϕ, ϕ ∈ Γ ó ¬ϕ ∈ Γ.
I
Para toda fórmula ϕ, ψ, ϕ ∨ ψ ∈ Γ sii ϕ ∈ Γ ó ψ ∈ Γ.
: Lógica modal computacional, Completitud
Carlos Areces
Lema de Lindenbaum
Como los MCSs van a ser las piezas que necesitamos para construir el
modelo canónico, tenemos que asegurarnos de tener suficientes.
Cualquier conjunto consistente de fórmulas puede ser extendido a uno
maximal consistente.
: Lógica modal computacional, Completitud
Carlos Areces
Lema de Lindenbaum
Como los MCSs van a ser las piezas que necesitamos para construir el
modelo canónico, tenemos que asegurarnos de tener suficientes.
Cualquier conjunto consistente de fórmulas puede ser extendido a uno
maximal consistente.
I Si Σ es un conjunto ∆-consistente de fórmulas, entonces existe
un ∆-MCS Σ+ tal que Σ ⊆ Σ+ .
: Lógica modal computacional, Completitud
Carlos Areces
Lema de Lindenbaum
Como los MCSs van a ser las piezas que necesitamos para construir el
modelo canónico, tenemos que asegurarnos de tener suficientes.
Cualquier conjunto consistente de fórmulas puede ser extendido a uno
maximal consistente.
I Si Σ es un conjunto ∆-consistente de fórmulas, entonces existe
un ∆-MCS Σ+ tal que Σ ⊆ Σ+ .
Demostración:
I ) Enumeramos las fórmulas de nuestro lenguaje ϕ1 , ϕ2 , . . . .
: Lógica modal computacional, Completitud
Carlos Areces
Lema de Lindenbaum
Como los MCSs van a ser las piezas que necesitamos para construir el
modelo canónico, tenemos que asegurarnos de tener suficientes.
Cualquier conjunto consistente de fórmulas puede ser extendido a uno
maximal consistente.
I Si Σ es un conjunto ∆-consistente de fórmulas, entonces existe
un ∆-MCS Σ+ tal que Σ ⊆ Σ+ .
Demostración:
I ) Enumeramos las fórmulas de nuestro lenguaje ϕ1 , ϕ2 , . . . .
II ) Definimos la secuencia de conjuntos:
Σ0
Σn+1
Σ+
= Σ
Σn ∪ {ϕn }
si el conjunto es ∆-consistente
=
Σ
∪
{¬ϕ
}
en otro caso
n
n
S
=
Σ
n≥0 n
: Lógica modal computacional, Completitud
Carlos Areces
Construcción del modelo canónico
El modelo canónico M ∆ para una lógica modal normal ∆ (en el
lenguaje básico) es hW ∆ , R∆ , v∆ i donde:
I
W ∆ es el conjunto de todos los ∆-MCSs
: Lógica modal computacional, Completitud
Carlos Areces
Construcción del modelo canónico
El modelo canónico M ∆ para una lógica modal normal ∆ (en el
lenguaje básico) es hW ∆ , R∆ , v∆ i donde:
I
W ∆ es el conjunto de todos los ∆-MCSs
I
R∆ es la relación binaria sobre W ∆ definida por R∆ wu si para
toda fórmula ψ, ψ ∈ u implica 3ψ ∈ w.
: Lógica modal computacional, Completitud
Carlos Areces
Construcción del modelo canónico
El modelo canónico M ∆ para una lógica modal normal ∆ (en el
lenguaje básico) es hW ∆ , R∆ , v∆ i donde:
I
W ∆ es el conjunto de todos los ∆-MCSs
I
R∆ es la relación binaria sobre W ∆ definida por R∆ wu si para
toda fórmula ψ, ψ ∈ u implica 3ψ ∈ w.
I
V ∆ es la valuación definida como V ∆ (p) = {w ∈ W ∆ | p ∈ w}
: Lógica modal computacional, Completitud
Carlos Areces
Algunos comentarios sobre el modelo canónico
I
La valuación canónica iguala la verdad de un símbolo
proposicional en w con su pertenencia a w. Nuestro objetivo es
probar el truth lemma que lleva “verdad = pertenencia” al nivel
de fórmulas.
: Lógica modal computacional, Completitud
Carlos Areces
Algunos comentarios sobre el modelo canónico
I
La valuación canónica iguala la verdad de un símbolo
proposicional en w con su pertenencia a w. Nuestro objetivo es
probar el truth lemma que lleva “verdad = pertenencia” al nivel
de fórmulas.
I
Los estados de M ∆ son todos los MCSs ∆-consistentes. La
consecuencia de esto es que, dado el lema de Lindenbaum,
cualquier conjunto ∆-consistente es un subconjunto de algún
punto en M ∆ . Y por el truth lemma que vamos a probar después,
cualquier conjunto ∆-consistente es verdadero en algún punto
del modelo.
: Lógica modal computacional, Completitud
Carlos Areces
Algunos comentarios sobre el modelo canónico
I
Esto significa que este único modelo M ∆ es un ‘modelo
universal’ para la lógica ∆.
: Lógica modal computacional, Completitud
Carlos Areces
Algunos comentarios sobre el modelo canónico
I
Esto significa que este único modelo M ∆ es un ‘modelo
universal’ para la lógica ∆.
I
Por último, la relación canónica de accesibilidad captura la idea
que dos MCSs están ‘coherentemente relacionados’ en función
de las fórmulas que valen en cada uno.
: Lógica modal computacional, Completitud
Carlos Areces
Completitud
Estamos en condiciones de probar el siguiente lema, que nos dice que
hay ‘suficientes’ MCSs en nuestro modelo para lo que necesitamos
hacer:
: Lógica modal computacional, Completitud
Carlos Areces
Completitud
Estamos en condiciones de probar el siguiente lema, que nos dice que
hay ‘suficientes’ MCSs en nuestro modelo para lo que necesitamos
hacer:
I
Existence lemma: Para cualquier lógica modal normal ∆, y
cualquier estado w ∈ W ∆ , si 3ϕ ∈ w entonces existe un estado
v ∈ W ∆ tal que R∆ wv y ϕ ∈ v.
Demostración: Supongamos que 3ϕ ∈ w. Vamos a construir v tal que
R∆ wv y ϕ ∈ v. Sea v− = {ϕ} ∪ {ψ | 2ψ ∈ w}.
I
v− es consistente. Ejercicio! (y acá hay que hacer
demostraciones sintácticas! :P)
Luego por Lindenbaum existe un ∆-MCS v que extiende a v− . Por
construcción, ϕ ∈ v, y para toda fórmula ψ, 2ψ ∈ w implica ψ ∈ v.
I
Esto último implica que R∆ wv. Ejercicio!
: Lógica modal computacional, Completitud
Carlos Areces
Completitud
Ahora sí podemos llevar “verdad = pertenencia” al nivel de fórmulas
arbitrarias.
I
Truth lemma: Para cualquier lógica modal normal ∆ y
cualquier fórmula ϕ, M ∆ , w |= ϕ sii ϕ ∈ w.
: Lógica modal computacional, Completitud
Carlos Areces
Completitud
Ahora sí podemos llevar “verdad = pertenencia” al nivel de fórmulas
arbitrarias.
I
Truth lemma: Para cualquier lógica modal normal ∆ y
cualquier fórmula ϕ, M ∆ , w |= ϕ sii ϕ ∈ w.
La demostración sale fácil por inducción en ϕ. El único caso
interesante es el modal, y eso está cubierto por el existence lemma (la
dirección difícil).
: Lógica modal computacional, Completitud
Carlos Areces
Completitud
Ahora sí podemos llevar “verdad = pertenencia” al nivel de fórmulas
arbitrarias.
I
Truth lemma: Para cualquier lógica modal normal ∆ y
cualquier fórmula ϕ, M ∆ , w |= ϕ sii ϕ ∈ w.
La demostración sale fácil por inducción en ϕ. El único caso
interesante es el modal, y eso está cubierto por el existence lemma (la
dirección difícil).
Y finalmente:
I
Teorema del Modelo Canónico: Cualquier lógica modal normal
es fuertemente completa con respecto a su modelo canónico.
: Lógica modal computacional, Completitud
Carlos Areces
Completitud
Ahora sí podemos llevar “verdad = pertenencia” al nivel de fórmulas
arbitrarias.
I
Truth lemma: Para cualquier lógica modal normal ∆ y
cualquier fórmula ϕ, M ∆ , w |= ϕ sii ϕ ∈ w.
La demostración sale fácil por inducción en ϕ. El único caso
interesante es el modal, y eso está cubierto por el existence lemma (la
dirección difícil).
Y finalmente:
I
Teorema del Modelo Canónico: Cualquier lógica modal normal
es fuertemente completa con respecto a su modelo canónico.
Demostración: Supongamos que Σ es un conjunto ∆-consistente. Por
el lema de Lindenbaum existe un ∆-MCS Σ+ que extiende a Σ. Por
el truth lemma, M ∆ , Σ+ |= Σ.
: Lógica modal computacional, Completitud
Carlos Areces
Completitud
Como corolario tenemos:
I
La lógica modal normal K es fuertemente completa con respecto
a la clase de todos los modelos.
: Lógica modal computacional, Completitud
Carlos Areces
Completitud
Como corolario tenemos:
I
La lógica modal normal K es fuertemente completa con respecto
a la clase de todos los modelos.
Por el teorema anterior, dado que K es una lógica modal normal, es
fuertemente completa con respecto a su modelo M K . Sólo queda
chequear que M K pertenece a la clase de todos los modelos, pero esto
es trivial.
: Lógica modal computacional, Completitud
Carlos Areces