Lógica do diálogo

Lógica do Diálogo (em alemão: dialogische Logik, traduzido como Lógica Dialógica) é uma abordagem para a semântica formal que fundamenta os conceitos de verdade e validade no escopo de teoria dos jogos, como a existência de uma estratégia de vitória para um jogador, que se assemelha, de certa forma, ao Diálogo socrático e à teoria das obligationes medieval. No final dos anos 50, Paul Lorenzen foi o primeiro a introduzir a Lógica do diálogo, posteriormente aprimorada por Kuno Lorenz. Quase ao mesmo tempo que Lorenzen, Jaakko Hintikka desenvolveu uma abordagel modelo-teórica conhecida na literatura como GTS.

Desde então, várias abordagens da Lógica do Diálogo têm sido estudadas pela lógica. Shahid Rahman (Lille) e colaboradores transformaram a dialógica em uma plataforma geral para o estudo de problemas lógicos e filosóficos relacionados ao pluralismo lógico. Por volta de 1995, isso iniciou uma forma de "Renascimento" que geraria resultados duradouros. Atualmente, essa nova filosofia impulsiona uma renovação paralela nos campos da Ciência da computação teórica, linguística computacional, inteligência artificial e da semântica formal das linguagens de programação iniciada pelo trabalho de Johan van Benthem e colaboradores em Amsterdam que analisaram profundamente a interface entre lógica e jogos. Novos resultados em lógica linear por J-Y. Girard nas interfaces entre teoria dos jogos matemática e lógica de um lado e teoria da argumentação e lógica do outro, resultaram no trabalho de muitos outros como S. Abramsky, J. van Benthem, A. Blass, D. Gabbay, M. Hyland, W. Hodges, R. Jagadeesan, G. Japaridze, E. Krabbe, L. Ong, H. Prakken, G. Sandu D. Walton, e J. Woods que puseram a Lógica do Diálogo no centro de um novo conceito na lógica em que esta é compreendida como um instrumento dinâmico de inferência.

Lógica Clássica

A aplicação mais simples da Lógica do Diálogo é a lógica proposicional. Cada fórmula dessa linguagem é interpretada como um jogo entre dois jogadores, chamados de "verificador" e "falsificador". Ao verificador é dada "propriedade" sobre todas as disjunções na fórmula, e ao falsificador é dada propriedade sobre todos as conjunções. Cada jogada consiste em permitir ao dono do conectivo predominante pegar um de seus ramos; a partida continua, então, com essa "sub-fórmula", com o jogador que é dono do conectivo predominante fazendo a jogada. O jogo termina quando uma proposição primitiva tiver sido escolhida pelos dois jogadores; o verificador é considerado o vencedor se a proposição resultante é verdadeira, e o falsificador vence se ela for falsa. A formula original será considerada verdadeira sempre que o "verificador" tiver uma estratégia de vitória, e falsa quando o falsificador tiver uma estratégia de vitória.

Se a fórmula contiver negações ou implicações, outras técnicas, mais complicadas, podem ser usadas. Por exemplo, a negação será verdade se o que está sendo negado é falso, então ela terá o efeito de troca de papéis entre os dois jogadores.

De forma mais genérica, a lógica do diálogo pode ser aplicada à Lógica de predicados; os novos papéis permitem que um quantificador dominante seja removido pelo seu "dono" (o verificador, no caso de quantificadores existenciais, ou o falsificador para quantificadores existenciais) e a variável ligada ao quantificador substituída em todas as suas ocorrências por um objeto de escolha do dono. Note que um contraexemplo seria suficiente para deixar falsa uma sentença universalmente quantificada, e o mesmo vale para verificar a validade de uma existencialmente quantificada. Assumindo o axioma da escolha, a lógica dialógica para a lógica de primeira ordem clássica coincide com a model-based (Tarskian) semantics.

Para a lógica clássica de primeira ordem, a estratégia de vitória para o verificador consiste, essencialmente, em encontrar funções Skolem e testemunhas adequadas. Por exemplo, se S denota $\forall x\exists y\,\phi (x,y)$ então uma sentença equisatisfatível para S é $\exists f\forall x\,\phi (x,f(x))$. A função Skolem f (se existir) codifica uma estratégia de vitória para o verificador de S, retornando uma sub-fórmula existencial testemunha para cada escolha de x que o falsificador fizer.

Atualmente, a formulação descrita acima é devido à interpretação-GTS de Jaakko Hintikka. A versão original da lógica clássica e intuicionista de Paul Lorenzen e Kuno Lorenz não foram definidas em relação a modelos, mas com a ajuda de estratégias de vitória sobre diálogos formais (P. Lorenzen, K. Lorenz 1978, S. Rahman and L. Keiff 2005).

Shahid Rahman e Tero Tulenheimo criaram um algoritmo para transofmar as estratégias de vitória GTS na lógica clássica em estratégias de vitória diálogicas e vice-versa. Todos esses jogos são de informação perfeita, ou seja, os dois jogadores sempre sabem os valores (verdadeiro ou falso) de cada primitiva, e sabem todas as jogadas anteriores.

Lógica intuicionista, semantica denotacional, lógica linear, pluralismo lógico

A motivação inicial para Lorenzen e Kuno Lorenz foi encontrar uma semantica dialógica para a lógica intuicionista. Andreas Blass foi o primeiro a apontar conexões entre a semântica dos jogos (ou dialógica) e a lógica linear. Esse linha foi posteriormente aprimorada por Samson Abramsky, Radhakrishnan Jagadeesan, Pasquale Malacaria e, independentemente, por Martin Hyland e Luke Ong, que deu uma enfâse especial em composicionalidade, i.e. a definição de estratégias indutivas na sintaxe. Usando semâtica dos jogos, os autores mencionados acima solucionaram o problema de longa data sobre a definição de um modelo completamente abstrato para as linguagens de programaçao PCF. Consequentemente, a semantica de jogos levou a modelos de semantica completamente abstratos para uma variedade de linguagens de programação e, novos métodos de verificação de softwares por checagem de modelos direcionados a semântica.

Shahid Rahman e Helge Rückert estenderam a abordagem dialógica ao estudo de várias lógicas não-clássicas com a lógica modal, lógica relevante, lógica livre e lógica conectiva. Recentemente, Rahman e colaboradores desenvolveram uma abordagem dialógica dentro de uma plataforma geral com o objetivo de discutir o pluralismo lógico.Os últimos trabalhos de Rahman e sua equipe em Lille envolvem uma abordagem dialógica da teoria construtiva de tipos de Per Martin-Löf, a fim de incluir diálogos envolvendo conteúdo ou idiomas totalmente interpretados. Essa abordagem foi aplicada a um grande conjunto de contextos, como, por exemplo; a elucidação o papel da dialética na silogística aristotélica, a demonstração do axioma de escolha dependente, ou o desenvolvimento de diálogos cooperativos para a argumentação jurídica.

Quantificadores

Considerações fundamentais da semântica de jogos foram enfatizadas por Jaakko Hintikka e Gabriel Sandu, especialmente para a uma lógica com quantificadores de ramificaçoes dentro de la Independence-friendly logic (IF). Foi pensado que o princípio da composicionalidade falha para essas lógicas, tanto que uma definição de verdade Tarskiana pode não proporcionar uma semântica adequada. Para resolver esse problema, foi dado aos quantificadores um significado teórico na lógica dialógica. Especificamente, a abordagem é a mesma da lógica clássica proposicional, com exceção de que os jogadores nem sempre tem informação perfeita sobre as jogadas anteriores do outro jogador. Wilfrid Hodges propôs uma semântica composicional e provou que ela é equivalente à semantica dos jogos para la lógica IF. Considerações fundamentais motivaram o trabalho de outos, como em lógica computacional de Japaridze'.

Mais recentemente e a equipe de lógica dialógica em Lille implementaram dependências e independências entre quantificadores (como no caso de quantificadores de ramificaçoes dentro da lógica IF) dentro de uma estrutura dialógica por meio de uma abordagem dialógica da teoria intuicionista do tipos chamada de "raciocínio imanente" .

Ver também

• Lógica Intuicionista
• Computação interativa
• Ludics

Referências

Artigos

• S. Abramsky and R.Jagadeesan, Games and full completeness for multiplicative linear logic. Journal of Symbolic Logic 59 (1994): 543-574.
• A. Blass, A game semantics for linear logic. Annals of Pure and Applied Logic 56 (1992): 151-166.
• D.R. Ghica, Applications of Game Semantics: From Program Analysis to Hardware Synthesis. 2009 24th

Annual IEEE Symposium on Logic In Computer Science: 17-26. ISBN 978-0-7695-3746-7.

• G. Japaridze, Introduction to computability logic. Annals of Pure and Applied Logic 123 (2003): 1-99.
• G. Japaridze, In the beginning was game semantics. In Ondrej Majer, Ahti-Veikko Pietarinen and Tero Tulenheimo (editors),

Games: Unifying logic, Language and Philosophy. Springer (2009).

• Krabbe, E. C. W., 2001. "Dialogue Foundations: Dialogue Logic Restituted [title has been misprinted as "...Revisited"]," Supplement to the Proceedings of The

Aristotelian Society 75: 33-49.

• S. Rahman and L. Keiff, On how to be a dialogician. In Daniel Vanderken (ed.), Logic Thought and Action, Springer (2005), 359-408. ISBN 1-4020-2616-1.
• S. Rahman and T. Tulenheimo, From Games to Dialogues and Back: Towards a General Frame for Validity. In Ondrej Majer, Ahti-Veikko Pietarinen and Tero

Tulenheimo (editors), Games: Unifying logic, Language and Philosophy. Springer (2009).

• Johan van Benthem (2003). «Logic and Game Theory: Close Encounters of the Third Kind». In: G. E. Mints; Reinhard Muskens. Games, logic, and constructive sets. [S.l.]: CSLI Publications. ISBN 978-1-57586-449-5 

Livros

• T. Aho and A-V. Pietarinen (eds.) Truth and Games. Essays in honour of Gabriel Sandu. Societas Philosophica Fennica (2006).ISBN 951-9264-57-4.
• J. van Benthem, G. Heinzmann, M. Rebuschi and H. Visser (eds.) The Age of Alternative Logics. Springer (2006).ISBN 1-40-20-5011-4.
• R. Inhetveen: Logik. Eine dialog-orientierte Einführung., Leipzig 2003 ISBN 3-937219-02-1
• L. Keiff Le Pluralisme Dialogique. Thesis Université de Lille3(2007).
• K. Lorenz, P. Lorenzen: Dialogische Logik, Darmstadt 1978
• P. Lorenzen: Lehrbuch der konstruktiven Wissenschaftstheorie, Stuttgart 2000 ISBN 3-476-01784-2
• O. Majer, A.-V. Pietarinen and T. Tulenheimo (editors). Games: Unifying Logic, Language and Philosophy. Springer (2009).
• S. Rahman, Über Dialogue protologische Kategorien und andere Seltenheiten. Frankfurt 1993 ISBN 3-631-46583-1
• S. Rahman and H. Rückert (editors), New Perspectives in Dialogical Logic. Synthese 127 (2001) ISSN 0039-7857.
• S. Rahman and N. Clerbout: Linking Games and Constructive Type Theory: Dialogical Strategies, CTT-Demonstrations and the Axiom of Choice. Springer-Briefs (2015).https://www.springer.com/gp/book/9783319190624
• S. Rahman, Z. McConaughey, A. Klev, N. Clerbout: Immanent Reasoning and the Dialogical Approach to Constructive Type Theory. A Plaidoyer for the Play level. Springer (2018).https://www.springer.com/gp/book/9783319911489

Ligações externas

• Computability Logic Homepage
• GALOP: Workshop on Games for Logic and Programming Languages
• Game Semantics or Linear Logic?
• Stanford Encyclopedia of Philosophy entry on Logic and Games
• SEP entry on Dialogical Logic