Lógica modal

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

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, deve, 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 semântica de Kripke.

História[editar | editar código-fonte]

Hugh MacColl foi o pioneiro da lógica modal axiomática, particularmente com a sua obra de 1906 Symbolic Logic and its Applications. Em 1918, C. I. Lewis é o primeiro autor a fazer um estudo sistemático nesta área com 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[editar | editar código-fonte]

Modalidades de necessidade e possibilidade são chamadas modalidades aléticas. A lógica modal foi desenvolvida primariamente para lidar com esses conceitos, e somente posteriormente foi estendida para tratar outros. 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;
  • 'consistente '(ou melhor "contingente") se e somente se ela é de fato verdadeira (e então possivelmente verdade) 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 estas 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[editar | editar código-fonte]

Algumas vezes é fisicamente possível se é permitida pelas leis da natureza. Por exemplo, é possível (fisicamente falando) haver um átomo com um número atômico de 150, apesar de talvez de fato não haver um. Por outro lado, não é possível, no mesmo contexto, haver um elemento cujo núcleo contém 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[editar | editar código-fonte]

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 existe (ou não existe). Saul Kripke argumentou que toda pessoa necessariamente tem os pais que tem: qualquer um com pais diferentes não seria a mesma pessoa.

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 possibilidade física é questão 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[editar | editar código-fonte]

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, pode-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[editar | editar código-fonte]

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[editar | editar código-fonte]

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 \and 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 \and 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 \and 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 \and x\,R\,z \longrightarrow \exists w (y\,R\,w \and z\,R\,w)
(2) \Box \Box A \longrightarrow \Box A (simula densidade)
  • \forall x \forall y (x\neq y \and x\,R\,y \longrightarrow \exists z (z \neq x \and z \neq y \and (x\,R\,y \and 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 \and x\,R\,y \longrightarrow \exists z (z \neq x \and z \neq y \and (x\,R\,y \and 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
  • \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[editar | editar código-fonte]

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[editar | editar código-fonte]

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

Definições[editar | editar código-fonte]

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:

\, F A \longleftrightarrow \lnot G \lnot A
\, P A \longleftrightarrow \lnot H \lnot A

Sistema base[editar | editar código-fonte]

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[editar | editar código-fonte]

Mais detalhes no artigo 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[editar | editar código-fonte]

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:

\, P A \longleftrightarrow \lnot O \lnot A
\, F A \longleftrightarrow O \lnot A

Sistema base[editar | editar código-fonte]

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[editar | editar código-fonte]

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 O A . Mas há conceitos de obrigação que diferenciam essas iterações, portanto é necessário tomar cuidado.

Lógica doxástica[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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 \and \varphi ' se M, w \vDash\varphi e M, w \vDash \varphi';
  •  M, w \vDash \varphi \or \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[editar | editar código-fonte]

No século XX tivemos um considerável avanço sobre o entendimento formal do significado das modalidades. Os trabalhos de Jónsson, McKinsey e Tarski na década de quarenta 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 cinqüenta, Kripke propôs uma semântica interessante para estes sistemas como acima apresentada. 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 60 têm por objetivo apresentar uma síntese destas 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 surpreendente e interessante do trabalho do Lemmon é o teorema da representação. Esse teorema de representação 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). O objetivo inicial do presente trabalho era estender este mesmo resultado algébrico para os sistemas da classe “Gmnpq” proposta por Lemmon e Scott nas “Lemmon notes”.[1]

Principais contribuidores da lógica modal[editar | editar código-fonte]

  • 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 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 intensional.

Aplicações[editar | editar código-fonte]

  • 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]

Notas e referências

Ligações externas[editar | editar código-fonte]