Logica Modal

Capítulo 8
Lógica Modal
8.1. Introducción
El término “modalidad” significa: forma o manera de ser o de manifestarse
una cosa. En el caso de la lógica son los enunciados los que aparecen calificados
modalmente, añadiendo a su alcance descriptivo o denotativo una nueva dimen-
sión hasta cierto punto autorreflexiva. (En lógica modal escribimos ¤ϕ para
indicar que “ ϕ es una verdad necesaria”.)
Para interpretar las fórmulas modales se precisan contextos intensionales, de
referencias múltiples, que pueden ser de naturaleza temporal o incluir estados o
situaciones diversos.
La oposición “intensional” versus “extensional” se encuentra en toda la tra-
dición lógica, desde sus inicios hasta nuestros días. Sin embargo, los sistemas
lógicos básicos son extensionales en la concepción de Frege: la lógica proposi-
cional se ocupa del valor de verdad de las proposiciones, sin tener en cuenta
otros aspectos del significado; la de predicados trata sólo las extensiones de los
predicados –esto es, el conjunto de los objetos que los cumplen– y olvida
otras características de los conceptos que corresponden a esos predicados. En
el Begriﬀsschrift de Frege se critican implícitamente las nociones intensionales
diciendo, por ejemplo, que en “necesariamente A” la información lógicamente
relevante es “ A es verdadero”, lo demás no pasa de ser percepción psicológica,
semejante a cuando decimos “lo creo firmemente”.
Hay diversos sistemas lógicos en los que se toman los fenómenos intensionales
como objeto de estudio. El ejemplo paradigmático nos lo proporciona la lógica
modal, pero son también de esta clase la lógica epistémica –que se interesa
por los enunciados de creencia y de conocimiento–, la deóntica –que califica
los enunciados como obligatorios o simplemente permitidos–, la temporal –
siempre, alguna vez– y la dinámica1 .
1A la que dedicamos el capítulo 9.
195
196 CAPÍTULO 8. LÓGICA MODAL
8.1.1. Historia
La historia de la lógica modal comienza en la época clásica, incluyendo el
trabajo de Aristóteles, los megáricos (Diodoro Cronos) y los estoicos.
Los lógicos modales crearon un formalismo capaz de captar situaciones di-
námicas, de relativizar la verdad. Desde sus inicios se destacó la relación entre
nociones modales y temporales, siendo debatida por los megáricos y los estoicos.
El tratamiento sistemático es de principios del siglo XX, con Lewis a la cabeza,
aunque participan también Łukasievicz y Carnap. En esta fase se desarrollan
los cálculos modales, pero la semántica está sólo apuntada, sugerida. Con los
trabajos de Kanger, Hintikka, Prior y Kripke alcanza también ella una estruc-
turación y sistematización notable. Con los de Lemmon, Scott y Segerberg la
prueba de completud de los cálculos modales se lleva a término. Hay un cambio
de perspectiva con van Benthem, Thomason, Goldblatt y otros, conocido como
teoría de la correspondencia, que consiste fundamentalmente en tomarse en serio
las intuiciones obvias sobre la lectura clásica de las fórmulas modales, desarro-
llándose también una nueva semántica modal. Con posterioridad a 1975 su uso
en aplicaciones tanto a la Inteligencia Artificial como en informática teórica ha
hecho que se diversifique enormemente.
Para Aristóteles el tema principal es la diferencia entre necesidad y posibili-

dad.
Escribamos ¤ϕ para expresar que “ϕ es una proposición necesaria”
y ♦ϕ para expresar que “ ϕ es una proposición posible”. Aristóteles ve la
contradicción existente entre los pares
(¤ϕ y ¬¤ϕ) por un lado, y (♦ϕ y ¬♦ϕ) por otro (8.1)
pero piensa que no son contradictorios
(¤ϕ y ¬♦ϕ) ni (♦ϕ y ¬¤ϕ) (8.2)
–porque aunque ¬♦ϕ es lo mismo que ¤¬ϕ, y ¬¤ϕ es lo mismo que ♦¬ϕ
los otros pares podrían darse a la vez–
NECESARIO POSIBLE
¤ϕ ♦ϕ
¬♦¬ϕ ¬¤¬ϕ
IMPOSIBLE INNECESARIO
¬♦ϕ ¬¤ϕ
¤¬ϕ ♦¬ϕ
El denominado cuadro de Boecio de la silogística (ver página 104) aparece

ahora así modificado (ver figura: 8.1)
Aristóteles acepta como principio válido el siguiente:
α := ¤ϕ → ♦ϕ
Conclusión: ¤q ∨ ¤¬q
Comentario 271 En la primera de las propuestas la conclusión se sigue de-

ductivamente de las hipótesis, sin embargo la formalización de las dos primeras
hipótesis no es plausible. En la segunda sí que lo es, pero la conclusión no se
sigue de las hipótesis.
La relación entre nociones modales y temporales es muy antigua. Diodoro

define:
1. lo posible ♦ como aquello que es o será
2. lo imposible ¬♦ como aquello que siendo falso no será verdadero
3. lo necesario ¤ como aquello que es verdadero y no será falso
4. lo no necesario ¬¤ como aquello que es o será falso
Las denominadas paradojas de la implicación material a las que se respon-

sabiliza del nacimiento de la lógica modal fueron anticipadas por los filósofos
medievales. Las más importantes son:
1. “una proposición verdadera es implicada por cualquier proposición”
q → (p → q)
2. “toda proposición falsa implica cualquier proposición”
¬p → (p → q)
3. “todas las proposiciones están conectadas por implicación”
(p → q) ∨ (q → p)
Ninguna de ellas es contradictoria, si aceptamos el uso clásico –extensional–

del condicional material.
p q p→q
1 1 1
1 0 0
0 1 1
0 0 1
¿Capta este condicional el sentido de la implicación?

Si así fuera, sorprende en todos los casos la debilidad del vínculo entre an-
tecedente y consecuente de una implicación ya que sería de desear una relación
mucho más fuerte, de imposibilidad de antecedente sin consecuente –o tal vez
8.1. INTRODUCCIÓN 199
más constructiva: indicando cómo q se obtiene de p al operarlo de una cierta

manera para que p → q sea una implicación aceptable–.
El pistoletazo de salida de la carrera modal en el siglo XX se produce con

las investigaciones de Lewis de 1912 cuyo origen hay que buscarlo justamente
en el descontento creado por la interpretación de la implicación en el sistema
de Russell y Frege; esto es, en la tabla de verdad del condicional –también
denominado implicación material – que posibilita las paradojas y que hace que
la fórmula
α→β
sea equivalente a
¬(α ∧ ¬β)
y que él considera que debería tener la potencia de un
¬♦(α ∧ ¬β)
o, de forma equivalente, de un
¤(α → β)
Para solventar el problema se introduce un nuevo operador binario intensional,

no extensional, para la denominada implicación estricta
α →β
o, de forma equivalente, se la define con el operador de necesariedad.

Una observación semejante es extensiva al tratamiento de otras conectivas;
por ejemplo, en los enunciados α y β
α : John Lenon murió o John Lenon es una piedra
β : Eros no me ama o soy amada
la fuerza de la disyunción es muy distinta. En α es meramente “material”

su verdad en el mundo real depende del hecho empírico de que Lenon muriera.
En β no hace falta saber en qué mundo estamos, ni quien es Eros ni quien soy
yo. Así que se propone una nueva disyunción no extensional, paralela a la del
operador →.
La pregunta crucial es, ¿debemos expresar en el lenguaje objeto las diferen-
cias entre la disyunción de α y β?
Lewis piensa que sí y por ello introduce sus conocidos sistemas modales,
desde S1 a S5. El procedimiento es sólo sintáctico, mediante axiomas y reglas
de inferencia que seleccionan del conjunto de todas las fórmulas a sus teoremas
lógicos modales. Todavía la semántica es intuitiva, no está matematizada, no
hay tampoco una lectura única de los operadores modales, lo que origina en
consecuencia varias lógicas o sistemas modales.
La interpretación de las conectivas como funciones veritativas es ciertamente

fructífera. Sin embargo, ¿cómo interpretar ♦ϕ y ¤ϕ?, ninguna de las co-
nectivas monarias sobre {1, 0} serviría para ello. Una posibilidad, que apunta
Łukasiewicz, es tomar más valores de verdad. Así:
ϕ ¤ϕ ϕ ♦ϕ
1 1 1 1
1/2 0 1/2 1
0 0 0 0
Dejando a un lado el tratamiento algebraico, descrito por algunos como

sintaxis disfrazada, el que primero proporcionó una semántica a las fórmulas
modales fue Carnap. Algunos consideran que en él se funden tres corrientes fun-
damentales: Frege, Leibniz y Wittgenstein. De Frege2 le viene su interés por la
semántica, incluyendo la distinción entre intensión y extensión. De Leibniz la
interpretación de necesariedad como verdad en todo mundo posible, y posibilidad
como verdad en algunos, proporcionando de esta forma una semántica para S5.
De Wittgenstein tomó la idea de un mundo de hechos atómicos y de descripcio-
nes de estados. Veremos cómo se reelaborará esta intuición en los denominados
modelos canónicos, que se usan para probar completud. En la semántica de
Carnap tenemos:
U : descripciones de estados
s : un estado
p : proposición atómica
Definiéndose
U, s ° p syss p ∈ s
y para los operadores modales
U, s ° ¤ϕ syss para todo t ∈ U : U, t ° ϕ
El sistema S5 de Lewis es completo con la semántica de Carnap.
La semántica actualmente más usada es la de Kripke: La razón principal es

que es muy versátil, permite poner énfasis en las distintas relaciones de accesi-
bilidad, que proporcionan la “clave semántica” para la modalidad. Se definen
los modelos de la lógica modal como tripletes
D ® E
A = W, R, pA p∈ATOM (8.3)
donde:
W : estados, mundos, situaciones, puntos,...
R : relación de accesibilidad
2 De hecho Carnap fue uno de los escasísimos discípulos de Frege.
8.1. INTRODUCCIÓN 201
pA : conjunto de mundos donde p es verdadera
¿Qué significado intuitivo tienen las fórmulas?

Esta semántica permite muchas lecturas de los operadores modales:
Necesario (Lebniz): Una verdad es necesaria cuando lo es en todo mundo

posible
¤ϕ significa: ϕ es necesario en todo mundo posible
W : conjunto de mundos
R : relación de accesibilidad entre mundos.
hs, ti ∈ R : t es una alternativa a s –todas las verdades necesarias de
s se verifican–
Necesario en Física (6= Necesario en Lógica)

¤ϕ: ϕ es consecuencia de las leyes de la física
hs, ti ∈ R : t es una alternativa científica a s.
Por ejemplo, en nuestro mundo es verdadera ¤(x < c)
c : velocidad de la luz
x : velocidad de un objeto material
sin embargo, no es una verdad lógica.
Necesario en lógica deóntica

¤ϕ significa: ϕ es obligatorio
hs, ti ∈ R : t es una alternativa moral a s.
Necesario en lógica temporal

¤ϕ significa: “en todo momento futuro, ϕ”
♦ϕ significa: “en algún momento futuro, ϕ”
W : momentos (tiempo) –W puede ser N, Z, Q, R–
hs, ti ∈ R : t es posterior a s.
Lógica dinámica
¤ϕ significa: cada ejecución del programa que termina, lo hace en un
estado en donde vale ϕ
♦ϕ significa: hay una ejecución del programa que terminaen un estado en
donde vale ϕ
W : estados posibles de un proceso de computación
hs, ti ∈ R : hay una ejecución del programa que empieza en estado s y
termina en estado t
8.1.2. Necesario en lógica: El sistema S5

Es muy fácil entender el planteamiento en el caso de la lógica S5, la que
capta y sistematiza la necesariedad lógica. Observemos nuestras fórmulas clási-
cas desde la atalaya del metalenguaje; podremos en él expresar las características
de las expresiones clásicas pertinentes al nivel –esto es, su validez, satisfaci-
bilidad, etc– usando la lengua natural, utilizando signos como abreviaturas
–recuérdese que ² no es un signo del lenguaje objeto– o introduciendo el

lenguaje modal.
EN LENGUAJE
SIGNOS
ESPAÑOL MODAL
ϕ válida ϕ necesaria
²ϕ
ϕ tautología ¤ϕ
ϕ innecesaria
ϕ no válida 2ϕ ¬¤ϕ
♦¬ϕ
ϕ imposible
ϕ contradicción
² ¬ϕ ¤¬ϕ
ϕ insatisfacible
¬♦ϕ
ϕ satisfacible ϕ posible
2 ¬ϕ
¬ϕ no es válida ♦ϕ
ϕ contingente 2 ϕ y 2 ¬ϕ ♦¬ϕ ∧ ♦ϕ
De esta forma, en la lógica modal (PML) hemos formalizado el metalenguaje

(español o español con abreviaturas) que empleábamos para hablar del lenguaje
formal de la lógica proposicional (PL).
La ventaja es que ahora podremos no sólo expresar nuestros juicios sobre las
fórmulas de PL, sino que también los podremos verificar mediante un cálculo
deductivo; el de la lógica modal S5
Ejemplo 272 En la figura de clasificación de fórmulas se ve claramente que

las verdades necesarias constituyen un subconjunto del de las posibles y que las
imposibles son un subconjunto de las no necesarias.
En lógica modal lo expresamos así:
¤ϕ → ♦ϕ
¤¬ϕ → ¬¤ϕ
Incluso, y esta es la ventaja principal, podremos demostrarlo en un cálculo
deductivo.
Vamos a explicar de manera gráfica lo que hacemos al definir S5.

Para expresar ciertas características de las fórmulas de la lógica proposicio-
nal, usamos habitualmente el metalenguaje.
Metalenguaje
(de PL)
PL
Lenguaje objeto
¤ϕ : ϕ es necesariamente verdadera
ϕ es siempre verdadero
ϕ es obligatoriamente verdadero
ϕ es sabido
ϕ es creído
ϕ es demostrable (en la Aritmética)
ϕ es verdadero tras ejecutar el programa
etc.
y en consecuencia el catálogo de lógicas modales es amplio:
Normales (K, T, S4, S5, ...), temporales, dinámicas, epistémicas, deónticas, de
la demostrabilidad, etc.
Por consiguiente, no hay una única lógica modal, sino multitud de ellas. Ello se
concreta a nivel sintáctico y semántico.
1. Sintácticamente: distintos axiomas para las distintas lógicas
2. Semánticamente: distintas propiedades de la relación de accesibilidad
Comentario 274 De hecho, los axiomas de una lógica modal intentan caracte-
rizar las propiedades de la relación de accesibilidad que les es propia. Y no sólo
eso: el lenguaje modal puede entenderse como el lenguaje ideal para expresar
propiedades de las relaciones binarias, como se verá en lo que sigue. Es también
un lenguaje muy equilibrado: es bastante expresivo, sin dejar de ser decidible.
8.2. Lenguaje y Semántica

8.2.1. El lenguaje de la lógica modal
La lógica modal proposicional añade los operadores modales ¤ y ♦ al
alfabeto clásico, y una nueva regla de formación para ellos.
hf órmulai := hATOMi | ⊥ | ¬ hf órmulai | hf órmulai ∧ hf órmulai |

hf órmulai∨hf órmulai | hf órmulai → hf órmulai | hf órmulai ↔ hf órmulai |
¤ hf órmulai | ♦ hf órmulai
Es decir, además de las atómicas (regla F1), tenemos las fórmulas formadas
mediante la regla F2: ⊥, ¬ϕ, (ϕ ∧ ψ), (ϕ ∨ ψ), (ϕ → ψ), (ϕ ↔ ψ) y las que
usan la regla modal F3: ¤ϕ y ♦ϕ.
8.2. LENGUAJE Y SEMÁNTICA 205
OPERADORES MODALES
¤,Á♦ 


y
α ¤α ⊥ª
ÁTOMOS ϕ
(ϕ ∧ ψ)
pª Á
ψ x



CONECTORES BINARIOS
¬, ∨, ∧
→, ↔
Definición 275 FORM es el menor conjunto que contiene a las fórmulas

atómicas y está cerrado bajo F2 y F3
Ejemplo 276 Como ejercicios de formalización de enunciados de la lengua

natural podemos plantear los siguientes:
1. Nada es completamente relativo: ¬¤(♦α ∧ ♦¬α)
2. Es posible que no me entiendas, pero no es así necesariamente: ♦¬p ∧

¬¤¬p
3. Si puede que llueva, entonces necesariamente puede llover: ♦q → ¤♦q
4. Puede que me suspendan, pero tal esto vez no sea necesario: ♦r ∧ ♦¬¤r
8.2.2. Modelos de Kripke

Como se comentó con anterioridad, en un modelo de Kripke se nos da: un
conjunto W 6= ∅ de estados, mundos, situaciones, puntos,...; una relación bi-
naria, de accesibilidad entre ellos, R ⊆ W × W ; y, para interpretar a cada
fórmula atómica, un subconjunto de mundos, pA ⊆ W.
Dado un modelo de Kripke
D ® E
A = W, R, pA p∈ATOM (8.4)
definimos por inducción sobre la construcción de fórmulas una función de inter-

pretación
= : FORM(P M L) −→ ℘(W) (8.5)
que a cada fórmula ϕ ∈ FORM(P M L) le asigna como interpretación =(ϕ)
⊆ W –conjunto de los mundos donde ϕ es verdadera–
F1 Para fórmulas atómicas: =(p) = pA

F2 Para fórmulas obtenidas con operadores booleanos a partir de fórmulas

cualesquiera: =(⊥) = ∅, =(ϕ∧ψ) = =(ϕ)∩=(ψ), =(ϕ → ψ) = W−(=(ϕ)∩
(W − =(ψ)), de forma similar para el resto de conectivas
F3 Para fórmulas obtenidas con operadores modales a partir de fórmulas

cualesquiera:
=(♦ϕ) = {s ∈ W | ∃t(t ∈ W & hs, ti ∈ R & t ∈ =(ϕ))}
=(¤ϕ) = {s ∈ W | ∀t(t ∈ W & hs, ti ∈ R ⇒ t ∈ =(ϕ))}
Comentario 277 En lógica modal la interpretación de una fórmula no es un

valor de verdad, sino el conjunto formado por todos los estados o mundos donde
la fórmula es verdadera. A continuación veremos cómo podemos usar las inter-
pretaciones para definir el operador de satisfacibilidad y la relación de conse-
cuencia
8.2.3. Marcos de Kripke

Llamamos marcos de Kripke a las estructuras relacionales. En el caso de la
lógica multimodal hay varias relaciones, en el que nos ocupa, una sola, pudién-
dose decir que son todos de la forma
M = hW, Ri
donde W 6= ∅ y R ⊆ W × W. Podemos interpretar las fórmulas modales

usando estos marcos, siempre que definamos además una asignación
H : ATOM −→ ℘(W)
que con cada fórmula atómica asocia un subconjunto de W. De manera que
A = hM, Hi
será un modelo de Kripke –hacemos H(p) = pA – sobre el que se define

la interpretación = de la manera antes dicha. Escribiremos =H cuando
la referencia explícita a la asignación sea relevante –algunos autores escriben
[|ϕ|]H en vez de =H (ϕ)–.
Claramente con cada marco de Kripke se crean tantos modelos distintos
como funciones H se puedan definir, y cada modelo contiene un marco.
8.2.4. Estructuras por mundos (o puntos)

Dado un modelo de Kripke
D ® E
A = W, R, pA p∈ATOM
8.2. LENGUAJE Y SEMÁNTICA 207
y un elemento de su universo s ∈ W diremos que

D ® E
W, R, pA p∈ATOM , s
–que abreviadamente escribiremos hA, si– es la estructura de Kripke A en

el mundo s. La interpretación =s de una fórmula modal en una de estas
estructuras utiliza la definida para el modelo y extrae de él un valor de verdad,
F o V. Como era previsible su definición es:
=s (ϕ) = V syss s ∈ =(ϕ)
8.2.5. Tres “satisfacciones”

Para cada conjunto de letras proposicionales ATOM hemos definido tres
clases distintas de estructuras asociadas. Tenemos los marcos M = hW, Ri, que
pueden convertirse en modelos al unírseles asignaciones A = hM, Hi y tene-
mos también las estructuras por puntos hA, si . Es importante no confundirlas,
pues cada una juega su papel. Hay, por lo tanto tres relaciones de satisfacción
correspondientes.
Sea A = hM, Hi un modelo de Kripke, = su interpretación asociada,
M = hW, Ri su marco y s ∈ W.
1. ϕ es verdadera en estado s del modelo A : A, s ° ϕ ⇐⇒Df s ∈ =(ϕ)

Esta es la relación básica de satisfacción.
2. ϕ es válida (o verdadera) en el modelo A
A ° ϕ ⇐⇒Df ∀s ∈ W (A,s ° ϕ) –i.e. =(ϕ) = W–
3. ϕ es válida (o verdadera) en el marco M
M ° ϕ ⇐⇒Df ∀H (hM, Hi ° ϕ) –i.e. ∀H (=H (ϕ) = W)–
Cuando queramos distinguirlas explícitamente podemos usar superíndices
°p satisfacción por puntos, la primera
°v satisfacción por valoraciones o asignaciones, la segunda
°m satisfacción por marcos, la tercera
4. ϕ es válida: |= ϕ ⇐⇒Df ∀A A ° ϕ (para todo modelo)
5. ϕ es marco-válida: |=m ϕ ⇐⇒Df ∀M M °m ϕ (para todo marco)
⇐⇒Df ∀MH hM, Hi °v ϕ (para todo marco y todo modelo sobre él
construido)
6. ϕ es válida en la clase de modelos D
|=D ϕ ⇐⇒Df ∀A ∈ D [A ° ϕ] (para todo modelo de la clase)
7. ϕ es válida en la clase de marcos F
F ϕ ⇐⇒Df ∀M ∈ F [M ° ϕ] (para todo marco de la clase)
²m m
8. Γ es satisfacible en estado
\ s del modelo A
A,s ° Γ ⇐⇒Df s ∈ =(ϕ)
9. Γ es válido en\
el modelo A
A ° Γ ⇐⇒Df =(ϕ) = W
ϕ∈Γ
10. ϕ es consecuencia de Γ en la clase de modelos D \

Γ |=D ϕ ⇐⇒Df Para todo A ∈ D y s ∈ W: si s ∈ =(γ) entonces
γ∈Γ
s ∈ =(ϕ)
11. ϕ es consecuencia de Γ \
Γ |= ϕ ⇐⇒Df Para todo modelo A y s ∈ W : si s ∈ =(γ) entonces
γ∈Γ
s ∈ =(ϕ)
8.2.6. Ejercicios
Se puede ver que las siguientes fórmulas son válidas en todo modelo y en todo
marco, pero que no expresan condición alguna sobre la relación de accesibilidad.
1. ¤¬⊥
2. ¤(p ∨ ¬p)
3. ¤(p → (q → p))
4. ¤(α → β) → (¤α → ¤β)
5. ¤(α ∧ β) ↔ (¤α ∧ ¤β)
6. ¤(α → β) → (♦α → ♦β)
7. ♦(α ∨ β) ↔ (♦α ∨ ♦β)
8. ♦(α → β) → (¤α → ♦β)
Sin embargo, se pueden poner como ejemplos los de las fórmulas siguientes,
que no son válidas.
1. D := ¤ϕ → ♦ϕD E
®
tomando: A = W, R, pA p∈ATOM , W = {1}, R = ∅ y pA = ∅
2. T := ¤ϕ → ϕ D E
®
tomando (ver figura: 8.3): A = W, R, pA p∈ATOM , W = {0, 1},
R = {h0, 1i} y pA = {1}
3. B := ϕ → ¤♦ϕ D E
®
tomando (ver figura: 8.4): A = W, R, pA p∈ATOM , W = {0, 1},
R = {h0, 1i} y pA = {0}
4. 4 := ¤ϕ → ¤¤ϕ D E
®
tomando (ver figura: 8.5): A = W, R, pA p∈ATOM , W = {0, 1, 2},
R = {h0, 1i , h1, 2i} y pA = {1}
8.5. LÓGICAS MODALES PROPOSICIONALES 215
En otro lugar –concretamente, en la sección 12.1– entraré en el debate

sobre la naturaleza de los sistemas lógicos, ahora indicaré que hay dos procedi-
mientos para definir una lógica modal: el semántico y el sintáctico.
SEMÁNTICA SINTÁCTICA
Á Â
D Clase de modelos CAL cálculo

LOG(D) = {ϕ ||=D ϕ} LOG = {ϕ |`CAL ϕ}
Para no comprometerse con ninguno de estos planteamientos y permitir un

acercamiento neutro al tema, definiremos una lógica modal como un conjunto
de fórmulas modales que contiene a las tautologías (escritas modalmente, ¤ϕ y
♦ϕ cuentan como atómicas) y está cerrado bajo modus ponens.
Definición 283 Una lógica modal L es un conjunto tal que:
{ϕ ∈ F ORM |`P C ϕ} ⊆ L ⊆ F ORM
L está cerrado bajo M P

(es decir, α ∈ L & α → β ∈ L ⇒ β ∈ L)
Definición 284 (Teoremas lógicos) ϕ ∈ L syss `L ϕ
Definición 285 Deducibilidad a partir de hipótesis: Γ `L ϕ

syss hay {γ 1 , ..., γ n } ⊆ Γ tal que
(γ 1 ∧ ... ∧ γ n ) → ϕ ∈ L
Se puede demostrar que el operador de consecuencia `L así introducido

verifica las propiedades consiguientes; esto es, las características de un operador
clásico de consecuencia:
1. Monotonía: Γ ⊆ ∆ & Γ `L ϕ ⇒ ∆ `L ϕ
2. M P Generalizado: Γ `L ϕ & Γ `L ϕ → ψ ⇒ Γ `L ψ
3. Deducción: Γ ∪ {ϕ} `L ψ ⇒ Γ `L ϕ → ψ
8.5.1. Lógicas modales normales

A las lógicas modales normales se las suele definir sintácticamente
Definición 286 El cálculo {K, Df♦ }(N) de la lógica K contiene todas las tau-
tologías de la lógica clásica, la regla de M P y los siguientes axiomas y reglas:
1. K := ¤(ϕ → ψ) → (¤ϕ → ¤ψ)

2. Df♦ := ♦ϕ ↔ ¬¤¬ϕ
3. (N ) : ` ϕ ⇒ ` ¤ϕ (Denominada regla de necesariedad)
Definición 287 La lógica K (denominada lógica modal minimal) es la me-
nor lógica modal normal que contiene los esquemas axiomáticos K y Df♦ y
está cerrada bajo (N ) n o
K = ϕ |`{K,Df♦ }(N) ϕ
Otras lógicas modales normales se obtienen al añadirle alguno de los siguien-

tes esquemas axiomáticos: D, T, B, 4 ó 5. Las más conocidas son:
1. KT 4 Esta lógica es el resultado de añadir a la lógica minimal los axiomas
T y 4 (También conocida como S4)
2. KT 5 Esta lógica es el resultado de añadir a la lógica minimal los axiomas
T y 5 (También conocida como S5)
Ejercicio 288 Como ejercicio de deducción en la lógica S5 se puede demos-
trar:
Todas las lógicas modales normales obtenidas añadiendo a K algunos de los
axiomas D, T, B, 4 y 5 están contenidas en S5.
8.6. Completud y corrección

Tanto cuando se define la lógica como un conjunto de fórmulas válidas en una
clase de modelos de Kripke, como cuando nos valemos de un cálculo, es preciso
complementar la presentación con su otra dimensión semántica o sintáctica,
según el caso.
Para demostrar la equivalencia entre la semántica y la sintaxis de una lógica
modal se demuestran los teoremas de corrección y completud5 .
Definición 289 Una lógica modal B es correcta respecto de la clase de
modelos D syss para cada ϕ ∈ FORM :
`B ϕ ⇒ |=D ϕ
Definición 290 Una lógica modal B es completa respecto de la clase
de modelos D syss para cada ϕ ∈ FORM :
|=D ϕ ⇒ `B ϕ
Definición 291 Una lógica modal B está determinada por la clase de
modelos D syss para cada ϕ ∈ FORM
`B ϕ ⇐⇒ |=D ϕ
5 Una prueba alternativa de estos teoremas se establece en el entorno de la lógica multiva-
riada como marco unificador [13.4].
8.6. COMPLETUD Y CORRECCIÓN 217
8.6.1. Corrección
Teorema 292 (corrección de K). La lógica K es correcta en la clase formada
por todos los modelos de Kripke.
Demostración. Hay que demostrar que todas las tautologías son válidas en
la clase de todos los modelos de Kripke, que los esquemas axiomáticos K y
Df♦ son válidos y que tanto M P como N preservan la validez.
1. Es claro que las tautologías son válidas, pues la interpretación de los co-
nectores es la clásica.
2. Para ver que ² Df♦ tenemos que demostrar que si A es un modelo de

Kripke cualquiera y = su interpretación asociada, se cumple que
=(♦ϕ ↔ ¬¤¬ϕ) = W
Es decir, que
=(♦ϕ) = =(¬¤¬ϕ)
3. Para ver que ² K tenemos que demostrar que en toda interpretación

= sobre un modelo de Kripke A se cumple que
=((¤(ϕ → ψ) → (¤ϕ → ¤ψ)) = W
Es decir, que
=(¤(ϕ → ψ)) ⊆ =(¤ϕ → ¤ψ)
4. Para demostrar que la regla M P preserva la validez hemos de ver que

para todo modelo de Kripke A se cumple lo siguiente: Si A ² ϕ → ψ y
A ² ϕ entonces A ² ψ.
5. Para demostrar que la regla N preserva la validez hemos de ver que para
todo modelo de Kripke A se cumple lo siguiente: Si A ² ϕ entonces A ²
¤ϕ.
Corrección de otras lógicas modales normales

Para demostrar la corrección de las lógicas modales normales obtenidas con
D, T, B, 4 y 5 usamos las propiedades asociadas –esto es, las especificadas en
la sección 8.4–. Haciéndolo así es sencillo obtener lo siguiente:
Teorema 293 La lógica KD es correcta en la clase D de modelos de Kripke

con R serial
Teorema 294 La lógica KT es correcta en la clase E de modelos de Kripke

con R reflexiva
Teorema 295 La lógica KB es correcta en la clase F de modelos de Kripke

con R simétrica
Teorema 296 La lógica K4 es correcta en la clase G de modelos de Kripke
con R transitiva
Teorema 297 La lógica K5 es correcta en la clase H de modelos de Kripke
con R euclídea
Usando estos resultados demostramos la corrección de lógicas KS1 ...Sn
Teorema 298 Corrección de KS1 ...Sn
Demostración. Sean S1 , ..., Sn esquemas axiomáticos válidos, respectiva-
mente en las clases de modelos C1 , ..., Cn , entonces la lógica KS1 ...Sn es
correcta en la clase de modelos C1 ∩ ... ∩ Cn .
Si S1 , ..., Sn son esquemas axiomáticos válidos, respectivamente, en las clases
de modelos C1 , ..., Cn , entonces cada uno de los esquemas Si (i ∈ {1, ..., n})
es válido en la clase de modelos C1 ∩ ... ∩ Cn . Por otra parte, hemos visto que
la lógica minimal es correcta en la clase de todos los modelos de Kripke. Por
consiguiente, lo seguirá siendo en una clase más restringida de modelos.
Comentario 299 El teorema utilizado afirmaba que si una clase de modelos
era, respectivamente, serial, reflexiva, transitiva, simétrica o euclídea, entonces
dicha clase validaba, respectivamente los esquemas D, T, 4, B, 5. No demostra-
mos (porque no es válido) el teorema con una doble implicación; es decir, que
todo modelo de, respectivamente, D, T, 4, B, 5 sea, respectivamente, serial, re-
flexivo, transitivo, simétrico o euclídeo. Habitualmente sucede que si un modelo
no es, respectivamente, serial, reflexivo, transitivo, simétrico o euclídeo, enton-
ces fallará, respectivamente, D, T, 4, B, 5. Pero habrá que verlo en cada ocasión
porque para la semántica de modelos esta implicación no es necesariamente el
caso.
8.7. Modelos canónicos: completud

Para demostrar los teoremas de completud y de equivalencia de las lógicas
modales normales usamos este esquema (ver figura: 8.11):
Antes de comenzar con la demostración de la completud del cálculo compro-
bamos que el organigrama funciona; esto es,


ADECUACIÓN  



MODELO
CANÓNICO =⇒ COMPLETUD


& 



COROLARIO
La demostración es así de sencilla:
Supongamos que AB ∈ D y que AB ² ϕ ⇐⇒ `B ϕ, para cada ϕ ∈ FORM
Queremos demostrar que |=D ϕ ⇒ `B ϕ. Supongamos que |=D ϕ. Es
decir, que A ² ϕ, para cada A ∈ D. Puesto que AB ∈ D, tenemos que `B ϕ
Proposición 307 Γ `B ϕ ⇐⇒ Γ ∪ {¬ϕ} no es B−consistente

Proposición 308 Γ es B−consistente =⇒ para cada ϕ : Γ ∪ {ϕ} o Γ ∪
{¬ϕ} es consistente
Definición 309 Sea Γ ⊆ FORM. B es B−máximamente consistente ⇐⇒
Γ es B−consistente y para cada ϕ ∈ FORM : ϕ ∈ Γ o ¬ϕ ∈ Γ
D ® E
Ejemplo 310 Sea A = W, R, pA p∈ATOM un modelo de B y s ∈ W. El
conjunto {ϕ | A, s |= ϕ} es máximamente consistente.
Ejercicio 311 Sea Γ un conjunto B−máximamente consistente. Proponemos
como ejercicios los siguientes:
1. Γ `B ϕ =⇒ ϕ ∈ Γ
2. ϕ∈/ Γ =⇒ Γ ∪ {ϕ} es B−contradictorio
(Γ ⊆ ∆ y ∆ es B−consistente =⇒ Γ = ∆)
3. ¬ϕ ∈ Γ ⇐⇒ ϕ ∈
/ Γ, para cada ϕ ∈ F ORM
4. B⊆Γ
5. ⊥∈
/Γ
6. ϕ → ψ ∈ Γ ⇐⇒ (ϕ ∈ Γ =⇒ ψ ∈ Γ)
7. ϕ ∧ ψ ∈ Γ ⇐⇒ (ϕ ∈ Γ y ψ ∈ Γ)
8. ϕ ∨ ψ ∈ Γ ⇐⇒ (ϕ ∈ Γ ó ψ ∈ Γ)
9. ϕ ↔ ψ ∈ Γ ⇐⇒ (ϕ ∈ Γ ⇐⇒ ψ ∈ Γ)
8.7.2. Teorema de Lindenbaum

Como en la lógica clásica, se puede demostrar el teorema de Lindenbaum.
Teorema 312 Todo conjunto consistente Γ puede extenderse a uno máxima-
mente consistente ∆
Demostración. Sea Γ un conjunto B−consistente y sea ϕ1 , ..., ϕn , · · · una
enumeración de FORM
Definimos:
∆0 = Γ ½
∆n ∪ {ϕn } , si ∆n `B ϕn
∆n+1 =
∆n ∪
S{¬ϕn } , en caso contrario
Hagamos ∆ = n≥0 ∆n
Se puede demostrar que:
1. ∆n es B−consistente, para cada n ≥ 0
2. Para cada ϕ ∈ FORM : ϕ ∈ ∆ ó ¬ϕ ∈ ∆ (no ambos)
3. ∆ `B ϕ =⇒ ϕ ∈ ∆
8.7. MODELOS CANÓNICOS: COMPLETUD 221
8.7.3. Modelo canónico

Sea B una lógica modal normal, consistente. Llamaremos AB al modelo
canónico de B que definimos así:
D ® E
AB = WB , RB , pAB p∈ATOM
1. WB = {s ⊆ FORM | s es máximamente B − consistente}
2. RB ⊆ WB × WB se define así: hs, ti ∈ RB syss {ϕ | ¤ϕ ∈ s} ⊆ t
3. pAB = {s ∈ WB | p ∈ s} , para todo p ∈ ATOM
Vemos cómo en los modelos canónicos reaparecen las ideas de Carnap: el

universo lo forman las descripciones de estados.
¿Y qué descripción mejor y más pormenorizada podríamos tener que la de
un conjunto máximamente consistente?
Un conjunto tal contiene todas las sentencias capaces de caracterizar el mo-
delo, recoge todas sus verdades. La relación de accesibilidad: “ t es una alterna-
tiva a s” se establece cuando t satisface las verdades necesarias de s
Proposición 313 Sea B una lógica modal normal, consistente. AB su

modelo canónico. Para cada ϕ ∈ FORM, s ∈ WB :
¤ϕ ∈ s ⇐⇒ (para cada t ∈ WB : hs, ti ∈ RB =⇒ ϕ ∈ t])
Lema 314 (de la verdad) Sea B una lógica modal normal, consistente. AB
su modelo canónico.
Para cada ϕ ∈ FORM, s ∈ WB se verifica: AB , s |= ϕ ⇐⇒ ϕ ∈ s
Corolario 315 Sea B una lógica modal normal, consistente. AB su modelo

canónico. Para cada ϕ ∈ FORM se verifica: AB |= ϕ ⇐⇒ `B ϕ
Teorema 316 (Completud de K) La lógica K es completa en la clase de todos

los modelos de Kripke. Para cada ϕ ∈ FORM se verifica: |= ϕ =⇒ `K ϕ
Teorema 317 (Completud de KD) La lógica KD es completa en la clase D

de modelos de Kripke con R serial. Para cada ϕ ∈ FORM se verifica:
|=D ϕ =⇒ `KD ϕ ( basta mostrar la adecuación del modelo canónico; es
decir, AKD ∈ D)
Teorema 318 (Completud de KT ) La lógica KT es completa en la clase E

de modelos de Kripke con R reflexiva. Para cada ϕ ∈ FORM se verifica:
|=E ϕ =⇒ `KT ϕ
Teorema 319 (Completud de K4) La lógica K4 es completa en la clase F

de modelos de Kripke con R transitiva. Para cada ϕ ∈ FORM se verifica:
|=F ϕ =⇒ `K4 ϕ
Teorema 320 (Completud de KB) La lógica KB es completa en la clase G

de modelos de Kripke con R simétrica. Para cada ϕ ∈ FORM se verifica:
|=G ϕ =⇒ `KB ϕ
Teorema 321 (Completud de K5) La lógica K5 es completa en la clase H

de modelos de Kripke con R euclídea. Para cada ϕ ∈ FORM se verifica:
|=H ϕ =⇒ `K5 ϕ
Teorema 322 (Completud de KS1 ...Sn ) Sean S1 , ..., Sn esquemas axiomáti-

cos válidos, respectivamente en las clases de modelos C1 , ..., Cn , entonces la
lógica KS1 ...Sn es completa en la clase de modelos C1 ∩ ... ∩ Cn . Para cada
ϕ ∈ FORM se verifica: |=C 1 ∩...∩C n ϕ =⇒ `KS1 ...Sn ϕ
8.8. Apéndice: Tableaux para la lógica modal

Como se comentó con anterioridad en la sección 4.3 es fácil comprobar si una
prueba hecha en el cálculo axiomático o en uno de deducción natural es correcta,
pero hacerla no lo es en absoluto. Posiblemente el problema resida en la regla
de Modus Ponens y sobretodo en la ausencia de la denominada propiedad de la
subfórmula. Ni los sistemas axiomáticos ni los de deducción natural la tienen,
pero hay otros sistemas muy sencillos que sí que la tienen: los de Resolución,
los Sistemas de Gentzen y los Tableaux Semánticos de Smullyan.
Para las lógicas modales hay distintos tipos de tableaux. Hemos elegido uno
que incluye nombres para los mundos posibles como parte del mecanismo de-
ductivo, de forma que la relación de accesibilidad entre mundos queda reflejada
en las características sintácticas de sus propios nombres. Lo que haremos es
introducir prefijos.
La idea intuitiva es que un prefijo nombra un mundo posible. Si escribimos
ξ ϕ
siendo ξ un prefijo, queremos decir que ϕ es verdadera en el mundo cuyo

nombre es ξ. Los mundos de un modelo pueden estar relacionados mediante
la relación de accesibilidad, o no estarlo. El sistema de prefijos que elegiremos
nos permitirá saber cuando dos mundos están relacionados, mediante ciertas
características sintácticas de sus nombres.
Empezaremos por la lógica K, luego consideraremos otras lógicas modales.
8.8.1. Tableaux semánticos para la lógica K

Definición 323 Un prefijo para K es una sucesión finita y no vacía de
números naturales; por ejemplo, h1, 3, 2, 1, 4i . El mundo real es h1i
Definición 324 Una fórmula con prefijo es de la forma ξ ϕ, donde ϕ es

una fórmula y ξ un prefijo.
8.8. APÉNDICE: TABLEAUX PARA LA LÓGICA MODAL 223
Si n es un número natural y ξ es un prefijo, ξn es el resultado de

añadir n al final: por ejemplo, si ξ = h1, 3, 2, 1, 4i y n = 3, entonces
ξn = h1, 3, 2, 1, 4, 3i
Definición 325 Decimos que un prefijo de la forma ξn es K−accesible

desde ξ.
Un tableau tiene forma de árbol, donde cada nudo contiene una fórmula con
prefijo. Daremos reglas de inicio del tableau, reglas de inferencia y reglas para
terminar. Creo que resultará útil intercalar con la presentación de las reglas las
razones que justifican la corrección de las mismas; servirá tanto de motivación
intuitiva, como de justificación formal.
La definición de satisfacibilidad refleja la concepción que tenemos de un
tableau como una disyunción de sus ramas y una rama como la conjunción de
sus nudos.
Definición 326 Un tableau es K−satisfacible si alguna de sus ramas

es K−satisfacible. Y una rama es K−satisfacible si el conjunto de las fórmulas
con prefijo que lo constituyen lo es. Finalmente, un conjunto de fórmulas Γ es
K−satisfacible si hay un modelo
D ® E
A = W, R, pM p∈AT OM
y una función F de los prefijos de Γ en W tal que
1. Si ξ, χ están en Γ y el prefijo χ es accesible desde ξ, entonces
hF (ξ), F (χ)i ∈ R
2. Si ξ ϕ ∈ Γ, entonces A, F (ξ) ° ϕ.
Es decir, un conjunto de fórmulas con prefijo es K−satisfacible si describe

parcialmente un mundo. Ahora que hemos introducido esta terminología, pode-
mos presentar las reglas de los tableaux.
Reglas para K
Una demostración de ϕ comienza con h1i ¬ϕ.
El procedimiento de los tableaux es refutativo: Para demostrar ϕ suponemos
que puede haber algún modo de hacer que ϕ falle, y obtenemos de ello una
contradicción y concluimos que ϕ. Es fácil ver que si ϕ no es K−válida,
el conjunto {h1i ¬ϕ} es K−satisfacible y por lo tanto, el tableau con que
comienza es K−satisfacible.
Tenemos también reglas de inferencia, que son reglas de extensión de sus
ramas. Las clásicas son:
¬¬ Doble negación Una rama que contiene ξ ¬¬ϕ puede extenderse a ξ ϕ

¬ → Negación del condicional Una rama que contiene ξ ¬(ϕ → ψ) puede

extenderse dos nudos con ξ ϕ y ξ ¬ψ. (Es una regla de tipo α)
→ Condicional Una rama que contiene ξ (ϕ → ψ) puede bifurcarse en dos
ramas, con ξ ¬ϕ y ξ ψ. (Es una regla de tipo β)
Estas reglas se presentan esquemáticamente en la tabla siguiente

ξ ¬(ϕ → ψ)
ξ ¬¬ϕ ξ (ϕ → ψ)
––––––
–––– ––––––––
ξ ϕ
ξ ϕ ξ ¬ϕ || ξ ψ
ξ ¬ψ
A continuación introducimos las reglas propiamente modales, pero para ello
necesitamos introducir cierta terminología.
Definición 327 Un prefijo ξ está restringido en una rama siempre que sea un
segmento inicial (propio o impropio) de alguno de los prefijos de la rama.
Definición 328 Un prefijo está disponible en una rama si ocurre en la rama.
¤ Regla de necesariedad Una rama que contiene ξ ¤ϕ puede extenderse

a ξn ϕ para cualquier ξn disponible.
¬¤ Negación de necesariedad Una regla que contiene ξ ¬¤ϕ puede
extenderse a ξn ¬ϕ siempre que ξn no esté restringido en la rama
Es decir,
ξ ¤ϕ
–––
ξn ϕ
para cualquier ξn disponible
ξ ¬¤ϕ
–––
ξn ¬ϕ
siempre que ξn no esté restringido en la rama; es decir, no sea un segmento
inicial propio o impropio de ninguno de los prefijos de la rama.
De nuevo la motivación informal está clara: Si ¤ϕ es verdadera en un
mundo cuyo nombre es ξ, entonces ϕ es verdadera en todo mundo accesible
desde ξ; en particular, en ξn. También, si ¬¤ϕ es verdadera en el mundo
cuyo nombre es ξ, ¬ϕ debe ser verdadera en algún mundo accesible desde él;
podemos darle un nombre, pero este mundo no debe estar condicionado, debe
estar sin utilizar en el árbol. Es por ello por lo que la regla de la negación de
la necesariedad respeta la condición de que el prefijo no debe estar restringido.
Formalmente es fácil verificar que cada una de las reglas anteriores preserva
la K−satisfacibilidad. Es decir, si el conjunto de las fórmulas de la rama es
K−satisfacible antes de aplicarla, lo seguirá siendo después.
Esto completa la presentación de las reglas de extensión. Ahora indicamos
las de terminación.
Definición 329 Una rama de un tableau está cerrada si contiene ξ ϕ y ξ ¬ϕ para

una fórmula cualquiera, ϕ. O si contiene ξ ⊥ o ξ ¬>
Definición 330 Un tableau está cerrado, si cada rama lo está.
Definición 331 Un tableau cerrado que empieza por h1i ¬ϕ constituye una
prueba (por refutación) de ϕ.
Estar cerrado es la condición sintáctica que equivale en los árboles a ser

contradictorio. Formalmente, un tableau cerrado no puede ser K−satisfacible.
Ahora bien, si ϕ no es K−válida, entonces, como observamos antes, {h1i ¬ϕ} es
K−satisfacible y por lo tanto nuestro árbol inicial será K−satisfacible. Por con-
traposición diremos algo equivalente: Si hemos construido un tableau cerrado,
ϕ debe ser K−válida. Una prueba mediante tableaux garantiza la K−validez;
el procedimiento es correcto.
Reglas derivadas de inferencia En vez de tratar el resto de las conectivas

y modalidades como definidas en términos de ¬, → y de ¤, es más cómodo
proporcionar reglas derivadas para ellas.
ξ (ϕ ∧ ψ)
ξ ¬(ϕ ∧ ψ)
––––––
––––––––
ξ ϕ
ξ ¬ϕ || ξ ¬ψ
ξ ψ
ξ ¬(ϕ ∨ ψ)
ξ (ϕ ∨ ψ)
––––––
––––––––
ξ ¬ϕ
ξ ϕ || ξ ψ
ξ ¬ψ
ξ (ϕ ↔ ψ)
ξ ¬(ϕ ↔ ψ)
––––––
––––––––––––––
ξ (ϕ → ψ)
ξ ¬(ϕ → ψ) || ξ ¬(ψ → ϕ)
ξ (ψ → ϕ)
ξ ¬♦ϕ
––– para cualquier ξn disponible
ξn ϕ
ξ ♦ϕ
––– siempre que ξn no esté restringido en la rama
ξn ¬ϕ
–es decir, no sea un segmento inicial propio o impropio de ninguno de los
prefijos de la rama–
Completud
Voy a señalar simplemente la idea general de una demostración de completud,

que es sencilla.
Suponed que intentamos construir una demostración de ϕ. Empezamos el
tableau con h1i ¬ϕ, entonces aplicamos las reglas del tableau. Si lo hacemos
de una forma consistente, cada regla que puede ser aplicada lo habrá sido. No es
difícil indicar un procedimiento que asegure que no se cometen errores. Imaginad
que el procedimiento no termina en un tableau cerrado. Sea θ una rama no
cerrada. Por construcción, en la rama θ cada regla aplicable lo ha sido.
Construyamos un modelo
D ® E
A = W, R, pA p∈AT OM
como sigue:
W es el conjunto de los prefijos de θ. hξ, χi ∈ R syss χ es K−accesible
desde ξ. Hagamos pA = {ξ | ξ p está en θ} . Esto determina un modelo A.
Un argumento inductivo prueba que si ξ ϕ está en θ entonces
A, ξ ° ϕ
Puesto que h1i ¬ϕ está en θ (es su primer punto), A, h1i ° ¬ϕ. Por
consiguiente, ϕ no es válida.
Convirtiendo el argumento anterior por contraposición obtenemos: Si ϕ
es K−válida, entonces ϕ tiene una prueba mediante tableaux. De hecho, se
obtiene una prueba mediante cualquier tableau correcto que se construya. Hay
que señalar que el método anterior proporciona un procedimiento de decisión
para la lógica proposicional, K.
8.8.2. Lógica S4
Resulta fácil extender las ideas anteriores de forma que sirvan para otras
lógicas modales. Por ejemplo, obtenemos la lógica S4 manteniendo todo el
sistema anterior de la lógica K y modificando las reglas de los operadores
modales, que es sustituida por la siguiente:
Si ξ ¤ϕ está en una rama, entonces χ ϕ puede ser añadido para
cualquier prefijo χ que tenga a ξ como segmento inicial, propio o impropio
(la regla derivada para ¬¤ debe modificarse de forma similar)
Ejemplo 332 En este sistema demostramos que `S4 ¤p → ¤♦¤♦p así:

h1i ¬(¤p → ¤♦¤♦p)

h1i ¤p
h1i ¬¤♦¤♦p
h11i ¬♦¤♦p
h11i ¬¤♦p
h111i ¬♦p
h111i ¬p
h111i p
×
8.8.3. Otros sistemas modales

Para poder presentar sistemas modales para la variedad de lógicas moda-
les proposicionales que hemos estado estudiando, es conveniente introducir una
terminología nueva
Recordad que en la lógica K decíamos que un prefijo χ era accesible
desde ξ si χ era el resultado de añadir a ξ un número adicional al final.
Ahora queremos considerar otras relaciones de accesibilidad sobre prefijos, como
hicimos antes con S4.
Definición 333 La relación de accesibilidad sobre prefijos satisface:
1. La condición general: si ξn es accesible desde ξ, para cualquier n
2. La condición inversa: Si ξ es accesible desde ξn, para todo n
3. La condición de identidad (reflexividad): si ξ es accesible desde sí

mismo
4. La condición de transitividad: si χ es accesible desde ξ, siempre que

ξ sea un segmento inicial propio de χ
5. La condición universal (total): si cualquier prefijo es accesible desde cual-

quier otro.
Observad que la condición de transitividad incluye la condición general como

un caso particular: Para cada lógica se definirá una noción correspondiente de
accesibilidad de prefijos
LÓGICA CONDICIÓN DE ACCSESIBILIDAD

K, D general
T general, identidad
KB, DB general, inversa
B general, identidad, inversa
K4, D4 general, transitividad
S4 general, identidad, transitividad
S5 universal
Definición 334 Un prefijo χ es una extensión simple de ξ si χ es ξ con

un sólo número añadido al final.
Daremos las reglas básicas para el operador de necesariedad ¤ las del ope-
rador de posibilidad ♦ tienen una formulación similar
¬¤ Negación de necesariedad Una rama que contiene ξ ¬¤ϕ puede
extenderse a χ ¬ϕ siempre que χ sea una extensión simple de ξ, y no
esté restringido en la rama
¤ Regla de necesariedad Una rama que contiene ξ ¤ϕ puede extenderse
a χ ϕ para cualquier χ accesible desde ξ siempre que:
1. para las lógicas K, KB y KT, el prefijo χ debe estar disponible en

la rama.
2. para las lógicas D, T, DB, B, D4, S4 y S5, el prefijo χ debe ser
una extensión simple, no restringida de ξ o estar disponible en la
rama.
8.8.4. Sistema para la lógica S5

Para la lógica modal S5 la relación de accesibilidad ha degenerado en la
relación universal (de trivialidad, pues todos están relacionados con todos) y por
consiguiente se puede abandonar el sistema de prefijos como sucesiones finitas
e introducir otros más simples. Para esta lógica, pero sólo para ella, podemos
hacer que estos prefijos sean números naturales. Las reglas adecuadas para los
operadores modales se introducen a continuación:
¬¤ Negación de necesariedad Una rama que contiene n ¬¤ϕ puede ex-
tenderse a k ¬ϕ siempre que k sea nuevo en la rama.
¤ Regla de necesariedad Una rama que contiene n ¤ϕ puede extenderse
a k ϕ para cualquier número natural k
8.8.5. Prueba a partir de hipótesis

No hemos hablado de pruebas a partir de hipótesis, pero se puede hacer
fácilmente. Si L es cualquiera de las lógicas antes mencionadas, entonces
Γ `L Ω → ϕ
si y sólo si hay un tableau cerrado para h1i ¬ϕ, usando las reglas de los
tableaux antes mencionadas, junto a las siguientes:
Regla global ξ γ puede añadirse al final de cualquier rama, para cualquier
γ∈Γ
Regla local h1i ψ puede añadirse al final de cualquier rama, para cualquier
ψ ∈ Ω,
Bibliografía
[1] van Benthem, J.F.A.K. [1975]. “A Note on Modal Formulas and Relational
Properties”. JSL 40 : 55-58.
[2] van Benthem, J.F.A.K. [1976]. “Modal Reduction Principles” JSL 41 : 301-
312.
[3] van Benthem, J.F.A.K. [1978]. “Two Simple Incomplete Modal Logics”.
Theoria 44. 25-37.
[4] van Benthem, J. [1988] A manual of Intensional Logic, CSLI, Stanford. USA
[5] Boolos, G. [1979]. The Unprovability of Consistency. Cambridge University
Press. Cambridge.
[6] Bull, R.y Segerberg, K. [2001] “Basic Modal Logic” en pp. 1-88.In Handbook
of Philosophical Logic, Vol. II (Eds, Gabbay, D. and Guenther, F.) Reidel,
Dordrecht,
[7] Chellas, B. [1980] Modal Logic: an Introduction, Cambridge University Press,
Cambridge. U.K.
[8] Fine, K. [1980 y 1981]“First-Order Modal Theories” –I Sets, II Proposi-
tions, III Facts–. Parte I en Nous 15, 1981, 177-205; Parte II en Studia
Logica 39, 1980, 159-202; Parte III en Synthese, 1981, 43-122.
[9] Fine, Kit. [1974]“An Incomplete Logic Containing S4”. Theoria 60 : 23-29.
[10] Fine, K. [1978, 81]. “Model Theory for Modal Logic”, Partes I-III. Part I y
II en Journal of Philosophical Logic 7, 1978, 125-156, 277-306; Parte III
en Journal of Philosophical Logic 10, 1981, 293-307.
[11] Fine, K.[1975]. “Vagueness, Truth and Logic”. Synthese 30, 265-300.
[12] Fitch, F.B. [1973]. “A Correlation Between Modal Reduction Principles and
Properties of Relations”. Journal of Philosophical Logic 2. 97-101.
[13] Fitting, M. [1993] “Basic Modal and Temporal Logics”. In Handbook of
Logic in Artificial Intelligence and Logic Programming(Eds, Gabbay, D., Ho-
gger, C. J. and Robinson, J. A.) Oxford University Press, . In Handbook of
229
230 BIBLIOGRAFÍA
Logic in Artificial Intelligence and Logic Programming, edited by D. Gabbay,

C.J. Hogger and J.A. Robinson: Oxford University Press, 1993.
[14] Fitting, M. [1983]. Proof Methods for Modal and Tense Logics. Reidel. Dor-
drecht.
[15] Gabbay, D y Guenthner, F. [2001]. Handbook of Philosophical Logic 2 nd
edition. Kluwer Academic. Holanda. vol I-IV
[16] Gabbay, D. [1976]. Investigations in Model and Tense Logics, with Appli-
cations to Problems in Linguistics and Philosophy. . Reidel. Dordrecht.
[17] Gabbay, D., C.J. Hogger, and J.A. Robinson, eds. [1993]. Handbook of Logic
in Artificial Intelligence and Logic Programming. Oxford University Press,
Oxford.
[18] Gamut, L. T. F. [1991]. Logic, Language and Meaning. vol 2, Intensional
Logic and Logical Grammar. The University of Chicago Press. London. U.K.
[19] Gardies, J.L. [1979]. Lógica del Tiempo. Ed. castellana de J. Ordóñez y P.
Martínez-Freire. Paraninfo. Madrid, 1979.
[20] Goldblatt, R. [1986]. Logic of Time and Computation, Center for the Study
of Languege and Information. Stanford. USA
[21] Goldblatt, R. [1980]. “Diodorean Modality in Minkowski Space-Time”.
Studia Logica 39, 219-236.
[22] Haack, S. [1978]. Filosofía de las Lógicas. Ed. castellana de Amador Antón,
1982. ed. Madrid: Cátedra.
[23] Hintikka, J. [1969]. Models for Modalities. Reidel. Dordrecht.
[24] Hintikka, J. [1975]. The Intentions for Intentionality and Other New Models
for the Modalities. Reidel. Dordrecht.
[25] Huertas, A. [1994]. Modal Logic and Non-Classical Logic. Universidad de
Barcelona, tesis doctoral.
[26] Hughes, G. E. and Cresswell, M. J. [1968 (reimpreso con correcciones 1972)]
An introduction to modal logic, Methuen, London. U.K.
[27] Hughes, G. E. and Cresswell, M. J. [1984] A Companion to Modal Logic,
Methuen, London. U.K.
[28] Jansana, R. [1990]. Una Introducción a la Lógica Modal. Tecnos. Madrid.
[29] Kneale, W, y M. [1961]. El Desarrollo de la Lógica. Trducido por Javier
Muguerza, 1972, Colección Estructura y Función. Tecnos. Madrid.
[30] Kripke, Saul A. [1959]. “A completeness theorem in modal logic”. J. Sym-
bolic Logic 24, 1-14.
BIBLIOGRAFÍA 231
[31] Kripke, Saul A. [1963]. “Semantical analysis of modal logic I. Normal mo-
dal propositional calculi.”. Zeitschrift fur mathematische Logik und
Grundlagen der Mathematik. 9. 67-96.
[32] Kripke, Saul A. [1963]. “Semantical Considerations on Modal Logic”. Acta
Philosophica Fennica 16 : 83-94.
[33] Lemmon, E.J., and Dana S. Scott. [1977]. “The ‘Lemmon Notes’: an In-
troduction to Modal Logic.”. En American philosophical quarterly Mo-
nograph Series, edited by Nicholas Rescher. Basil Blackwell. Oxford.
[34] Manzano, M. [1996] Extensions of First Order Logic, Cambridge University
Press, Cambridge, U.K.
[35] Mints, G. [1992]. A short introduction to modal logic. CSLI, Stanford. USA
[36] Prior, A. N (ed). [1976]. Historia de la Lógica. Translated by Amador Antón
y Esteban Requena. Tecnos. Madrid.
[37] Sahlqvist, H. [1973]. “Completeness and Correspondence in the First and
Second Order Semantics for Modal Logic”. University of Oslo, .
[38] Sahlqvist, H. 1975“Completeness and Correspondence in the First and Se-
cond Order Semantics for Modal Logic.” In Proceedings of the 3rd Scandina-
vian Logic Symposium, 110-143: North-Holland, .
[39] Segerberg, K. [1971]. An Essay in Classical Modal Logic. Filosofiska Studier.
Uppsala University.
[40] Thomason, R. [1984]. “Combinations of Tense and Modality”. En [15]
[41] Thomason, S.K. [1974]. “An Incompleteness Theorem in Modal Logic”.
Theoria 60. 30-34.
232 BIBLIOGRAFÍA

Logica Modal

Cargado por

Copyright:

Formatos disponibles

Logica Modal

Cargado por

Información del documento

Título original

Derechos de autor

Formatos disponibles

Compartir este documento

Compartir o incrustar documentos

Opciones para compartir

¿Le pareció útil este documento?

¿Este contenido es inapropiado?

Copyright:

Formatos disponibles

Logica Modal

Cargado por

Copyright:

Formatos disponibles

Capítulo 8

1A la que dedicamos el capítulo 9.

Para Aristóteles el tema principal es la diferencia entre necesidad y posibili-

El denominado cuadro de Boecio de la silogística (ver página 104) aparece

Comentario 271 En la primera de las propuestas la conclusión se sigue de-

La relación entre nociones modales y temporales es muy antigua. Diodoro

1. lo posible ♦ como aquello que es o será

2. lo imposible ¬♦ como aquello que siendo falso no será verdadero

3. lo necesario ¤ como aquello que es verdadero y no será falso

4. lo no necesario ¬¤ como aquello que es o será falso

Las denominadas paradojas de la implicación material a las que se respon-

1. “una proposición verdadera es implicada por cualquier proposición”

2. “toda proposición falsa implica cualquier proposición”

3. “todas las proposiciones están conectadas por implicación”

Ninguna de ellas es contradictoria, si aceptamos el uso clásico –extensional–

¿Capta este condicional el sentido de la implicación?

más constructiva: indicando cómo q se obtiene de p al operarlo de una cierta

El pistoletazo de salida de la carrera modal en el siglo XX se produce con

Para solventar el problema se introduce un nuevo operador binario intensional,

o, de forma equivalente, se la define con el operador de necesariedad.

α : John Lenon murió o John Lenon es una piedra

β : Eros no me ama o soy amada

la fuerza de la disyunción es muy distinta. En α es meramente “material”

La interpretación de las conectivas como funciones veritativas es ciertamente

Dejando a un lado el tratamiento algebraico, descrito por algunos como

U, s ° ¤ϕ syss para todo t ∈ U : U, t ° ϕ

El sistema S5 de Lewis es completo con la semántica de Carnap.

La semántica actualmente más usada es la de Kripke: La razón principal es

pA : conjunto de mundos donde p es verdadera

¿Qué significado intuitivo tienen las fórmulas?

Necesario (Lebniz): Una verdad es necesaria cuando lo es en todo mundo

Necesario en Física (6= Necesario en Lógica)

Necesario en lógica deóntica

Necesario en lógica temporal

8.1.2. Necesario en lógica: El sistema S5

–recuérdese que ² no es un signo del lenguaje objeto– o introduciendo el

De esta forma, en la lógica modal (PML) hemos formalizado el metalenguaje

Ejemplo 272 En la figura de clasificación de fórmulas se ve claramente que

En lógica modal lo expresamos así:

Vamos a explicar de manera gráfica lo que hacemos al definir S5.

1. Sintácticamente: distintos axiomas para las distintas lógicas

2. Semánticamente: distintas propiedades de la relación de accesibilidad

8.2. Lenguaje y Semántica

hf órmulai := hATOMi | ⊥ | ¬ hf órmulai | hf órmulai ∧ hf órmulai |

Definición 275 FORM es el menor conjunto que contiene a las fórmulas

Ejemplo 276 Como ejercicios de formalización de enunciados de la lengua

1. Nada es completamente relativo: ¬¤(♦α ∧ ♦¬α)

2. Es posible que no me entiendas, pero no es así necesariamente: ♦¬p ∧

3. Si puede que llueva, entonces necesariamente puede llover: ♦q → ¤♦q

8.2.2. Modelos de Kripke

definimos por inducción sobre la construcción de fórmulas una función de inter-

F1 Para fórmulas atómicas: =(p) = pA

F2 Para fórmulas obtenidas con operadores booleanos a partir de fórmulas

F3 Para fórmulas obtenidas con operadores modales a partir de fórmulas

=(♦ϕ) = {s ∈ W | ∃t(t ∈ W & hs, ti ∈ R & t ∈ =(ϕ))}

=(¤ϕ) = {s ∈ W | ∀t(t ∈ W & hs, ti ∈ R ⇒ t ∈ =(ϕ))}

Comentario 277 En lógica modal la interpretación de una fórmula no es un

8.2.3. Marcos de Kripke

donde W 6= ∅ y R ⊆ W × W. Podemos interpretar las fórmulas modales