forallx-yyc-ml.tex

% !TeX root = ./forallxyyc.tex
% Chapter on modal logic. Original author: Rob Trueman, York
% University, http://www.rtrueman.com/

\part{Lógica Modal}
\label{ch.ML}
\addtocontents{toc}{\protect\mbox{}\protect\hrulefill\par}

\chapter{Introduciendo la lógica modal}
\label{Intro}

La lógica modal (LM) es la lógica de las \emph{modalidades}, formas en que una declaración puede ser verdadera. La \emph{necesidad} y la \emph{posibilidad} son dos de tales modalidades: una declaración puede ser verdadera, pero también puede ser necesariamente verdadera (verdadera sin importar cómo podría haber sido el mundo). Por ejemplo, las verdades lógicas no son simplemente verdaderas debido a alguna característica accidental del mundo, sino verdaderas pase lo que pase. Una declaración posible puede no ser realmente verdadera, pero podría haber sido verdadera. Usamos $\ebox$ para expresar necesidad, y $\ediamond$ para expresar posibilidad. Así, puedes leer $\ebox \metav{A}$ como \emph{Es necesariamente el caso que} $\metav{A}$, y $\ediamond \metav{A}$ como \emph{Es posiblemente el caso que} $\metav{A}$.

Hay muchos tipos diferentes de necesidad. Es \emph{humanamente imposible} para mí correr a 100 mph. Dados los tipos de criaturas que somos, ningún humano puede hacer eso. Pero aún así, no es \emph{físicamente imposible} para mí correr tan rápido. No tenemos la tecnología para hacerlo todavía, pero seguramente es físicamente posible intercambiar mis piernas biológicas por unas robóticas que podrían correr a 100 mph. Por el contrario, es físicamente imposible para mí correr más rápido que la velocidad de la luz. Las leyes de la física prohíben que cualquier objeto acelere hasta esa velocidad. Pero incluso eso no es \emph{lógicamente} imposible. No es una contradicción imaginar que las leyes de la física podrían haber sido diferentes, y que podrían haber permitido que los objetos se movieran más rápido que la luz.

\textexclamdown Con qué tipo de modalidad trata LM? \textexclamdown \emph{Con todas ellas}! LM es una herramienta muy flexible. Comenzamos con un conjunto básico de reglas que gobiernan $\ebox$ y $\ediamond$, y luego agregamos más reglas para ajustarnos a cualquier tipo de modalidad que nos interese. De hecho, LM es tan flexible que ni siquiera tenemos que pensar en $\ebox$ y $\ediamond$ como expresiones de \emph{necesidad} y \emph{posibilidad}. En cambio, podríamos leer $\ebox$ como expresión de \emph{probabilidad}, de modo que $\ebox\metav{A}$ significa \emph{Es demostrable que} $\metav{A}$, y $\ediamond\metav{A}$ significa \emph{No es refutable que} $\metav{A}$. De manera similar, podemos interpretar $\ebox$ para significar que $S$ \emph{sabe que $\metav{A}$} o que $S$ \emph{cree que $\metav{A}$}. O podríamos leer $\ebox$ como expresión de \emph{obligación moral}, de modo que $\ebox \metav{A}$ significa \emph{Es moralmente obligatorio que} $\metav{A}$, y $\ediamond \metav{A}$ significa \emph{Es moralmente permisible que} $\metav{A}$. Todo lo que necesitaríamos hacer es inventar las reglas correctas para estas diferentes lecturas de $\ebox$ y $\ediamond$.

Una fórmula modal es aquella que incluye operadores modales como $\ebox$ y $\ediamond$. Dependiendo de la interpretación que asignemos a $\ebox$ y $\ediamond$, diferentes fórmulas modales serán demostrables o válidas. Por ejemplo, $\ebox \metav{A} \eif \metav{A}$ podría decir que ``si $\metav{A}$ es necesario, es verdadero'', si $\ebox$ se interpreta como necesidad. Podría expresar ``si $\metav{A}$ es conocido, entonces es verdadero'', si $\ebox$ expresa verdad conocida. Bajo ambas interpretaciones, $\ebox\metav{A} \eif \metav{A}$ es válido: Todas las proposiciones necesarias son verdaderas pase lo que pase, por lo que son verdaderas en el mundo real. Y si una proposición se sabe que es verdadera, debe ser verdadera (uno no puede saber algo que es falso). Sin embargo, cuando $\ebox$ se interpreta como ``se cree que'' o ``debería ser el caso que'', $\ebox\metav{A} \eif \metav{A}$ no es válido: Podemos creer proposiciones falsas. No toda proposición que debería ser verdadera es de hecho verdadera, por ejemplo, ``Todo asesino será llevado ante la justicia.'' Esto \emph{debería} ser verdadero, pero no lo es.

Consideraremos diferentes tipos de sistemas de LM. Difieren en las reglas de prueba permitidas y en la semántica que usamos para definir nuestras nociones lógicas. Los diferentes sistemas que consideraremos se llaman \mlK, \mlT, \mlSfour y \mlSfive. \mlK{} es el sistema básico; todo lo que es válido o demostrable en \mlK{} también es demostrable en los demás. Pero hay algunas cosas que \mlK{} no prueba, como la fórmula $\ebox A \eif A$ para la letra de oración~$A$. Entonces \mlK{} no es una lógica modal apropiada para la necesidad y la posibilidad (donde $\ebox\metav{A} \eif \metav{A}$ debería ser demostrable). Esto es demostrable en el sistema \mlT, por lo que \mlT{} es más apropiado cuando se trata de necesidad y posibilidad, pero menos apropiado cuando se trata de creencia u obligación, ya que entonces $\ebox\metav{A} \eif \metav{A}$ no debería (siempre) ser demostrable. El sistema quizás mejor de LM para la necesidad y la posibilidad, y en cualquier caso el más ampliamente aceptado, es el más fuerte de los sistemas que consideramos, \mlSfive.

\section{El Lenguaje de LM}
\label{TFLtoML}

Para hacer lógica modal, tenemos que hacer dos cosas. Primero, queremos aprender a probar cosas en LM. Segundo, queremos ver cómo construir interpretaciones para LM. Pero antes de que podamos hacer cualquiera de estas cosas, necesitamos explicar cómo construir oraciones en LM.

El lenguaje de LM es una extensión de LFT. Podríamos haber comenzado con LPO, lo que nos habría dado Lógica Modal Cuantificada (LMC). LMC es mucho más poderoso que LM, pero también es mucho, mucho más complicado. Así que vamos a mantener las cosas simples, y comenzar con LFT.

Al igual que LFT, LM comienza con un stock infinito de \emph{átomos}. Estos se escriben como letras mayúsculas, con o sin subíndices numéricos: $A$, $B$, \dots $A_1$, $B_1$, \dots Tomamos entonces todas las reglas sobre cómo hacer oraciones de LFT, y añadimos dos más para $\ebox$ y~$\ediamond$:
\factoidbox{
\begin{compactlist}[labelindent=0pt,leftmargin=*]
    \item Cada átomo de LM es una oración de LM.
    \item Si $\metav{A}$ es una oración de LM, entonces $\enot\metav{A}$ es una oración de LM.
    \item Si $\metav{A}$ y $\metav{B}$ son oraciones de LM, entonces $(\metav{A}\eand\metav{B})$ es una oración de LM.
    \item Si $\metav{A}$ y $\metav{B}$ son oraciones de LM, entonces $(\metav{A}\eor\metav{B})$ es una oración de LM.
    \item Si $\metav{A}$ y $\metav{B}$ son oraciones de LM, entonces $(\metav{A}\eif\metav{B})$ es una oración de LM.
    \item Si $\metav{A}$ y $\metav{B}$ son oraciones de LM, entonces $(\metav{A}\eiff\metav{B})$ es una oración de LM.
    \item Si $\metav{A}$ es una oración de LM, entonces $\ebox\metav{A}$ es una oración de LM.
    \item Si $\metav{A}$ es una oración de LM, entonces $\ediamond\metav{A}$ es una oración de LM.
    \item Nada más es una oración de LM.
\end{compactlist}}
Aquí hay algunos ejemplos de oraciones de LM:
\begin{align*}
	& A\\
	& P\eor Q\\
	& \ebox A\\
	& C\eor \ebox D\\
	& \ebox\ebox (A\eif R)\\
	& \ebox\ediamond (S\eand (Z\eiff (\ebox W \eor \ediamond Q)))
\end{align*}

\chapter{Deducción natural para LM}
\label{Proof}

Ahora que sabemos cómo hacer oraciones en LM, podemos ver cómo \emph{probar} cosas en LM. Usaremos $\proves$ para expresar la demostrabilidad.  Así, $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n \proves \metav{C}$ significa que $\metav{C}$ se puede probar a partir de $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n$. Sin embargo, estaremos viendo varios sistemas diferentes de LM, por lo que será útil agregar un subíndice para indicar con qué sistema estamos trabajando. Entonces, por ejemplo, si queremos decir que podemos probar $\metav{C}$ a partir de $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n$ \emph{en el sistema}~\mlK, escribiremos: $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n \proves_\mlK \metav{C}$.

\section{Sistema \mlK}
\label{K}

Comenzamos con un sistema particularmente simple llamado \mlK, en honor al filósofo y lógico Saul Kripke. \mlK{} incluye todas las reglas de deducción natural de LFT, incluidas las reglas derivadas y las básicas. \mlK{} luego agrega un tipo especial de subprueba, más dos nuevas reglas básicas para \ebox.

El tipo especial de subprueba se parece a una subprueba ordinaria, excepto que tiene un~\ebox en su línea de suposición en lugar de una fórmula. Las llamamos \emph{subpruebas estrictas}: nos permiten razonar y probar cosas sobre posibilidades alternativas. Lo que podemos probar dentro de una subprueba estricta se cumple en cualquier posibilidad alternativa, en particular, en posibilidades alternativas donde las suposiciones vigentes en nuestra prueba pueden no cumplirse. En las subpruebas estrictas, todas las suposiciones se ignoran y no se nos permite apelar a ninguna línea fuera de la subprueba estricta (excepto según lo permitido por las reglas modales dadas a continuación).

La regla \ebox I nos permite derivar una fórmula $\ebox \metav{A}$ si podemos derivar $\metav{A}$ dentro de una subprueba estricta.  Es nuestro método fundamental para introducir \ebox{} en las pruebas. La idea básica es bastante simple: si $\metav{A}$ es un teorema, entonces $\ebox \metav{A}$ también debería ser un teorema. (Recuerda que llamar a $\metav{A}$ un teorema es decir que podemos probar $\metav{A}$ sin depender de ninguna suposición no descargada).

Supongamos que quisiéramos probar $\ebox(A\eif A)$. Lo primero que debemos hacer es probar que $A\eif A$ es un teorema. Ya sabes cómo hacer eso usando LFT. Simplemente presentas una prueba de $A\eif A$ que no comienza con ninguna premisa, como esta:
\begin{fitchproof}
		\open
		\hypo{1}{A}\AS
		\have{2}{A}\by{R}{1}
		\close
		\have{3}{A\eif A}\ci{1-2}
\end{fitchproof}
Pero para aplicar \ebox I, necesitamos haber probado la fórmula dentro de una subprueba estricta. Dado que nuestra prueba de $A \eif A$ no hace uso de ninguna suposición, esto es posible.
\begin{fitchproof}
		\open
		\hypo{1}{\ebox}\AS
		\open
		\hypo{2}{A}\AS
		\have{3}{A}\by{R}{2}
		\close
		\have{4}{A\eif A}\ci{2-3}
		\close
		\have{5}{\ebox(A\eif A)}\boxi{1-4}
\end{fitchproof}

\factoidbox{
	\begin{fitchproof}
			\open
			\hypo[m]{m}{\ebox}\AS
			\have[n]{n}{\metav{A}}
			\close
			\have[\,]{o}{\ebox\metav{A}}\boxi{m-n}
	\end{fitchproof}
	Ninguna línea por encima de la línea $m$ puede ser citada por ninguna regla dentro de la subprueba estricta iniciada en la línea $m$ a menos que la regla lo permita explícitamente.
}
Es esencial enfatizar que en una subprueba estricta no se puede usar ninguna regla que apele a algo que probaste fuera de la subprueba estricta. Hay excepciones, por ejemplo, la regla \ebox E a continuación. Estas reglas indicarán explícitamente que pueden usarse dentro de subpruebas estrictas y citar líneas fuera de la subprueba estricta. Esta restricción es esencial, de lo contrario obtendríamos resultados terribles. Por ejemplo, podríamos proporcionar la siguiente prueba para justificar $A\therefore \ebox A$:
\begin{fitchproof}
		\hypo{1}{A}\PR
		\open
		\hypo{2}{\ebox}\AS
		\have{3}{A}\by{uso incorrecto de R}{1}
		\close
		\have{4}{\ebox A}\boxi{2-3}
\end{fitchproof}
Esta no es una prueba legítima, porque en la línea 3 apelamos a la línea 1, aunque la línea 1 viene antes del comienzo de la subprueba estricta en la línea 2.

Dijimos anteriormente que una subprueba estricta nos permite razonar sobre situaciones posibles alternativas arbitrarias. Lo que se puede probar en una subprueba estricta se cumple en todas las situaciones posibles alternativas, y por lo tanto es necesario. Esta es la idea detrás de la regla \ebox I. Por otro lado, si hemos asumido que algo es necesario, hemos asumido con ello que es verdadero en todas las situaciones posibles alternativas.  Por lo tanto, tenemos la regla \ebox E:

\factoidbox{
	\begin{fitchproof}
			\have[m]{m}{\ebox\metav{A}}
			\open
			\hypo[\ ]{o}{\ebox}\AS
			\have[n]{n}{\metav{A}}\boxe{m}
			\close
		\end{fitchproof}
		\ebox E solo se puede aplicar si la línea $m$ (que contiene $\ebox A$) se encuentra \emph{fuera} de la subprueba estricta en la que cae la línea $n$, y esta subprueba estricta no es en sí misma parte de una subprueba estricta que no contenga~$m$.
		}
\ebox E te permite afirmar $\metav{A}$ dentro de una subprueba estricta si tienes $\ebox \metav{A}$ fuera de la subprueba estricta. La restricción significa que solo puedes hacer esto en la primera subprueba estricta, no puedes aplicar la regla \ebox E dentro de una subprueba estricta anidada. Entonces, lo siguiente no está permitido:
\begin{fitchproof}
	\have{1}{\ebox\metav{A}}
	\open
	\hypo{2}{\ebox}\AS
	\open
	\hypo{3}{\ebox}\AS
	\have{4}{\metav{A}}\by{uso incorrecto de \ebox E}{1}
\close\close
\end{fitchproof}
El uso incorrecto de \ebox E en la línea~$4$ viola la condición, porque aunque la línea~$1$ se encuentra fuera de la subprueba estricta en la que cae la línea~$4$, la subprueba estricta que contiene la línea~$4$ se encuentra dentro de la subprueba estricta que comienza en la línea~$2$ que no contiene la línea~$1$.

Comencemos con un ejemplo.
\begin{fitchproof}
		\hypo{1}{\ebox A}\PR
		\hypo{2}{\ebox B}\PR
		\open
		\hypo{3}{\ebox}\AS
		\have{4}{A}\boxe{1}
		\have{5}{B}\boxe{2}
		\have{6}{A \eand B}\ai{4,5}
		\close
		\have{6}{\ebox(A \land B)}\boxi{3-6}
\end{fitchproof}
También podemos mezclar subpruebas regulares y subpruebas estrictas:
\begin{fitchproof}
		\hypo{1}{\ebox (A \eif B)}\PR
		\open
		\hypo{2}{\ebox A}\AS
		\open
		\hypo{3}{\ebox}\AS
		\have{4}{A}\boxe{2}
		\have{5}{A \eif B}\boxe{1}
		\have{6}{B}\ce{4,5}
		\close
		\have{7}{\ebox B}\boxi{3-6}
		\close
		\have{8}{\ebox A \eif \ebox B} \ci{2-7}
\end{fitchproof}
Esto se llama la \emph{Regla de Distribución}, porque nos dice que $\ebox$ 'distribuye' sobre $\eif$.

Las reglas \ebox I y \ebox E parecen bastante simples, \textexclamdown y de hecho \mlK{} es un sistema muy simple! Pero \mlK{} es más poderoso de lo que podrías haber pensado. Puedes probar bastantes cosas en él.

\section{Posibilidad}
\label{possibility}

En la última subsección, vimos todas las reglas básicas para \mlK. Pero podrías haber notado que todas estas reglas eran sobre necesidad, $\ebox$, y ninguna de ellas era sobre posibilidad, $\ediamond$. Eso es porque podemos \emph{definir} la posibilidad en términos de necesidad:
\factoidbox{
$\ediamond\metav{A}=_{df} \enot \ebox\enot \metav{A}$
}
En otras palabras, decir que $\metav{A}$ es \emph{posiblemente verdadero}, es decir que $\metav{A}$ \emph{no es necesariamente falso}. Como resultado, no es realmente esencial agregar un $\ediamond$, un símbolo especial para la posibilidad, en el sistema \mlK. Aún así, el sistema será \emph{mucho} más fácil de usar si lo hacemos, y por lo tanto agregaremos las siguientes reglas definitorias:
\factoidbox{
	\begin{fitchproof}
			\have[m]{m}{\enot\ebox\enot \metav{A}}
			\have[\, ]{n}{\ediamond \metav{A}}\diadf{m}
	\end{fitchproof}
	\begin{fitchproof}
			\have[m]{m}{\ediamond \metav{A}}
			\have[\, ]{n}{\enot\ebox\enot \metav{A}}\diadf{m}
	\end{fitchproof}
}
Es importante que no pienses en estas reglas como una adición real a \mlK: simplemente registran la forma en que $\ediamond$ se define en términos de $\ebox$.

Si quisiéramos, podríamos dejar nuestras reglas para \mlK{} aquí. Pero será útil agregar algunas reglas de \emph{Conversión Modal}, que nos dan algunas formas más de alternar entre $\ebox$ y $\ediamond$:
\factoidbox{
	\begin{fitchproof}
			\have[m]{m}{\enot\ebox \metav{A}}
			\have[\, ]{n}{\ediamond \enot\metav{A}}\mc{m}
	\end{fitchproof}
	\begin{fitchproof}
			\have[m]{m}{\ediamond \enot \metav{A}}
			\have[\, ]{n}{\enot\ebox \metav{A}}\mc{m}
	\end{fitchproof}
	\begin{fitchproof}
			\have[m]{m}{\enot\ediamond \metav{A}}
			\have[\, ]{n}{\ebox \enot\metav{A}}\mc{m}
	\end{fitchproof}
	\begin{fitchproof}
			\have[m]{m}{\ebox\enot \metav{A}}
			\have[\, ]{n}{\enot\ediamond\metav{A}}\mc{m}
	\end{fitchproof}
}
Estas Reglas de Conversión Modal tampoco son una adición al poder de \mlK, porque pueden derivarse de las reglas básicas, junto con la definición de $\ediamond$.

En el sistema \mlK, usando Def\ediamond{} (o las reglas de conversión modal), se puede probar $\ediamond A \eiff \enot\ebox\enot A$. Al diseñar el sistema \mlK, comenzamos con $\ebox$ como nuestro símbolo modal primitivo, y luego definimos $\ediamond$ en términos de él. Pero si hubiéramos preferido, podríamos haber comenzado con $\ediamond$ como nuestro primitivo, y luego definido $\ebox$ de la siguiente manera: $\ebox\metav{A} =_{df} \enot \ediamond \enot \metav{A}$. No hay, entonces, ningún sentido en que la necesidad sea de alguna manera más \emph{fundamental} que la posibilidad. La necesidad y la posibilidad son exactamente tan fundamentales como la otra.

\section{Sistema \mlT}
\label{T}

Hasta ahora nos hemos centrado en \mlK, que es un sistema modal muy simple. \mlK{} es tan débil que ni siquiera te permitirá probar $\metav{A}$ a partir de $\ebox\metav{A}$. Pero si estamos pensando en $\ebox$ como expresión de \emph{necesidad}, entonces querremos poder hacer esta inferencia: si $\metav{A}$ es \emph{necesariamente verdadero}, \textexclamdown entonces seguramente debe ser \emph{verdadero}!

Esto nos lleva a un nuevo sistema, \mlT, que obtenemos agregando la siguiente regla a \mlK:
\factoidbox{
	\begin{fitchproof}
			\have[m]{m}{\ebox \metav{A}}
			\have[n]{n}{\metav{A}}\rt{m}
	\end{fitchproof}
	La línea $n$ en la que se aplica la regla R\mlT{} \emph{no} debe estar en una subprueba estricta que comience después de la línea~$m$.
}

La restricción en la regla \mlT{} es en cierto modo lo opuesto a la restricción en \ebox E: solo puedes usar \ebox E en una subprueba estricta anidada, pero no puedes usar \mlT{} en una subprueba estricta anidada.

Podemos probar cosas en \mlT{} que no podíamos probar en \mlK, por ejemplo, $\ebox A \eif A$.
\section{Sistema \mlSfour}
\label{S4}

\mlT{} te permite eliminar las cajas de necesidad: de $\ebox \metav{A}$, puedes inferir $\metav{A}$. Pero, \textexclamdown y si quisiéramos agregar cajas adicionales? Es decir, \textexclamdown y si quisiéramos pasar de $\ebox\metav{A}$ a $\ebox\ebox\metav{A}$? Bueno, eso no sería un problema, si hubiéramos probado $\ebox\metav{A}$ aplicando \ebox I a una subprueba estricta de $\metav{A}$ que a su vez no usa \ebox E. En ese caso, $\metav{A}$ es una tautología, y al anidar la subprueba estricta dentro de otra subprueba estricta y aplicar \ebox I nuevamente, podemos probar $\ebox\ebox \metav{A}$. Por ejemplo, podríamos probar $\ebox\ebox (P\eif P)$ así:
\begin{fitchproof}
		\open
		\hypo{1}{\ebox}\AS
		\open
		\hypo{2}{\ebox}\AS
		\open
		\hypo{3}{P}\AS
		\have{4}{P}\by{R}{3}
		\close
		\have{5}{P\eif P}\ci{3-4}
		\close
		\have{6}{\ebox(P\eif P)}\boxi{2-5}
		\close
		\have{7}{\ebox\ebox(P\eif P)}\boxi{1-6}
\end{fitchproof}
Pero, \textexclamdown y si no probamos $\ebox\metav{A}$ de esta manera restringida, sino que usamos \ebox E dentro de la subprueba estricta de $\metav{A}$? Si ponemos esa subprueba estricta dentro de otra subprueba estricta, se viola el requisito de la regla \ebox E de no citar una línea que contenga $\ebox\metav{A}$ que se encuentre en otra subprueba estricta que aún no haya concluido. \textexclamdown O qué pasa si $\ebox\metav{A}$ fuera solo una suposición con la que comenzamos nuestra prueba? \textexclamdown Podríamos inferir $\ebox\ebox\metav{A}$ entonces? No en \mlT, no podríamos. Y esto bien podría parecerte una limitación de \mlT, al menos si leemos $\ebox$ como expresión de \emph{necesidad}. Parece intuitivo que si $\metav{A}$ es necesariamente verdadero, entonces no podría haber \emph{fallado} en ser necesariamente verdadero.

Esto nos lleva a otro nuevo sistema, \mlSfour, que obtenemos agregando la siguiente regla a~\mlT:
\factoidbox{
	\begin{fitchproof}
			\have[m]{m}{\ebox\metav{A}}
			\open
			\hypo[\ ]{k}{\ebox}\AS
			\have[n]{n}{\ebox\metav{A}}\rfour{m}
			\close
	\end{fitchproof}
	Ten en cuenta que R$\mathbf{4}$ solo se puede aplicar si la línea $m$ (que contiene $\ebox A$) se encuentra fuera de la subprueba estricta en la que cae la línea $n$, y esta subprueba estricta no es en sí misma parte de una subprueba estricta que no contenga~$m$.
}

La regla R$\mathbf{4}$ se parece a {\ebox}E, excepto que en lugar de producir $\metav{A}$ a partir de $\ebox\metav{A}$, produce $\ebox\metav{A}$ dentro de una subprueba estricta. La restricción es la misma, sin embargo: R$\mathbf{4}$ nos permite ``importar'' $\ebox \metav{A}$ a una subprueba estricta, pero no a una subprueba estricta anidada dentro de una subprueba estricta. Sin embargo, si eso es necesario, una aplicación adicional de R$\mathbf{4}$ tendría el mismo resultado.

Ahora podemos probar aún más resultados. Por ejemplo:
\begin{fitchproof}
	\open
	\hypo{1}{\ebox A}\AS
	\open
	\hypo{2}{\ebox}\AS
	\have{3}{\ebox A}\rfour{1}
	\close
	\have{4}{\ebox\ebox A}\boxi{2-3}
	\close
	\have{5}{\ebox A \eif \ebox\ebox A}\ci{1-6}
\end{fitchproof}
De manera similar, podemos probar $\ediamond\ediamond A \eif \ediamond A$. Esto nos muestra que, además de permitirnos \emph{agregar} cajas adicionales, \mlSfour{} nos permite \emph{eliminar} diamantes adicionales: de $\ediamond\ediamond \metav{A}$, siempre puedes inferir $\ediamond\metav{A}$.

\section{Sistema \mlSfive}
\label{S5}

En \mlSfour, siempre podemos agregar una caja delante de otra caja. Pero \mlSfour{} no nos permite automáticamente agregar una caja delante de un \emph{diamante}. Es decir, \mlSfour{} generalmente no permite la inferencia de $\ediamond\metav{A}$ a $\ebox\ediamond\metav{A}$. Pero nuevamente, eso podría parecerte una deficiencia, al menos si estás leyendo $\ebox$ y $\ediamond$ como expresión de \emph{necesidad} y \emph{posibilidad}. Parece intuitivo que si $\metav{A}$ es posiblemente verdadero, entonces no podría haber \emph{fallado} en ser posiblemente verdadero.

Esto nos lleva a nuestro sistema modal final, \mlSfive, que obtenemos agregando la siguiente regla a \mlSfour:
\factoidbox{
	\begin{fitchproof}
			\have[m]{m}{\enot \ebox\metav{A}}
			\open
			\hypo[\ ]{k}{\ebox}\AS
			\have[n]{n}{\enot\ebox\metav{A}}\rfive{m}
			\close
	\end{fitchproof}
	La regla R$\mathbf{5}$ solo se puede aplicar si la línea $m$ (que contiene $\enot \ebox\metav{A}$) se encuentra fuera de la subprueba estricta en la que cae la línea $n$, y esta subprueba estricta no es en sí misma parte de una subprueba estricta que no contenga la línea~$m$.
}

Esta regla nos permite mostrar, por ejemplo, que $\ediamond\ebox A\proves_\mlSfive \ebox A$:
\begin{fitchproof}
	\hypo{1}{\ediamond\ebox A}\PR
	\have{2}{\enot\ebox\enot\ebox A}\by{Def\ediamond}{1}
	\open
	\hypo{3}{\enot \ebox A}\AS
	\open
	\hypo{4}{\ebox}\AS
	\have{5}{\enot\ebox A}\rfive{3}
	\close
	\have{6}{\ebox\enot\ebox A}\boxi{4-5}
	\have{7}{\ered}\ne{2,6}
	\close
	\have{8}{\ebox A}\by{IP}{3-7}
\end{fitchproof}

Entonces, además de agregar cajas delante de diamantes, también podemos eliminar diamantes delante de cajas.

Obtuvimos \mlSfive{} agregando la regla~R$\mathbf{5}$ a~\mlSfour. De hecho, podríamos haber agregado la regla~R$\mathbf{5}$ a \mlT{}, omitido la regla~R$\mathbf{4}$ y obtenido un sistema equivalente. Eso es porque todo lo que podemos probar usando la regla~R$\mathbf{4}$ también se puede probar usando R\mlT{} junto con~R$\mathbf{5}$. Por ejemplo, aquí hay una prueba que muestra $\ebox A \proves_\mlSfive \ebox\ebox A$ sin usar~R$\mathbf{4}$:
\begin{fitchproof}
	\hypo{1}{\ebox A}\PR
	\open
	\hypo{2}{\ebox\enot\ebox A}\AS
	\have{3}{\enot\ebox A}\rt{2}
	\have{4}{\ered}\ne{1,3}
	\close
	\have{5}{\enot\ebox\enot\ebox A}\ni{2-4}
	\open
	\hypo{6}{\ebox}\AS
	\open
	\hypo{7}{\enot\ebox A}\AS
	\open
	\hypo{8}{\ebox}\AS
	\have{9}{\enot\ebox A}\rfive{7}
	\close
	\have{10}{\ebox \enot\ebox A}\boxi{8-9}
	\have{11}{\enot\ebox\enot\ebox A}\rfive{5}
	\have{12}{\ered}\ne{10,11}
	\close
	\have{13}{\ebox A}\ip{7-12}
	\close
	\have{14}{\ebox\ebox A}\boxi{6-13}
\end{fitchproof}
\mlSfive{} es \emph{estrictamente más fuerte} que \mlSfour: hay cosas que se pueden probar en \mlSfive, pero no en \mlSfour{} (por ejemplo, $\ediamond\ebox A \eif \ebox A$).

El punto importante sobre \mlSfive{} se puede expresar así: si tienes una larga cadena de cajas y diamantes, en cualquier combinación, puedes eliminar todos menos el último de ellos. Entonces, por ejemplo, $\ediamond\ebox\ediamond\ediamond\ebox\ebox\ediamond\ebox A$ se puede simplificar a solo $\ebox A$.

\practiceproblems

\problempart
Proporciona pruebas para lo siguiente:
\begin{compactlist}
	\item $\ebox (A\eand B)\proves_\mlK\ebox A \eand \ebox B$
	\item $\ebox A\eand\ebox B\proves_\mlK\ebox( A \eand B)$
	\item $\ebox A\eor\ebox B\proves_\mlK\ebox( A \eor B)$
	\item $\ebox (A \eiff B)\proves_\mlK \ebox A \eiff \ebox B$
\end{compactlist}

\problempart
Proporciona pruebas para lo siguiente (\textexclamdown sin usar Conversión Modal!):
\begin{compactlist}
	\item $\enot\ebox A\proves_\mlK \ediamond \enot A$
	\item $\ediamond\enot A\proves_\mlK\enot \ebox A$
	\item $\enot\ediamond A\proves_\mlK\ebox\enot A$
	\item $\ebox\enot A\proves_\mlK\enot\ediamond A$
\end{compactlist}

\problempart
Proporciona pruebas de lo siguiente (\textexclamdown y ahora siéntete libre de usar Conversión Modal!):
\begin{compactlist}
	\item $\ebox(A\eif B), \ediamond A \proves_\mlK \ediamond B$
	\item $\ebox A \proves_\mlK \enot\ediamond\enot A$
	\item $\enot\ediamond\enot A \proves_\mlK \ebox A$
\end{compactlist}

\problempart
Proporciona pruebas para lo siguiente:
\begin{compactlist}
	\item $P\proves_\mlT\ediamond P$
	\item $\proves_\mlT (A\eand B)\eor(\enot \ebox A\eor\enot\ebox B)$
\end{compactlist}

\problempart
Entregue una prueba para lo siguiente:
\begin{compactlist}
	\item $\ebox(\ebox A\eif B), \ebox (\ebox B\eif C), \ebox A \proves_\mlSfour \ebox\ebox C$
	\item $\ebox A \proves_\mlSfour \ebox(\ebox A \eor B)$
	\item $\ediamond \ediamond A \proves_\mlSfour \ediamond A$
\end{compactlist}


\problempart
Entregue pruebas en \mlSfive{} para los siguientes:
\begin{compactlist}
	\item $\enot\ebox\enot A, \ediamond B\proves_\mlSfive \ebox(\ediamond A \eand \ediamond B)$
	\item $A \proves_\mlSfive  \ebox\ediamond A$
	\item $\ediamond\ediamond A\proves_\mlSfive  \ediamond A$
\end{compactlist}

\chapter{Semántica para LM}
\label{Semantics}

Hasta ahora, nos hemos centrado en presentar varios sistemas de Deducción Natural para LM. Ahora veremos la \emph{semántica} para LM. Una semántica para un lenguaje es un método para asignar valores de verdad a las oraciones en ese lenguaje. Entonces, una semántica para LM es un método para asignar valores de verdad a las oraciones de LM.

\section{Interpretaciones de LM}

La gran idea detrás de la semántica para LM es esta. En LM, las oraciones no son simplemente verdaderas o falsas, punto final. Una oración es verdadera o falsa \emph{en un mundo posible dado}, y una sola oración bien puede ser verdadera en algunos mundos y falsa en otros. Luego decimos que $\ebox \metav{A}$ es verdadero si y solo si $\metav{A}$ es verdadero en \emph{todos} los mundos, y $\ediamond\metav{A}$ es verdadero si y solo si $\metav{A}$ es verdadero en \emph{algún} mundo.

Esa es la gran idea, pero necesitamos refinarla y hacerla más precisa. Para hacer esto, necesitamos introducir la idea de una \emph{interpretación} de LM. Lo primero que necesitas incluir en una interpretación es una colección de \emph{mundos posibles}. Ahora, en este punto podrías querer preguntar: \textexclamdown Qué es exactamente un mundo posible? La idea intuitiva es que un mundo posible es otra forma en que este mundo podría haber sido. Pero, \textexclamdown qué significa exactamente eso? Esta es una excelente pregunta filosófica, y la veremos con mucho detalle más adelante. Pero no necesitamos preocuparnos demasiado por eso ahora mismo. En lo que respecta a la lógica formal, los mundos posibles pueden ser cualquier cosa que quieras. Todo lo que importa es que proporciones a cada interpretación una colección no vacía de cosas etiquetadas como \define{mundos posibles}.

Una vez que hayas elegido tu colección de mundos posibles, necesitas encontrar alguna forma de determinar qué oraciones de LM son verdaderas en qué mundos posibles. Para hacer eso, necesitamos introducir la noción de una \emph{función de valoración}. Aquellos de ustedes que hayan estudiado algo de matemáticas ya estarán familiarizados con la idea general de una función. Pero para aquellos de ustedes que no lo hayan hecho, una función es una entidad matemática que mapea argumentos a valores. Eso podría sonar un poco abstracto, pero algunos ejemplos familiares ayudarán. Toma la función $x+1$. Esta es una función que toma un número como argumento y luego escupe el siguiente número como valor. Entonces, si introduces el número $1$ como argumento, la función $x+1$ escupirá el número $2$ como valor; si introduces $2$, escupirá $3$; si introduces $3$, escupirá $4$ \dots O aquí hay otro ejemplo: la función $x+y$. Esta vez, tienes que introducir dos argumentos en esta función si quieres que devuelva un valor: si introduces $2$ y $3$ como tus argumentos, escupe $5$; si introduces $1003$ y $2005$, escupe $3008$; y así sucesivamente.

Una función de valuación para la lógica modal (LM) toma una oración y un mundo como sus argumentos, y luego devuelve un valor de verdad como su valor. Entonces, si $\nu$ es una función de valuación y $w$ es un mundo posible, $\nu_w(\metav{A})$ es cualquier valor de verdad al que $\nu$ mapea $\metav{A}$ y $w$: si $\nu_w(\metav{A})=F$, entonces $\metav{A}$ es falsa en el mundo $w$ según la valuación $\nu$; si $\nu_w(\metav{A})=T$, entonces $\metav{A}$ es verdadera en el mundo $w$ según la valuación $\nu$.

Se permite que estas funciones de valuación mapeen cualquier oración \emph{atómica} a cualquier valor de verdad en cualquier mundo. Pero hay reglas sobre qué valores de verdad se asignan a las oraciones más complejas en un mundo. Aquí están las reglas para los conectivos de Lógica Formal Traducción (LFT):
\begin{compactlist}
	\item $\nu_w(\enot\metav{A})=T$ si y solo si $\nu_w(\metav{A})=F$
	\item $\nu_w(\metav{A}\eand\metav{B})=T$ si y solo si $\nu_w(\metav{A})=T$ y $\nu_w(\metav{B})=T$
	\item $\nu_w(\metav{A}\eor\metav{B})=T$ si y solo si $\nu_w(\metav{A})=T$ o $\nu_w(\metav{B})=T$, o ambas
	\item $\nu_w(\metav{A}\eif\metav{B})=T$ si y solo si $\nu_w(\metav{A})=F$ o $\nu_w(\metav{B})=T$, o ambas
	\item $\nu_w(\metav{A}\eiff\metav{B})=T$ si y solo si $\nu_w(\metav{A})=T$ y $\nu_w(\metav{B})=T$, o $\nu_w(\metav{A})=F$ y $\nu_w(\metav{B})=F$
\end{compactlist}
Hasta ahora, estas reglas deberían parecer muy familiares. Esencialmente, todas funcionan exactamente como las tablas de verdad de LFT. La única diferencia es que estas reglas de tablas de verdad tienen que aplicarse una y otra vez, a un mundo a la vez.

Pero, \textexclamdown cuáles son las reglas para los nuevos operadores modales, $\ebox$ y $\ediamond$? La idea más obvia sería dar reglas como estas:
\begin{itemize}
	\item $\nu_w(\ebox \metav{A})=T$ si y solo si $\forall w' (\nu_{w'}(\metav{A})=T)$
	\item $\nu_w(\ediamond \metav{A})=T$ si y solo si $\exists w' (\nu_{w'}(\metav{A})=T)$
\end{itemize}
Esta es solo la forma formal elegante de escribir la idea de que $\ebox\metav{A}$ es verdadera en $w$ si y solo si $\metav{A}$ es verdadera en \emph{todos} los mundos, y $\ediamond\metav{A}$ es verdadera en $w$ si y solo si $\metav{A}$ es verdadera en \emph{algún} mundo.

Sin embargo, aunque estas reglas son agradables y simples, resulta que no son tan útiles como nos gustaría. Como mencionamos, LM está destinado a ser una herramienta muy flexible. Está destinado a ser un marco general para tratar con muchos tipos diferentes de necesidad. Como resultado, queremos que nuestras reglas semánticas para $\ebox$ y $\ediamond$ sean un poco menos rígidas. Podemos hacer esto introduciendo otra nueva idea: \emph{relaciones de accesibilidad}.

Una relación de accesibilidad, $R$, es una relación entre mundos posibles. Aproximadamente, decir que $Rw_1w_2$ (en español: el mundo $w_1$ \emph{accede} al mundo $w_2$) es decir que $w_2$ es posible \emph{relativo a} $w_1$. En otras palabras, al introducir relaciones de accesibilidad, abrimos la idea de que un mundo dado podría ser posible relativo a algunos mundos pero no a otros. Esto resulta ser una idea \emph{muy} fructífera al estudiar sistemas modales. Ahora podemos dar las siguientes reglas semánticas para $\ebox$ y $\ediamond$:
\begin{compactlist}[resume]
	\item $\nu_{w_1}(\ebox \metav{A})=T$ si y solo si $\forall w_2 (Rw_1w_2\eif \nu_{w_2}(\metav{A})=T)$
	\item $\nu_{w_1}(\ediamond \metav{A})=T$ si y solo si $\exists w_2 (Rw_1w_2\eand \nu_{w_2}(\metav{A})=T)$
\end{compactlist}
O en español sencillo: $\ebox\metav{A}$ es verdadera en el mundo $w_1$ si y solo si $\metav{A}$ es verdadera en todos los mundos que son posibles relativos a $w_1$; y $\ediamond\metav{A}$ es verdadera en el mundo $w_1$ si y solo si $\metav{A}$ es verdadera en algún mundo que es posible relativo a $w_1$.

Entonces, ahí lo tenemos. Una interpretación para LM consta de tres cosas: una colección de mundos posibles, $W$; una relación de accesibilidad, $R$; y una función de valuación, $\nu$. La colección de ``mundos posibles'' realmente puede ser una colección de cualquier cosa que quieras. Realmente no importa, siempre y cuando $W$ no esté vacío. (Para muchos propósitos, es útil simplemente tomar una colección de números como tu colección de mundos). Y por ahora, al menos, $R$ puede ser cualquier relación entre los mundos en $W$ que quieras. Podría ser una relación que cada mundo en $W$ tiene con cada mundo en $W$, o una que ningún mundo tiene con ningún mundo, o cualquier cosa intermedia. Y por último, $\nu$ puede mapear cualquier oración atómica de LM a cualquier valor de verdad en cualquier mundo. Todo lo que importa es que siga las reglas (1)-(7) cuando se trata de las oraciones más complejas.

Veamos un ejemplo. A menudo es útil presentar interpretaciones de LM como diagramas, como este:
\begin{center}
	\begin{arialabel}{Los números 1 y 2 están conectados por flechas. Hay flechas de 1 a sí mismo, y de 2 a 1. El nodo 1 está etiquetado con A y no con B. El nodo 2 está etiquetado por no-A y B.}
	\begin{tikzpicture}
		\node (atom1) at (0,1) {1};
		\node (atom2) at (3,1) {2};
		\node (atom3) at (-0.25,0) {$A$};
		\node (atom4) at (3,0) {$\enot A$};
		\node (atom5) at (-0.25,-0.7) {$\enot B$};
		\node (atom6) at (3,-0.7) {$B$};
		\draw[->, thick] (atom1)+(-0.15,0.15) arc (-330:-30:.3);
		%\draw[->, thick] (atom2)+(0.15,-0.15) arc (-150:150:.3); 
		\draw[<-, thick] (atom1) -- (atom2);
		\draw (-0.8,-1.2) rectangle (0.4,0.5);
		\draw (2.4,-1.2) rectangle (3.6,0.5);
	\end{tikzpicture}
\end{arialabel}
\end{center}
Aquí se explica cómo leer la interpretación de este diagrama. Contiene solo dos mundos, 1 y 2. Las flechas entre los mundos indican la relación de accesibilidad. Entonces, 1 y 2 acceden a 1, pero ni 1 ni 2 acceden a 2. Las cajas en cada mundo nos permiten saber qué oraciones atómicas son verdaderas en cada mundo: $A$ es verdadera en 1 pero falsa en 2; $B$ es falsa en 1 pero verdadera en 2. Solo puedes escribir una oración atómica o la negación de una oración atómica en una de estas cajas. Podemos averiguar qué valores de verdad obtienen las oraciones más complejas en cada mundo a partir de eso. Por ejemplo, en esta interpretación, todas las siguientes oraciones son verdaderas en $w_1$:
\[
A\eand\enot B,\qquad B\eif A,\qquad \ediamond A,\qquad \ebox\enot B
\]
Si no te gusta pensar en forma de diagrama, también puedes presentar una interpretación como ésta:
\begin{ekey}
	\item[W]$1,2$
	\item[R]$\langle 1,1\rangle, \langle 2,1\rangle$
	\item[\nu]$\nu_{1}(A)=T, \nu_{1}(B)=F, \nu_{2}(A)=F, \nu_{2}(B)=T$
\end{ekey}
Tendrás la oportunidad de cocinar algunas interpretaciones propias en breve, cuando empecemos a ver las \emph{contra-interpretaciones}.

\section{Una semántica para el sistema \mlK}
\label{SemanticsK}

Ahora podemos extender todos los conceptos semánticos de LFT para cubrir LM:
\factoidbox{
	\begin{factoiditems}
		\item $\metav{A}_1,\metav{A}_2, \dots
		\metav{A}_n\therefore\metav{C}$ es \define{modalmente v\'alido} si y solo si
		no hay ningún mundo en ninguna interpretación en el que
		$\metav{A}_1,\metav{A}_2, \dots \metav{A}_n$ sean todas verdaderas y
		$\metav{C}$ sea falsa.

		\item $\metav{A}$ es una \define{verdad modal} si y solo si $\metav{A}$
		es verdadera en cada mundo en cada interpretación.

		\item $\metav{A}$ es una \define{contradicci\'on modal} si y solo si
		$\metav{A}$ es falsa en cada mundo en cada interpretación.

		\item $\metav{A}$ es \define{modalmente satisfacible} si y solo si
		$\metav{A}$ es verdadera en algún mundo en alguna interpretación.
	\end{factoiditems}
		}
(De ahora en adelante, omitiremos las calificaciones explícitas ``modales'', ya que se pueden dar por sentadas).

También podemos extender nuestro uso de $\entails$. Sin embargo, necesitamos agregar subíndices nuevamente, tal como lo hicimos con $\proves$. Entonces, cuando queramos decir que $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\therefore\metav{C}$ es válido, escribiremos: $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\entails_\mlK\metav{C}$.

Obtengamos una mayor comprensión de esta semántica presentando algunas contra-interpretaciones. Consideremos la siguiente afirmación (falsa):
\[\enot A\entails_\mlK \enot \ediamond A\]
Para presentar una contra-interpretación a esta afirmación, necesitamos construir una interpretación que haga que $\enot A$ sea verdadera en algún mundo $w$, y que $\enot\ediamond A$ sea falsa en $w$. Aquí hay una de esas interpretaciones, presentada diagramáticamente:
\begin{center}
\begin{arialabel}{Los números 1 y 2 están conectados por una flecha de 1 a 2. El nodo 1 está etiquetado como no-A y el nodo 2 está etiquetado como A.}
	\begin{tikzpicture}
		\node (atom1) at (0,1) {1};
		\node (atom2) at (3,1) {2};
		\node (atom3) at (-0.25,0) {$\enot A$};
		\node (atom4) at (3,0) {$A$};
		\draw[->, thick] (atom1) -- (atom2);
		\draw (-0.8,-0.6) rectangle (0.4,0.5);
		\draw (2.4,-0.6) rectangle (3.6,0.5);
	\end{tikzpicture}
\end{arialabel}
\end{center}
Es fácil ver que esto funcionará como una contra-interpretación para nuestra afirmación. Primero, $\enot A$ es verdadera en el mundo $1$. Y segundo, $\enot\ediamond A$ es falsa en $1$: $A$ es verdadera en $2$, y $2$ es accesible desde $1$. Entonces, hay algún mundo en esta interpretación donde $\enot A$ es verdadera y $\enot\ediamond A$ es falsa, por lo que no es el caso que $\enot A\entails_\mlK\enot\ediamond A$.

\textexclamdown Por qué elegimos el subíndice \mlK? Bueno, resulta que hay una relación importante entre el sistema \mlK{} y la definición de validez que acabamos de dar. En particular, tenemos los siguientes dos resultados:
\begin{compactlist}
	\item Si $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\proves_\mlK\metav{C}$, entonces $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\entails_\mlK\metav{C}$
	\item Si $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\entails_\mlK\metav{C}$, entonces $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\proves_\mlK\metav{C}$
\end{compactlist}
El primer resultado se conoce como un resultado de \emph{solidez}, ya que nos dice que las reglas de \mlK{} son buenas, reglas sólidas: si puedes justificar un argumento dando una prueba para él usando el sistema \mlK, entonces ese argumento realmente es válido. El segundo resultado se conoce como un resultado de \emph{completitud}, ya que nos dice que las reglas de \mlK{} son lo suficientemente amplias para capturar todos los argumentos válidos: si un argumento es válido, entonces será posible ofrecer una prueba en \mlK{} que lo justifique.

Ahora, una cosa es declarar estos resultados, y otra muy distinta es demostrarlos. Sin embargo, no intentaremos demostrarlos aquí. Pero la idea detrás de la prueba de solidez quizás aclare cómo funcionan las subpruebas estrictas.

En una subprueba estricta, no se nos permite hacer uso de ninguna información fuera de la subprueba estricta, excepto lo que importamos a la subprueba estricta usando \ebox E. Si hemos asumido o probado $\ebox \metav{A}$, por \ebox E, podemos usar $\metav{A}$ dentro de una subprueba estricta. Y en \mlK, esa es la única forma de importar una fórmula a una subprueba estricta. Entonces, todo lo que se puede probar dentro de una subprueba estricta debe seguir de las fórmulas $\metav{A}$ donde fuera de la subprueba estricta tenemos $\ebox \metav{A}$. Imaginemos que estamos razonando sobre lo que es verdadero en un mundo posible en alguna interpretación. Si sabemos que $\ebox\metav{A}$ es verdadero en ese mundo posible, sabemos que $\metav{A}$ es verdadero en todos los mundos accesibles. Entonces, todo lo que se prueba dentro de una subprueba estricta es verdadero en todos los mundos posibles accesibles. Es por eso que \ebox I es una regla sólida.

\section{Una Semántica para el Sistema \mlT}
\label{SemanticsT}

Hace unos momentos, dijimos que el sistema \mlK{} es sólido y completo. \textexclamdown Dónde deja eso a los otros sistemas modales que vimos, a saber, \mlT, \mlSfour{} y \mlSfive? Bueno, todos son \emph{no sólidos}, en relación con la definición de validez que dimos anteriormente. Por ejemplo, todos estos sistemas nos permiten inferir $A$ de $\ebox A$, aunque $\ebox A\nentails_\mlK A$.

\textexclamdown Significa eso que estos sistemas son una pérdida de tiempo? \textexclamdown De ningún modo! Estos sistemas solo son no sólidos \emph{en relación con la definición de validez que dimos anteriormente}. (O para usar símbolos, son no sólidos en relación con $\entails_\mlK$.) Entonces, cuando estamos lidiando con estos sistemas modales más fuertes, solo necesitamos modificar nuestra definición de validez para que encaje. Aquí es donde las relaciones de accesibilidad resultan realmente útiles.

Cuando introdujimos la idea de una relación de accesibilidad, dijimos que podía ser cualquier relación entre mundos que quisieras: podrías hacer que relacionara cada mundo con cada mundo, ningún mundo con ningún mundo, o cualquier cosa intermedia. Así es como estábamos pensando en las relaciones de accesibilidad en nuestra definición de $\entails_\mlK$. Pero si quisiéramos, podríamos comenzar a poner algunas restricciones a la relación de accesibilidad. En particular, podríamos insistir en que tiene que ser \emph{reflexiva}:
\[\forall w\, Rww\]
En español: cada mundo se accede a sí mismo. O en términos de posibilidad relativa: cada mundo es posible relativo a sí mismo. Si impusiéramos esta restricción, podríamos introducir una nueva relación de consecuencia, $\entails_\mlT$, de la siguiente manera:
\factoidbox{
	$\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\entails_\mlT \metav{C}$ si y solo si no hay ningún mundo en ninguna interpretación \emph{que tenga una relación de accesibilidad reflexiva}, en el que $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n$ sean todas verdaderas y $\metav{C}$ sea falsa
}
Hemos adjuntado el subíndice \mlT{} a $\entails$ porque resulta que el sistema \mlT{} es sólido y completo con respecto a esta nueva definición de validez:
\begin{compactlist}
	\item Si $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\proves_\mlT\metav{C}$, entonces $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\entails_\mlT\metav{C}$
	\item Si $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\entails_\mlT\metav{C}$, entonces $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\proves_\mlT\metav{C}$
\end{compactlist}
Como antes, no intentaremos demostrar estos resultados de solidez y completitud. Sin embargo, es relativamente fácil ver cómo insistir en que la relación de accesibilidad debe ser reflexiva justificará la regla R\mlT{}:
\factoidbox{
	\begin{fitchproof}
			\have[m]{m}{\ebox \metav{A}}
			\have[\, ]{n}{\metav{A}}\rt{m}
	\end{fitchproof}
}
Para ver esto, simplemente imagina intentar construir una contra-interpretación a esta afirmación:
\[
	\ebox \metav{A}\entails_\mlT \metav{A}
\]
Necesitaríamos construir un mundo, $w$, en el que $\ebox \metav{A}$ fuera verdadero, pero $\metav{A}$ fuera falso. Ahora, si $\ebox \metav{A}$ es verdadero en $w$, entonces $\metav{A}$ debe ser verdadero en cada mundo al que $w$ accede. Pero como la relación de accesibilidad es reflexiva, $w$ accede a $w$. Entonces $\metav{A}$ debe ser verdadero en $w$. Pero ahora $\metav{A}$ debe ser verdadero \emph{y} falso en $w$. \textexclamdown Contradicción!

\section{Una Semántica para \mlSfour}
\label{SemanticsS4}

\textexclamdown De qué otra manera podríamos ajustar nuestra definición de validez? Bueno, también podríamos estipular que la relación de accesibilidad tiene que ser \emph{transitiva}:
\[\forall w_1\forall w_2\forall w_3 ((Rw_1w_2 \eand Rw_2w_3)\eif Rw_1w_3)\]
En español: si $w_1$ accede a $w_2$, y $w_2$ accede a $w_3$, entonces $w_1$ accede a $w_3$. O en términos de posibilidad relativa: si $w_3$ es posible relativo a $w_2$, y $w_2$ es posible relativo a $w_1$, entonces $w_3$ es posible relativo a $w_1$. Si agregáramos esta restricción a nuestra relación de accesibilidad, podríamos introducir una nueva relación de consecuencia, $\entails_\mlSfour$, de la siguiente manera:
\factoidbox{
	$\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\entails_\mlSfour \metav{C}$ si y solo si no hay ningún mundo en ninguna interpretación \emph{que tenga una relación de accesibilidad reflexiva y transitiva}, en el que $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n$ sean todas verdaderas y $\metav{C}$ sea falsa
}
Hemos adjuntado el subíndice \mlSfour{} a $\entails$ porque resulta que el sistema \mlSfour{} es sólido y completo con respecto a esta nueva definición de validez:
\begin{compactlist}
	\item Si $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\proves_\mlSfour\metav{C}$, entonces $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\entails_\mlSfour\metav{C}$
	\item Si $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\entails_\mlSfour\metav{C}$, entonces $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\proves_\mlSfour\metav{C}$
\end{compactlist}
Como antes, no intentaremos demostrar estos resultados de solidez y completitud. Sin embargo, es relativamente fácil ver cómo insistir en que la relación de accesibilidad debe ser transitiva justificará la regla \mlSfour{}:
\factoidbox{
	\begin{fitchproof}
			\have[m]{m}{\ebox\metav{A}}
			\open
			\hypo[\ ]{k}{\ebox}\AS
			\have[\ ]{n}{\ebox\metav{A}}\rfour{m}
	\end{fitchproof}
}
La idea detrás de las subpruebas estrictas, recuerda, es que son formas de probar cosas que deben ser verdaderas en todos los mundos accesibles. Entonces, la regla R$\mathbf{4}$ significa que siempre que $\ebox \metav{A}$ es verdadero, $\ebox \metav{A}$ también debe ser verdadero en cada mundo accesible. En otras palabras, debemos tener $\ebox\metav{A} \entails_\mlSfour \ebox\ebox\metav{A}$.

Para ver esto, simplemente imagina intentar construir una contra-interpretación a esta afirmación:
\[\ebox\metav{A} \entails_\mlSfour \ebox \ebox \metav{A}\]
Necesitaríamos construir un mundo, $w_1$, en el que $\ebox\metav{A}$ fuera verdadero, pero $\ebox \ebox \metav{A}$ fuera falso. Ahora, si $\ebox \ebox \metav{A}$ es falso en $w_1$, entonces $w_1$ debe acceder a algún mundo, $w_2$, en el que $\ebox\metav{A}$ es falso. Igualmente, si $\ebox \metav{A}$ es falso en $w_2$, entonces $w_2$ debe acceder a algún mundo, $w_3$, en el que $\metav{A}$ es falso. Acabamos de decir que $w_1$ accede a $w_2$, y $w_2$ accede a $w_3$. Entonces, como ahora estamos insistiendo en que la relación de accesibilidad sea transitiva, $w_1$ debe acceder a $w_3$. Y como $\ebox\metav{A}$ es verdadero en $w_1$, y $w_3$ es accesible desde $w_1$, se deduce que $\metav{A}$ debe ser verdadero en $w_3$. Entonces $\metav{A}$ es verdadero \emph{y} falso en $w_3$. \textexclamdown Contradicción!

\section{Una semántica para \mlSfive}
\label{SemanticsS5}

Agreguemos una restricción más a la relación de accesibilidad. Esta vez, insistamos en que también debe ser \emph{simétrica}:
\[\forall w_1\forall w_2(Rw_1w_2 \eif Rw_2w_1)\]
En español: si $w_1$ accede a $w_2$, entonces $w_2$ accede a $w_1$. O en términos de posibilidad relativa: si $w_2$ es posible relativo a $w_1$, entonces $w_1$ es posible relativo a $w_2$. Los lógicos llaman a una relación que es reflexiva, simétrica y transitiva una relación de \emph{equivalencia}. Ahora podemos definir una nueva relación de consecuencia, $\entails_\mlSfive$, de la siguiente manera:
\factoidbox{
	$\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\entails_\mlSfive \metav{C}$ si y solo si no hay ningún mundo en ninguna interpretación \emph{cuya relación de accesibilidad sea una relación de equivalencia}, en el que $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n$ sean todas verdaderas y $\metav{C}$ sea falsa
}
Hemos adjuntado el subíndice \mlSfive{} a $\entails$ porque resulta que el sistema \mlSfive{} es sólido y completo con respecto a esta nueva definición de validez:
\begin{compactlist}
	\item Si $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\proves_\mlSfive \metav{C}$, entonces $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\entails_\mlSfive \metav{C}$
	\item Si $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\entails_\mlSfive \metav{C}$, entonces $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\proves_\mlSfive \metav{C}$
\end{compactlist}
Como antes, no intentaremos demostrar estos resultados de solidez y completitud aquí. Sin embargo, es relativamente fácil ver cómo insistir en que la relación de accesibilidad debe ser una relación de equivalencia justificará la regla R$\mathbf{5}$:
\factoidbox{
	\begin{fitchproof}
			\have[m]{m}{\enot\ebox \metav{A}}
			\open
			\hypo[\ ]{k}{\ebox}\AS
			\have[\ ]{n}{\enot\ebox\metav{A}}\rfive{m}
	\end{fitchproof}
}
La regla dice que si $\metav{A}$ no es necesaria, es decir, falsa en algún mundo accesible, tampoco es necesaria en ningún mundo posible accesible, es decir, tenemos $\enot\ebox \metav{A} \proves_\mlSfive \ebox\enot\ebox \metav{A}$.

Para ver esto, simplemente imagina intentar construir una contra-interpretación a esta afirmación:
\[
	\enot\ebox\metav{A} \entails_\mlSfive \ebox \enot\ebox \metav{A}
\]
Necesitaríamos construir un mundo, $w_1$, en el que $\enot\ebox\metav{A}$ fuera verdadero, pero $\ebox \enot\ebox \metav{A}$ fuera falso.
Ahora, si $\enot\ebox\metav{A}$ es verdadero en $w_1$, entonces $w_1$ debe acceder a algún mundo, $w_2$, en el que $\metav{A}$ es falso. Igualmente, si $\ebox \enot\ebox \metav{A}$ es falso en $w_1$, entonces $w_1$ debe acceder a algún mundo, $w_3$, en el que $\enot\ebox \metav{A}$ es falso. Como ahora estamos insistiendo en que la relación de accesibilidad es una relación de equivalencia, y por lo tanto simétrica, podemos inferir que $w_3$ accede a $w_1$. Por lo tanto, $w_3$ accede a $w_1$, y $w_1$ accede a $w_2$. Nuevamente, como ahora estamos insistiendo en que la relación de accesibilidad es una relación de equivalencia, y por lo tanto transitiva, podemos inferir que $w_3$ accede a $w_2$. Pero antes dijimos que $\enot\ebox \metav{A}$ es falso en $w_3$, lo que implica que $\metav{A}$ es verdadero en todos los mundos a los que $w_3$ accede. Entonces $\metav{A}$ es verdadero \emph{y} falso en $w_2$. \textexclamdown Contradicción!

En la definición de $\entails_\mlSfive$, estipulamos que la relación de accesibilidad debe ser una relación de equivalencia. Pero resulta que hay otra forma de obtener una noción de validez adecuada para \mlSfive. En lugar de estipular que la relación de accesibilidad sea una relación de equivalencia, podemos estipular que sea una relación \emph{universal}:
\[\forall w_1\forall w_2\, Rw_1w_2\]
En español: cada mundo accede a cada mundo. O en términos de posibilidad relativa: cada mundo es posible relativo a cada mundo. Usando esta restricción en la relación de accesibilidad, podríamos haber definido $\entails_\mlSfive$ así:
\factoidbox{
	$\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\entails_\mlSfive \metav{C}$ si y solo si no hay ningún mundo en ninguna interpretación \emph{que tenga una relación de accesibilidad universal}, en el que $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n$ sean todas verdaderas y $\metav{C}$ sea falsa.
}
Si definiéramos $\entails_\mlSfive$ así, aún obtendríamos los mismos resultados de solidez y completitud para \mlSfive. \textexclamdown Qué nos dice esto? Bueno, significa que si estamos lidiando con una noción de necesidad según la cual \emph{cada} mundo es posible relativo a \emph{cada} mundo, entonces deberíamos usar \mlSfive. Es más, la mayoría de los filósofos asumen que las nociones de necesidad que más les preocupan, como la \emph{necesidad lógica} y la \emph{necesidad metafísica}, son exactamente de este tipo. Así que \mlSfive{} es el sistema modal que la mayoría de los filósofos usan la mayor parte del tiempo.

\practiceproblems

\problempart
Presente contrainterpretaciones a las siguientes afirmaciones falsas:
\begin{compactlist}
	\item $\enot P \entails_\mlK \enot\ediamond P$
	\item $\ebox(P \eor Q)\entails_\mlK \ebox P \eor \ebox Q$
	\item $\entails_\mlK \enot \ebox (A\eand \enot A)$
	\item $\ebox A\entails_\mlK A$
\end{compactlist}

\problempart
Presente contrainterpretaciones a las siguientes afirmaciones falsas:
\begin{compactlist}
	\item $\ediamond A\entails_\mlSfour \ebox\ediamond A$
	\item $\ediamond A, \ebox (\ediamond A \eif B)\entails_\mlSfour\ebox B$
\end{compactlist}

\problempart
Presente contrainterpretaciones a las siguientes afirmaciones falsas:
\begin{compactlist}
	\item $\ebox (M\eif O),\ediamond M\entails_\mlT O$
	\item $\ebox A\entails_\mlT \ebox \ebox A$
\end{compactlist}

\section*{Lecturas recomendadas}

La lógica modal es un amplio subcampo de la lógica. Sólo hemos arañado la superficie. Si quieres aprender más sobre lógica modal, aquí tienes algunos libros de texto que puedes consultar.

\begin{itemize}
	\item George E. Hughes and Max J. Cresswell, \textit{A New Introduction
	to Modal Logic}, Oxford: Routledge, 1996.
	\item Graham Priest, \textit{An Introduction to Non-Classical Logic},
	2nd ed., Cambridge: Cambridge University Press, 2008.
	\item James W. Garson, \textit{Modal Logic for Philosophers}, 2nd
	ed., Cambridge: Cambridge University Press, 2013.
\end{itemize}

Ninguno de estos autores formula sus sistemas de pruebas modales como lo hemos hecho nosotros, pero la formulación más parecida es la de Garson.