# Lógica modal

A lógica modal se refere a qualquer sistema de lógica formal que procure lidar com modalidades (tratar de modos quanto a tempo, possibilidade, probabilidade, etc.). Tradicionalmente, as modalidades mais comuns são possibilidade e necessidade. Lógicas para lidar com outros termos relacionados (como probabilidade, eventualidade, padronização, poder, poderia, dever e deveria) são por extensão também chamadas de lógicas modais, já que elas podem ser tratadas de maneira similar.
Uma lógica modal formal representa modalidades usando operadores modais. Por exemplo: "Era possível o assassinato de Arnaldo" e "Arnaldo foi possivelmente assassinado" são exemplos que contêm a noção de possibilidade. Formalmente, essa noção é tratada como o operador modal Possível, aplicado à sentença "Arnaldo foi assassinado".
Normalmente os operadores modais básicos unários são escritos como $\Box$ (ou L) para Necessário e $\Diamond$ (ou M) para Possível. Nas lógicas modais clássicas, cada um pode ser expresso em função do outro e da negação:
    $\Diamond A\equiv \lnot \Box \lnot A$
    $\Box A\equiv \lnot \Diamond \lnot A$
Para a formalização semântica da linguagem modal básica, veja a seção semântica de Kripke, a seguir.

## História

Hugh MacColl foi o pioneiro da lógica modal axiomática, particularmente por sua obra de 1906, Symbolic Logic and its Applications. Em 1918, C. I. Lewis foi o primeiro autor a fazer um estudo sistemático nesta área, em A Survey of Symbolic Logic. Na escola fenomenológica, o precursor foi Oskar Becker, com o seu artigo "Zur Logik der Modalitäten", de 1930. A primeira formalização clara da lógica modal surge com a obra de C. I. Lewis e de C. H. Langdorf, Symbolic Logic, de 1932, sendo esta a primeira grande referência desta disciplina.
O fundador da lógica formal moderna, Gottlob Frege, duvidava que a lógica modal fosse viável. Dois de seus mais conhecidos leitores, Rudolf Carnap e Kurt Gödel (1933), romperam com Frege, nessa questão, e escolheram buscar a estrutura matemática de uma lógica que lidasse com as três modalidades clássicas (possibilidade, necessidade e probabilidade). Em 1937, Robert Feyes, seguidor de Gödel, propôs o sistema T de lógica modal. Em 1951, Georg Henrik von Wright propôs o sistema M, que é elaborado sobre o sistema T. Também nos anos 1950s, C. I. Lewis construiu, sobre o sistema M, seus conhecidos sistemas modais S1, S2, S3, S4 e S5. Em 1965, Saul Kripke estabeleceu o sistema modal normal mínimo K.

## Modalidades aléticas

Modalidades de necessidade e possibilidade são chamadas modalidades aléticas. A lógica modal foi desenvolvida primariamente para lidar com esses conceitos, e só posteriormente foi estendida a outros conceitos. Por essa razão (ou talvez por sua familiaridade e simplicidade), necessidade e possibilidade são comumente tratadas como o tema principal da lógica modal.
Uma proposição é dita ser
* possível se e somente se ela é não necessariamente falsa (independente de ser realmente verdadeira ou falsa);
* necessária se e somente se ela é não possivelmente falsa;
* contingente se e somente se ela é de fato verdadeira (e então possivelmente verdadeira) e não necessariamente verdadeira.
Claramente, se quisermos definições dessas noções de forma não circular, precisaremos pegar algum dos operadores (possibilidade ou necessidade) como primitivo, ou então analisar essas noções em termos de outras que não incluam nem possibilidade nem necessidade, e que sejam elas mesmas definidas de forma não circular.

### Possibilidade física

Algumas vezes algo é fisicamente possível, se é permitido pelas leis da natureza. Por exemplo, é possível (fisicamente falando) haver um átomo com um número atômico 150, apesar de talvez não existir de fato. Por outro lado, não é possível, no mesmo contexto, haver um elemento cujo núcleo contenha queijo. Enquanto é logicamente possível acelerar um objeto além da velocidade da luz, não é, de acordo com Einstein, fisicamente possível ultrapassá-la.

### Possibilidade metafísica

Filósofos ponderam as propriedades que um objeto possui independentemente das leis científicas. Por exemplo, pode ser metafisicamente necessário, como alguns pensam, que todos os seres pensantes tenham corpos e possam experimentar a passagem do tempo, ou que Deus exista (ou não exista). Saul Kripke argumentou que toda pessoa necessariamente tem os pais que tem: qualquer um com pais diferentes não seria a mesma pessoa.
A possibilidade metafísica é geralmente tida como mais forte que a simples possibilidade lógica (isto é, menos coisas são metafisicamente possíveis do que logicamente possíveis). Sua exata relação com a possibilidade física é objeto de algumas discussões. Filósofos também discordam se verdades metafísicas são necessárias meramente "por definição", ou se elas refletem alguns importantes fatos sobre o mundo, ou alguma outra coisa completamente diferente.

## Lógicas modais

As lógicas mais familiares na família modal são construídas a partir da lógica fraca K (em homenagem a Saul Kripke). Usando K como base, podem-se construir diferentes sistemas. Os símbolos de K incluem $\lnot$ para negação, $\longrightarrow$ para implicação, e $\Box$ para o operador modal de necessidade (os outros operadores são construídos a partir destes, inclusive o $\Diamond$, com a equivalência usando negação e $\Box$).

### Definição do sistema base

K é o resultado da adição dos seguintes teoremas à lógica proposicional:
* Regra da necessitação: se $\,A$ é teorema de K, então $\Box A$ também é.
* Axioma da distributividade: $\Box (A\longrightarrow B)\longrightarrow (\Box A\longrightarrow \Box B)$.
A regra da necessitação estabelece que qualquer teorema da lógica é necessário. O axioma da distributividade diz que se é necessário $A\longrightarrow B$, então é necessário $\Box A\longrightarrow \Box B$.
Em K, os operadores $\Box$ e $\Diamond$ se comportam de forma parecida com os quantificadores $\forall$ (para todo) e $\exists$ (existe). Por exemplo, a definição de $\Diamond$ a partir de $\Box$ espelha a equivalência $\forall x\,A\equiv \lnot \exists x\,\lnot A$ em lógica de predicados. As bases dessa correspondência entre os operadores modais e os quantificadores ficam mais claras quando se lida com a semântica de Kripke.

### Construção de sistemas

Outros sistemas são construídos adicionando-se axiomas a K. Por exemplo, o sistema T é obtido com o acréscimo do axioma:
(T) $\Box A\longrightarrow A$
Em primeira ordem: $\forall x(x\,R\,x)$ (Axioma da reflexividade)
Outros axiomas que podem ser adicionados para construir outros sistemas são:
    (B) $\,A\longrightarrow \Box \Diamond A$ (axioma da simetria)
      * $\forall x,y(x\,R\,y\longrightarrow y\,R\,x)$
    (4) $\Box A\longrightarrow \Box \Box A$ (axioma da transitividade)
      * $\forall x,y,z(x\,R\,y\land y\,R\,z\longrightarrow x\,R\,z)$
    (5) $\Diamond A\longrightarrow \Box \Diamond A$ (axioma da euclidianidade)
      * $\forall x\forall y\forall z(x\,R\,y\land x\,R\,z\longrightarrow y\,R\,z)$
    (D) $\Box A\longrightarrow \Diamond A$ (axioma da serialidade)
      * $\forall x\exists y(x\,R\,y)$
    (CD) $\Diamond A\longrightarrow \Box A$ (axioma da unicidade)
      * $\forall x\forall y\forall z(x\,R\,y\land x\,R\,z\longrightarrow y=z)$
    (X) $\Diamond \Box A\longrightarrow \Box \Diamond A$ (simula convergência)
      * $\forall x\forall y\forall z(x\,R\,y\land x\,R\,z\longrightarrow \exists w(y\,R\,w\land z\,R\,w)$
    (2) $\Box \Box A\longrightarrow \Box A$ (simula densidade)
      * $\forall x\forall y(x\neq y\land x\,R\,y\longrightarrow \exists z(z\neq x\land z\neq y\land (x\,R\,y\land z\,R\,y)))$
    (GL) $\Box (\Box A\longrightarrow A)\longrightarrow \Box A$ (axioma de Gödel-Löb)
      * $\forall x\forall y(x\neq y\land x\,R\,y\longrightarrow \exists z(z\neq x\land z\neq y\land (x\,R\,y\land z\,R\,y)))$
O sistema S4 é o resultado de se adicionar 4 a T. Analogamente, S5 é o resultado de se adicionar 5 a T. Estes dois sistemas apresentam importantes característica de simplificação que propiciam a redução de suas fórmulas, devido às suas propriedades.
* Em S4:
** $\Box _{1}\Box _{2}\Box _{3}...\Box _{n}\alpha \dashv \vdash \Box \alpha$ e $\Diamond _{1}\Diamond _{2}\Diamond _{3}...\Diamond _{n}\alpha \dashv \vdash \Diamond \alpha$
* Em S5, onde é ainda mais forte (ver teorema de redução em S5):
** $\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$.

## Lógica epistêmica

Modalidades epistêmicas (do grego episteme, conhecimento) lidam com a certeza de sentenças. Os operadores são traduzidos como "É certamente verdade que..." e "É possível (dada a informação disponível) ser verdade que...". Na fala normal ambas as modalidades são normalmente expressas em palavras similares; os seguintes contrastes podem ajudar:
Uma pessoa, José, pode perfeitamente dizer ambos: (1) "Não, não é possível que o Pé-grande exista; estou certo disso."; e, (2) "Claro, o Pé-grande possivelmente poderia existir". O que José quer dizer por (1) é que dadas todas as informações disponíveis, não há dúvida quanto ao Pé-grande existir. Isto é uma asserção epistêmica. Por (2) ele faz a asserção metafísica que é possível vir a existir o Pé-grande, mesmo que ele não exista (o que não é equivalente a "é possível que o Pé-grande exista - pelo que sei", o que contradiz (1)).
Possibilidades epistêmicas também se portam no mundo real de uma forma que as possibilidades metafísicas não fazem. Possibilidades metafísicas se portam no modo que o mundo pode ter sido, mas as possibilidades epistêmicas se portam no modo que o mundo pode ser (pelo que se sabe). Suponha, por exemplo, que quero saber se vou ou não pegar o guarda-chuva antes de sair. Se você me diz "é possível que esteja chovendo lá fora" - no sentido de possibilidade epistêmica - então isto iria pesar em pegar ou não o guarda-chuva. Mas se você me diz "é possível vir a chover lá fora" - no sentido de possibilidade metafísica - então este tipo de esclarecimento modal não me ajuda.

## Lógica temporal

O termo faz menção às lógicas que buscam falar sobre o tempo, atrelando as ideias de possibilidade e necessidade à de tempo. Por exemplo: "Possivelmente choverá amanhã", ou "é necessário que chova amanhã".

### Definições

Definida a partir dos seguintes operadores:
    $\,G\equiv$ "será sempre o caso que..."
    $\,F\equiv$ "será o caso que..."
    $\,H\equiv$ "sempre foi o caso que..."
    $\,P\equiv$ "foi o caso que..."
Sendo que os primitivos são G e H, e os outros podem ser introduzidos através das seguntes equivalências:
    $\,FA\longleftrightarrow \lnot G\lnot A$
    $\,PA\longleftrightarrow \lnot H\lnot A$

### Sistema base

O sistema básico de lógicas temporais, chamado Kt, é resultado de adotar-se os princípios de K tanto para G como para H, junto com dois axiomas para controlar as interações entre os operadores de passado e futuro:
* Regra da necessitação: se $\,A$ é teorema de K, então também o são $\,GA$ e $\,HA$.
* Axiomas da distribuição:
    $G(A\longrightarrow B)\longrightarrow (GA\longrightarrow GB)$
    $H(A\longrightarrow B)\longrightarrow (HA\longrightarrow HB)$
* Axiomas de iteração:
    $A\longrightarrow GPA$
    $A\longrightarrow HFA$
Do mesmo modo que nas lógicas modais comuns, outros axiomas podem ser adicionados para criar novos sistemas, como é o caso da Lógica temporal linear (estendendo-a com a adição dos operadores $\,S$ e $\,U$ (desde e até) e retirando os operadores $\,H$ e $\,P$ para tratar a ideia de ordem temporal e a de que não é possível voltar no tempo).

## Lógica deôntica

Procura modular a ideia de dever e permissão, como a diferença entre "Você deve fazer isso..." e "Você pode fazer isso..." (semelhante à diferença entre ser necessário e possível). O nome deôntica vem do grego para dever.
Uma característica das lógicas deônticas é que elas não possuem o axioma T (semanticamente correspondente à reflexividade), pois ele correponderia a dizer que (interpretando $\Box$ como obrigatoriedade, $\,O$) que toda obrigação é verdadeira. Por exemplo, se é obrigatório não matar os outros, então T implecia que as pessoas realmente não matam umas as outras. Conseqüência esta obviamente falsa.
O axioma D (semanticamente correspondente à ideia de serialidade) é um comumente aceito como um princípio deôntico. É a formalização da ideia de Kant de que "dever implicar poder". (Claramente o 'poder' pode ser interpretado de várias maneiras, por exemplo, em um sentido moral ou alético.)

### Definições

Definida a partir dos seguintes operadores:
    $\,O\equiv$ "é obrigatório que..."
    $\,P\equiv$ "é permitido que..."
    $\,F\equiv$ "é proibido que..."
Sendo que o primitivo é O, e os outros podem ser introduzidos através das seguntes equivalências:
    $\,PA\longleftrightarrow \lnot O\lnot A$
    $\,FA\longleftrightarrow O\lnot A$

### Sistema base

O sistema básico D é construído adicionando o fraco axioma D a K (uma vez que o axioma T não é permitido):
    (D) $\,OA\longrightarrow \,PA$ (o que é obrigatório é permitido).

### Iterações

Há controvérsias sobre a iteração (repetição) de operadores na lógica deôntica. Em alguns conceitos, $\,OOA$ seria simplesmente equivalente a $\,OA$, $\,O$ que implica a introdução de teoremas que garantam que $\,O_{1}O_{2}O_{3}...O_{n}A\dashv \vdash OA$. Mas há conceitos de obrigação que diferenciam essas iterações, portanto é necessário tomar cuidado.

## Lógica doxástica

Preocupa-se com a ideia de crença e raciocínio. O termo "doxástica" é derivado do grego antido doxa, 'crença'. Tipicamente, uma lógica doxástica usa o $\Box$, ou $\,B$, significando "Acredita-se que", ou quando aplicado a um agente $\,\alpha$, "$\,\alpha$ acredita que".

## Outras lógicas modais

Significativamente, lógicas modais podem ser construídas para acomodarem a maioria desses idiomas; é fato que sua estrutura lógica comum faz com que todas variem a partir da mesma coisa. Lógica epistêmica é melhor capturada no sistema S4; lógica deôntica no sistema D; lógica temporal em T e lógica alética lida melhor com S5.

## Semântica de Kripke

Uma forma de definir uma semântica para um sistema de lógica modal é com a semântica de mundos possíveis, ou semântica de Kripke. Antes de mostrar quando uma forma é satisfatível ou não, algumas definições se fazem necessárias:

### Definições

Um enquadramento modal ou enquadramento é um par $\,E=(W,R)$, em que
   * $\,W$ é um conjunto não vazio (conjunto de mundos, pontos, estados, nós, instantes... depende do contexto da lógica modal).
   * $\,R$ é uma relação binária em $\,W$ dita relação de acessibilidade (ou relação de visibilidade).
Sendo $w_{1},w_{2}\in W$, diz-se que $\,w_{2}$ é acessível a partir de $\,w_{1}$ se $(w_{1},w_{2})\in R$.
Seja $\,At$ um conjunto enumerável de variáveis atômicas. Uma estrutura de interpretação modal sobre $\,At$ é um par $\,M=(E,V)$, em que
   * $\,E=(W,R)$ é um enquadramento modal
   * $V:At\longrightarrow {\mathcal {P}}(W)$ é uma função.
$\,M$ pode ser também representado como $\,(W,R,V)$, sendo as duas primeiras componentes os constituindos do enquadramento modal subjacente à estrutura de interpretação em $\,At$.

### Satisfatibilidade

Desta forma, finalmente, a noção de satisfação de uma forma modal, com essa semântica, é:
* Seja $\,M=(W,R,V)$ uma estrutura de interpretação modal e $w\in W$. A noção de satisfação de $\varphi \in FM_{P}$ por $\,M$ no mundo $\,w$ denota-se por
    $M,w\vDash \varphi$
e define-se indutivamente como se segue:
   * para cada $p\in At,M,w\vDash p$ se $w\in V(p)$;
   * não $M,w\vDash \bot$;
   * $M,w\vDash \varphi \longrightarrow \varphi '$ se $M,w\nvDash \varphi$ ou $M,w\vDash \varphi '$;
   * $M,w\vDash \varphi \land \varphi '$ se $M,w\vDash \varphi$ e $M,w\vDash \varphi '$;
   * $M,w\vDash \varphi \lor \varphi '$ se $M,w\vDash \varphi$ ou $M,w\vDash \varphi '$;
   * $M,w\vDash \Box \varphi$ se $M,w\vDash \varphi$ para todo $w'\in W$ tal que $w\,R\,w'$;
   * $M,w\vDash \Diamond \varphi$ se existe $w'\in W$ tal que $w\,R\,w'$ e $M,w'\vDash \varphi$;

## Semântica algébrica

No século XX tivemos um considerável avanço no entendimento formal do significado das modalidades. Os trabalhos de Jónsson, McKinsey e Tarski, na década de 1940, permitiram a construção dos resultados de completude algébrica para os sistemas modais. Estes resultados, porém, não receberam a devida atenção. No final da década de 1950, Kripke propôs uma semântica interessante para estes sistemas. Tal semântica, hoje conhecida como semântica de Kripke ou semântica dos mundos possíveis, causou um grande impacto no âmbito da filosofia analítica. Os artigos escritos por Lemmon na década de 1960 têm por objetivo apresentar uma síntese dessas duas semânticas. Um interessante resultado mostrado nestes artigos é que a completude semântica pode ser deduzida de resultados algébricos por meio de um teorema central. Um dos resultados mais surpreendentes e interessantes do trabalho do Lemmon é o teorema da representação. Esse teorema, para a lógica modal, tem como consequência a conexão entre o ponto de vista algébrico e o ponto de vista da semântica dos mundos possíveis (ou semântica de Kripke).

## Principais contribuidores da lógica modal

* Clarence Irving Lewis - em 1912 deu origem à lógica modal moderna, composta pelas três tradições: semântica, algébrica e sintática.
* Saul Aaron Kripke - amplamente conhecido como um dos mais importantes filósofos vivos, e relevantíssimo nessa área, por sua semântica (semântica de Kripke).
* Vaughan Ronald Pratt - desenvolvedor do sistema de lógica dinâmica.
* Arthur Norman Prior - fundou a lógica temporal e contribuiu com a lógica intencional.

## Aplicações

* Representação de conhecimento (protocolos de autenticação). [Lógica epistêmica]
* Verificação formal de programas (sistemas concorrentes, distribuídos, etc.). [Lógica temporal]