Uma lógica pode ser definida por um conjunto de fórmulas bem-formadas, uma classe de interpretações possíveis e uma relação de satisfação. A classe de interpreta- ções admissíveis para uma lógica modal L é geralmente especificada por restrições aos enquadramentos (frames) de Kripe. Em Nguyen (2010, p. 13-15) e em Nguyen (2006,
p. 250-252) encontram-se uma formulação tradicional, no estilo Hilbert, de uma Lógica mo- dal quantificada. Nessa lógica, termos são definidos indutivamente como variáveis, símbolos constantes e funções. Sintaticamente, as fórmulas são definidas como predicados n-ários e por operadores sintáticos de disjunção (∨) e negação clássica (¬), o quantificador universal (∀) e o (operador modal universal) 2, além da interdefinição de conectivos, nos moldes da Definição 3.3(Definição de conectivos). A semântica é dada em termos de enquadramentos e modelos de Kripe e por meio de relações de acessibilidade. A axiomatização desse sistema é dada como uma lógica modal normal ou seja, que possui no axioma K, conforme os seguintes axiomas:
a) axiomas da Lógica Clássica de Predicados sem identidade;
b) o axioma K = 2i(ϕ → ψ) → (2iϕ → 2iψ), também chamado de distribuição
epistêmica (van BENTHEM,2010, p. 139);
c) o axioma da fórmula de Barcan de alternação entre quantificadores e modalida- des: ∀x.2iϕ → 2i∀x.ϕ;
d) a definição da modalidade existencial: 3iϕ ≡ ¬2i¬ϕ;
e) a regra de modus ponens: ϕ, ϕ → ψ ⊢ ψ;
f) a regra de generalização: se ⊢ ϕ, então ⊢ ∀x.ϕx; g) a regra de necessitação: se ⊢ ϕ, então ⊢ 2iϕ.
Por questão de brevidade, por não apresentar contribuição relevante e por se tratar de construção padrão, obstém-se de transcrever nesta seção as definições presentes na obra citada para essa lógica. Porém, esse sistema é utilizado pelo autor para discutir como a combinação de diferentes axiomas pode ser incluída nessa lógica para criar sistemas cujas aplicações são de interesse desta pesquisa. Em vista disso, com o objetivo de explorar sistemas para formalização de raciocínios sobre epistemologias, aTabela 2 sistematiza um conjunto desses axiomas, as relações de acessibilidade que eles denotam entre os mundos e um significado possível para cada um deles.
Com base nos axiomas generalizados da Tabela 2, em Nguyen (2010, p. 14-18) explora-se a combinação arbitrária deles com a lógica apresentada para obtenção de sistemas com propriedades específicas referentes ao raciocínio sobre a crença de vários agentes. Os axiomas seguintes, por exemplo, podem ser combinados para criação de lógicas que se prestam a descrever estados epistêmicos de agentes sobre graus de conhecimentos:
3.2. Programação em Lógica Modal: MProlog 107
Tabela 2 – Axiomas referentes a modalidades epistêmicas
Axioma Esquema Restrição Exemplo de significado
(D)
2iϕ → ¬2i¬ϕ, que é o mesmo que 2iϕ → 3iϕ
∀u ∃v Ri(u, v)
a crença é consistente: afirma- ções aleticamente necessárias são também afirmações possí- veis
(I) 2iϕ → 2jϕ se i > j Rj⊆ Ri se i > j o índice indica grau de crença
(4) 2iϕ → 2i2iϕ ∀u, v, w (Ri(u, v)∧Ri(v, w) → Ri(u, w))
a crença satisfaz introspecção positiva (transitividade) (4s) 2iϕ → 2j2iϕ ∀u, v, w (Rj(u, v)∧Ri(v, w) → Ri(u, w))
a crença satisfaz introspecção positiva forte (transitividade) (5) ¬2iϕ → 2i¬2iϕ ∀u, v, w (Ri(u, v)∧Ri(u, w) → Ri(v, w))
a crença satisfaz introspecção negativa (euclidiana)
(5s) ¬2iϕ → 2j¬2iϕ ∀u, v, w (Rj(u, v)∧Ri(u, w) → Ri(v, w)) a crença satisfaz introspecçãonegativa forte (euclidiana) Fonte: Os autores. Adaptado de Nguyen(2010, p. 17, 18) e deNguyen(2004b, p. 268).
KDI4s = K(m) + (D) + (I) + (4s)
KDI4 = K(m) + (D) + (I) + (4)
KDI4s5 = K(m) + (D) + (I) + (4s) + (5)
KDI45 = K(m) + (D) + (I) + (4) + (5)
Nesses sistemas, o axioma (I) faz com que 2iϕ signifique “acredita-se em ϕ até
o grau i”, e que 3iϕ possa ser lido como “é possível fracamente até o grau i que ϕ”.
Os axiomas (5) são controversos, por serem são muito fortes, uma vez que poderia ser interpretados como “aquilo se crê como não sendo o caso, acredita-se que necessariamente não é o caso”. Por isso, os sistemas KDI4 e KDI4s7 foram desenvolvidos, como uma
alternativa mais fraca do que os que contém (I).
Para os sistemas multiagentes, os índices dos operadores modais 2 e 3 denotam agentes e assume-se que 2iϕ representa “o agente i acredita que ϕ é verdadeiro” e 3iϕ
representa que “ϕ é considerado possível pelo agente i”.
Em sistemas de crença distribuída, os agentes possuem acesso completo às bases de crenças uns dos outros. Nesse caso, os agentes são amigos e colaboram uns com os outros em um sistema unificado. Para sistemas de crença distribuída com colaboração, a seguinte composição de axiomas pode ser utilizada:
KD4s5s = K(m) + (D) + (4s) + (5s)
Outra forma de combinação de axiomas permite criar um sistema de multiagentes em que os integrantes são oponentes, e trabalham uns contra os outros. Uma interpretação desse tipo de sistema permite que sejam desenvolvidas situações em que um agente tenta simular os estados epistêmicos dos outros. Uma composição adequada para esse tipo de sistema é esta, em que o índice m é utilizado apenas para indicar que se trata de um sistema com múltiplos agentes:
KD45m = K(m) + (D) + (4s) + (5s)
O tipo de interpretação apresentada por esses sistemas é baseada na ideia crença, e não exatamente de conhecimento. Por isso, também poderiam ser chamados de lógicas doxásticas. O axioma (D) é especialmente importante para as interpretações doxásticas/e- pistêmicas porque denota que o agente não acredita simultaneamente em uma afirmação e sua negação, ou seja, trata-se de um tipo de agente racional (SMULLYAN, 1986).
O objetivo desses axiomas e sistemas é capturar propriedades importantes de crença e de crença compartilhada que são úteis aos objetivos desta pesquisa, e não investigar exaustivamente essas formulações. Esses sistemas epistêmicos são explorados noCapítulo 9.
3.2.2 Sintaxe base de teorias MProlog
Sintaticamente, em MProlog modalidades são representadas como listas, como nos exemplos seguintes. À esquerda estão fórmulas lógicas tradicionais (por exemplo, conforme são apresentadas por Carnielli e Pizzi (2008)), e à direita estão transliterações dessas fórmulas em sentenças de MProlog, sendo que b é um símbolo para “box”, d para “diamond”, bel para “believe”, e pos para “possible”:
23q(x, y) [b, d] : q (X, Y)
2ihX3i3jq(a) [bel(I), pos(3,X), pos(J)] : q (a)
christian(x) → 2xgod_exists [bel(X)] : god_exists :- christian(X)
Ainda no ponto de vista sintático, programas Prolog são programas MProlog, de modo que fragmentos modais em programas MProlog podem conter diretivas e cláusulas clássicas. Assim, cada cláusula que faz parte do conjunto de cláusulas de um programa MProlog possui uma das seguintes formas:
Context : (Head :- Body).
Head :- Body.
em que Context é uma lista que representa modalidades, Head ou possui a forma E ou a forma M : E, sendo que E é um átomo clássico, e M é uma lista contendo uma ou mais modalidades. Com essa forma, uma sentença em MProlog pode tanto conter expressões clássicas de Prolog, como modais de MProlog. Isso é útil aos objetivos estipulados na
3.2. Programação em Lógica Modal: MProlog 109
seção 1.2, por exemplo, porque permite combinar regras lógicas que validam restrições em modelos ontológicos classicamente, e regras epistêmicas modalmente.