# Teorema de redução de modalidades em S5

O teorema de redução de modalidades em S5 (um sistema de lógica modal construído com a adição da euclidianidade e reflexividade à lógica K) diz que qualquer fórmula de grau modal maior do que 1 (que apresente mais de um operador modal aplicado a uma mesma fórmula) é reduzível em S5 a uma fórmula de primeiro grau. Formalmente:
   * $\Theta _{1}\Theta _{2}...\Box \alpha \dashv \vdash \Box \alpha$ e $\Theta _{1}\Theta _{2}...\Diamond \alpha \dashv \vdash \Diamond \alpha$, em que $\,\Theta _{i}$ pode ser $\Box$ ou $\Diamond$.

## Procedimento para redução

É suficiente mostrar que qualquer fórmula de segundo grau pode ser reduzida a uma de primeiro grau, visto que a repetição desse procedimento possibilita tratar os casos de maior grau. As equivalências necessárias para aplicar o procedimento serão as seguintes (todas válidas em S5):

### Equivalências necessárias

   * R1: $\Diamond p\dashv \vdash \Box \Diamond p$
   * R2: $\Box p\dashv \vdash \Diamond \Box p$
   * R3: $\Diamond p\dashv \vdash \Diamond \Diamond p$
   * R4: $\Box p\dashv \vdash \Box \Box p$
   * K3: $\Box (p\land q)\dashv \vdash (\Box p\land \Box q)$
   * K6: $\Diamond (p\lor q)\dashv \vdash (\Diamond p\lor \Diamond q)$
   * S5(4): $\Box (p\lor \Box q)\dashv \vdash (\Box p\lor \Box q)$
   * S5(5): $\Box (p\lor \Diamond q)\dashv \vdash (\Box p\lor \Diamond q)$
   * S5(6): $\Diamond (p\land \Diamond q)\dashv \vdash (\Diamond p\land \Diamond q)$
   * S5(7): $\Diamond (p\land \Box q)\dashv \vdash (\Diamond p\land \Box q)$

### Método

K3 (lei de distribuição do $\Box$) nos permite distribuir $\Box$ sobre qualquer conjunção. Se qualquer dos membros da conjunção começar com um operador modal, a lei de redução apropriada nos possibilitará "deletar" $\Box$ quando ele encontrar com este operador. Assim, $\Box (p\land \Diamond q)$ se torna não somente $\Box p\land \Box \Diamond q$ por K3, mas também $\Box p\land \Diamond q$ por R1. Dizemos nesse caso que $\Box$ foi absorvido por $\Diamond$.
S4(4) e S4(5) nos permitem o mesmo tipo de distribuição e absorção quando $\Box$ precede uma disjunção, desde que pelo menos um dos lados originais dela comece com um operador modal. (S4(4) e S4(5) são definidos apenas para disjunções com dois membros. Se quisermos praticar a distrubuição do $\Box$ sobre uma disjunção de n membros devemos tomar todos os elementos da disjunção, menos um com um operador modal, e tratá-los como um único elemento. Por exemplo: $\Box (p\lor \Diamond q\lor r\lor \Box s)$ forma: $\Box ((p\lor r\lor \Box s)\lor \Diamond q)$, que aplicando S5(5) nos dá: $\Box ((p\lor e)\lor \Box s)\lor \Diamond q$ que por S4(4) nos dá: $\Box (p\lor r)\lor \Box s\lor \Diamond q$. Não vamos para: $\Box p\lor \Diamond q\lor \Box r\lor \Box s$, visto que a fórmula já apresenta grau modal 1.
K6 (lei de distruibuição do $\Diamond$), junto com S5(6) e S5(7) analogamente nos permitem executar a distribuição e absorção do $\Diamond$ irrestritamente sobre uma disjunção e, como visto anteriormente, sobre uma conjunção. Estes são passos chaves no processo de redução para o grau 1.
Como dito anteriormente, é suficiente mostrar como reduzir uma fórmula de grau 2 para uma de grau 1. Há quatro passos neste processo, apesar de nem sempre serem necessários os quatro em todos os casos. Os três primeiros são diretos:
* 1 - Primeiro eliminar todos os operadores com exceção de $\neg ,\Box ,\Diamond ,\lor$ e $\land$ usando as definições apropriadas.
* 2 - Então eliminar todas as ocorrências de $\neg$ imediatamente antes de um parêntese ou de um operador modal pelas leis de De Morgan e de interdefinição entre $\Box$ e $\Diamond$.
* 3 - Em seguida reduzir todas as modalidades iteradas (mais de uma em seqüência) para modalidades únicas pelas leis de redução R1-R4.
* 4 - Se a fórmula resultante dos passos 1-3 ainda é de segundo grau, só pode ser porque ela, ou alguma parte dela, é da forma $\Box \alpha$ ou $\Diamond \alpha$, em que $\,\alpha$ é de grau 1 e é ou uma conjunção ou uma disjunção.

#### Casos especiais

Considere o caso $\Box \alpha$. Há três possibilidades: (a) $\,\alpha$ é uma conjunção; nesse caso, desde que $\Box$ se ditribui irrestritamente sobre conjunções, distribui-se $\Box$ sobre a conjunção em $\,\alpha$, deixando-o ser absorvido por qualquer operador modal que venha a encontrar no processo.
(b) $\,\alpha$ é uma disjunção em que pelo menos um dos lados começa com um operador modal; nesse caso, novamente distribuimos $\Box$ e o deixamos ser absorvido.
(c) $\,\alpha$ é uma disjunção em que nenhum dos lados começa com um operador modal. Uma vez que $\,\alpha$ é de grau 1, só pode ser porque um dos lados da disjunção de $\,\alpha$ é uma conjunção com um operador modal nela. Para resolver este caso transforma-se $\,\alpha$ em uma conjunção, pela lei da distributividade ($p\lor (q\land r))\equiv ((p\lor q)\land (p\lor r))$), e distribui-se $\Box$ pela conjunção obtida. Por exemplo:
Se $\Box \alpha$ é $\Box (p\lor (q\land \Diamond r))$, transforma-se, pela distributividade, em $\Box ((p\lor q)\land (p\lor \Diamond r))$
e então, por K3', em
$\Box (p\lor q)\land \Box (p\lor \Diamond r)$, podendo resolver como em (b), obtendo $\Box (p\lor q)\land (\Box p\lor \Diamond r)$, ou, caso seja impossível, aplicando mais uma vez a distributividade e K3.
A repetição desses passos sempre possibilitará ao $\Box$ encontrar cada operador modal em $\,\alpha$, não importa o quão profundamente imerso o operador esteja.
O caso de $\Diamond \alpha$ pode ser resolvido de forma análoga, exceto que desta vez é quando $\,\alpha$ é uma conjunção em que nenhum dos lados começa com um operador modal que possa ser tratato diretamente, e a lei de distributividade se faz novamente necessária.

## Resultados

Portanto, em S5, qualquer fórmula bem fundada (que não pode ser reescrita infinitamente) é equivalente a alguma fórmula de grau modal 1 em função de suas variáveis. (Verdade mesmo que a fórmula não contenha operadores modais; qualque fórmula bem fundada $\,\alpha$ é equivalente a $\,\alpha \land (\Box p\lor \neg \Box p)$, sendo $\,p$ alguma variável de $\,\alpha$.) Não é difícil ver que só poe haver um número finito de funções modais (de qualquer conjunto de variáveis) de grau 1 distintas, visto que há apenas um número finito de fórmulas não-equivalentes.