Extensões de primeira ordem para a lógica do anúncio público

Abstract

Dentre as lógicas multimodais, a lógica epistêmica dinâmica foi desenvolvida para modelar as mudanças de estados epistêmicos em grupos de agentes. Inspirada em recursos da lógica dinâmica (concebida para lidar com programas computacionais), aquela lógica permite representar a própria transição entre estados epistêmicos, tanto individuais como grupais, dos agentes considerados. Essa transição pode ser devida a diferentes ações epistêmicas (p.ex., o compartilhamento de uma informação com uma pessoa ou grupo em privado). A versão mais simples (e inicial) dessa lógica ficou conhecida como lógica do anúncio público, que considera apenas um tipo de ação epistêmica: a divulgação pública e simultânea de uma informação para todos os agentes. Essa divulgação é referida genericamente como "anúncio público"; porém, não precisa consistir, a rigor, em um anúncio típico, podendo ser um evento percebido simultaneamente por todos os agentes, contanto que cada agente saiba que todos os agentes estão acessando essa informação juntos, e que todos saibam desse mesmo fato, etc. A lógica do anúncio público apresenta pelo menos duas especificidades, não necessariamente preservadas por suas extensões que incluam outras ações epistêmicas: trata-se de uma lógica funcional (quando um anúncio for exequível, haverá somente uma maneira de fazê-lo) e dispensa o emprego de definições e provas por dupla indução (não há necessidade de se definir fórmulas e ações como duas categorias distintas e mutuamente dependentes de expressões da linguagem). Alguns trabalhos foram publicados sobre essa lógica, explorando diferentes axiomatizações, tratamentos semânticos e extensões; entretanto, quase todos se dedicam exclusivamente ao nível proposicional. Em nossa pesquisa bibliográfica, encontramos somente um artigo que desenvolve satisfatoriamente uma versão de primeira ordem para a lógica do anúncio público (KISHIDA, K. Public announcements under sheaves. In: New Frontiers in Artificial Intelligence, p. 96-108, 2013, ISBN 978-3-642-39930-5). Contudo, apesar da extrema sofisticação e elevado rigor técnico encontrados naquele trabalho, seu tratamento considera linguagens com anúncios públicos contendo somente fórmulas fechadas (sentenças), bem como um único agente epistêmico. Além disso, sua semântica, uma combinação de semântica de vizinhanças com semântica de feixes, motivada por um interesse filosófico bem específico (a interpretação intuitiva do operador epistêmico usual como representando conhecimento verificável), pode ser vista como desnecessariamente complicada se estamos interessados em uma interpretação standard para aquele operador, além de comprometer-se com uma perspectiva (um tanto polêmica) de contrapartes individuais, segundo a qual o mesmo objeto do domínio de interpretação não pode estar associado a mais de um ponto no modelo. Nossa contribuição propõe duas famílias, por assim dizer, de extensões de primeira ordem para a lógica do anúncio público, para quaisquer conjuntos finitos não-vazios de agentes epistêmicos e para anúncios contendo quaisquer fórmulas de suas respectivas linguagens. Os sistemas da primeira família estendem os correspondentes sistemas epistêmicos estáticos, providos com os usuais operadores epistêmicos para agentes individuais; e os da segunda fazem o mesmo com seus correspondentes sistemas estáticos, os quais, além de operadores epistêmicos individuais, adotam operadores de conhecimento distribuído em grupos de agentes. Além disso, nosso framework é o tradicional (modelos relacionais), o que simplifica consideravelmente o tratamento do assunto e não se compromete com indivíduos world-bounded. Antes de construir aquelas extensões dinâmicas, dedicamos alguns capítulos ao estudo dos vários sistemas epistêmicos estáticos que servirão como lógicas de base para nossa lógica do anúncio público, inclusive detalhando sistemas epistêmicos com conhecimento distribuído, e mostramos a completude em cada caso. Em se tratando de lógica epistêmica de primeira ordem, também fazemos brevemente uma defesa filosófica do emprego de quantificadores atualistas na lógica modal, com curiosos resultados relacionados com os esquemas conhecidos como Fórmula de Barcan e sua recíproca.<br>

Abstract : Among multimodal logics, Dynamic Epistemic Logic has been developed for modelling changes in epistemic states for groups of agents. Inspired by resources from Dynamic Logic (designed for dealing with computational programs), Dynamic Epistemic Logic manages to represent the very transition between epistemic states, either individual or collective, involving relevant agents. That transition might be caused by several epistemic actions (ex., sharing privately an information with a person or group). The simplest (and earliest) version for that logic became known as Public Announcement Logic, which considers a single type of epistemic action: a public and simultaneous disclosure of an information for all agents. This disclosure is generically referred as a "public announcement"; however, it doesn't have to be a typical announcement, and it might be an event, provided that this event be simultaneously realized by every agent, and that each agent knows that everybody is accessing that information together, and that everyone know this later fact, etc. Public Announcement Logic displays at least two peculiarities, not necessarily shared with its extensions including other epistemic actions: it's a functional logic (meaning that, when an announcement is feasible, there should be a unique way of doing it), and it dispenses with definitions and proofs based on double induction (i.e, there's no need for defining formulas and actions as two distinct and mutually dependent categories of language expressions). Some results have been published on this logic, exploring different axiomatizations, semantic treatments and extensions; however, almost all of them deal exclusively with propositional level. In our bibliographical survey, we found a single paper with a satisfactory study on first-order Public Announcement Logic (KISHIDA, K. Public announcements under sheaves. In: New Frontiers in Artificial Intelligence, p. 96-108, 2013, ISBN 978-3-642-39930-5). Nevertheless, in spite of its extreme refinement and high technical rigor, its approach is restricted to single-agent languages where announcements contain only closed formulas (sentences). Besides, its semantics, a combination of neighborhood semantics with sheaf semantics, motivated by a peculiar philosophical interest (the intuitive interpretation of the usual epistemic operator as representing verifiable knowledge), might be seen as unnecessarily complicated, especially if we are interested in the standard interpretation for that operator, and it forcibly commits itself with the (somewhat controversial) perspective of individual counterparts, according to which the same object in the interpretation domain must be uniquely associated to a point in the model. Our contribution provides two families, so to speak, of first-order extensions for Public Announcement Logic, for any non-empty finite sets of agents, as well as for announcements containing any formulas from their respective languages. The systems in the first family extend their correspondent static epistemic systems, containing the usual epistemic operators for individual agents; and the systems in the second one, do the same with their correspondent static systems, which, beside individual epistemic operators, include operators for distributed knowledge in groups of agents. Moreover, our framework is traditional (relational models), which considerably simplifies the approach and doesn't commit itself to world-bounded individuals. Before presenting those dynamic extensions, we dedicate a few chapters to the study of those static epistemic systems which shall be the basis for our Public Announcement Logic, also detailing some epistemic systems with distributed knowledge, and we prove completeness for each case. Concerning first-order epistemic logic, we additionally make a brief philosophical defense for actualist quantification in modal logic, with interesting results related to the schemes known as Barcan Formula and its converse.