Lógica de independência amigável

Lógica de independência amigável (do inglês Independence-Friendly, Lógica IF), proposta por Jaakko Hintikka e Gabriel Sandu em 1989, objetiva ser uma alternativa mais natural e intuitiva à clássica lógica de primeira ordem (FOL). Lógica do SE é caracterizada por quantificadores ramificados. Esta é mais expressiva que FOL porque permite que sejam expressas relações independentes entre variáveis quantificadas.

Por exemplo, a fórmula ∀a ∀b ∃c/b ∃d/a φ(a,b,c,d) ("x/y" deve ser lida como "x independente de y") não pode ser expressa em FOL. Isso é porque c depende apenas de a, e d depende apenas de b. Lógica de primeira ordem não pode expressar esses independências por qualquer reordenação linear de quantificadores. Em parte, a lógica do SE foi motivada pela semântica de jogos para jogos com Informação perfeita.

A lógica IF é a tradução equivalente a lógica de segunda ordem existencial (${\displaystyle \Sigma _{1}^{1}}$) e também com dependência lógica de Väänänen e com a lógica de primeira ordem estendida com quantificadores de Henkin. Embora compartilhe várias propriedades meta lógicas com a lógica de primeira ordem, existem algumas diferenças, incluindo a falta de fechamento sob negação e uma complexidade superior para decidir a validade das fórmulas. A lógica IF expandida remete ao problema do fecho, mas sacrifica a semântica de jogos no processo, e isso pertence propriamente a um fragmento superior da lógica de segunda ordem ( ${\displaystyle \Delta _{2}^{1}}$).

A proposição de Hintikka de que a lógica IF e sua versão estendida ser usada como fundações da matemática tem sido visto com ceticismo por outros matemáticos, incluindo Väänänen e Solomon Feferman.

Já que a semântica Tarskiana não permite valores verdade indeterminados, não pode ser usada para a lógica do SE. Hintikka argumenta ainda que o padrão da semântica de FOL não pode acomodar a lógica IF por que o principio da composicionalidade falha posteriormente. Wilfrid Hodges (1997) nos dá uma semântica composicional para isso em parte por quantificar as cláusulas verdade para fórmulas SE sobre os conjuntos de atribuições, em vez de apenas atribuições (como as cláusulas verdade usuais fazem).

A semântica da teoria dos jogos para FOL trata as fórmulas FOL como um jogo de informação perfeita, na qual os jogadores são Verificador e Falsificador. O mesmo se aplica para a semântica padrão da lógica IF, exceto que os jogos são de informação imperfeita.

Relações de independência entre as variáveis quantificadas são modeladas na arvore do jogo como relações indistinguíveis entre estados de jogo com respeito a um determinado jogador. Em outras palavras, os jogadores não estão certos sobre onde eles estão na arvore (esta ignorância simula um jogo simultâneo). A formula é avaliada como verdadeira se o Verificador tem uma estratégia vencedora, e falso se o Falsificador tem uma estratégia vencedora, e indeterminável caso contrário.

Uma estratégia vencedora é informalmente definida como uma estratégia na qual é garantido vencer o jogo, independentemente de como os outros jogadores jogarem. Para isso pode ser dada uma definição completamente rigorosa e formal.

A lógica IF não é fechada sob a negação clássica. O fecho booleano da lógica IF é conhecido como lógica IF expandida e é equivalente a um fragmento de ${\displaystyle \Delta _{2}^{1}}$ (Figueira et al. 2011). Hintikka (1996, p. 196) diz que "virtualmente tudo da matemática clássica pode, a princípio, ser feito com a lógica de primeira ordem IF expandida".

Um número de propriedades da lógica IF segue da equivalência lógica com ${\displaystyle \Sigma _{1}^{1}}$ e se aproxima da lógica de primeira ordem incluindo o Teorema da compacidade, o Teorema de Löwenheim–Skolem, e o teorema de interpolação de Craig. (Väänänen, 2007, p. 86) Entretanto, Väänänen (2001) provou que o conjunto de números de Gödel de sentenças válidas da lógica IF com pelo menos um símbolo de predicado binário (conjunto denotado por Val_IF) é recursivamente isomorfo com o conjunto correspondente de números de Gödel de sentenças de segunda ordem válidas (completas) em um vocabulário que contém um símbolo de predicado binário (conjunto denotado por Val²). Posteriormente Väänänen mostrou que Val² é o Π₂-definível conjunto completo de integrais, e que é Val² não em ${\displaystyle \Sigma _{n}^{m}}$ para qualquer m e n finitos. Väänänen (2007, pp. 136-139) sumariza a complexidade dos resultados do seguinte modo:

Problema	lógica de primeira ordem	IF/depedencia/Lógica ESO
Decisão	${\displaystyle \Sigma _{1}^{0}}$ (r.e.)	${\displaystyle \Pi _{2}}$
Não-validade	${\displaystyle \Pi _{1}^{0}}$ (co-r.e.)	${\displaystyle \Sigma _{2}}$
Consistência	${\displaystyle \Pi _{1}^{0}}$	${\displaystyle \Pi _{1}^{0}}$
Inconsistencia	${\displaystyle \Sigma _{1}^{0}}$	${\displaystyle \Sigma _{1}^{0}}$

Feferman (2006) cita o resultado de Väänänen 2001 para discutir (contra Hintikka) que enquanto a satisfatibilidade pode ser um problema de primeira ordem, a questão de quando terá uma estratégia vencedora para o Verificador sobre todas as estruturas em geral "nos leva exatamente na lógica de segunda ordem completa" (enfatiza Feferman). Feferman também atacou a dita utilidade da lógica IF expandida, porque as sentenças em ${\displaystyle \Pi _{1}^{1}}$ não admitem uma interpretação na teoria dos jogos.

• Lógica do diálogo

• Hintikka, Jaakko and Gabriel Sandu (1989), "Informational independence as a semantical phenomenon", in Logic, Methodology and Philosophy of Science VIII (J. E. Fenstad, et al., eds.), North-Holland, Amsterdam, doi:10.1016/S0049-237X(08)70066-1
• Jaakko Hintikka, 1996, The Principles of Mathematics Revisited, Cambridge University Press, ISBN 978-0-521-62498-5
• Jaakko Hintikka and Gabriel Sandu, "Game-theoretical semantics", in Handbook of logic and language, ed. J. van Benthem and A. ter Meulen, Elsevier 1996 (1st ed.) Updated in the 2nd second edition of the book (2011).
• Wilfrid Hodges, 1997, 'Compositional semantics for a language of imperfect information'. Journal of the IGPL 5: 539–563.
• Daniel Kolak, On Hintikka, Belmont: Wadsworth 2001 ISBN 0-534-58389-X
• Väänänen, J. (2001). «Second-Order Logic and Foundations of Mathematics». Bulletin of Symbolic Logic. 7 (4): 504–520. JSTOR 2687796. doi:10.2307/2687796 
• Jaakko Hintikka, "Hyperclassical logic (a.k.a. IF logic) and its implications for logical theory", Bulletin of Symbolic Logic 8, 2002, 404-423
• Matti Eklund and Daniel Kolak, “Is Hintikka’s Logic First Order?” Synthese, 131(3): 371-388 June 2002
• Janssen, Theo M. V. "Independent choices and the interpretation of IF logic." Journal of Logic, Language and Information, Volume 11 Issue 3, Summer 2002, pp. 367-387 doi:10.1023/A:1015542413718
• Daniel Kolak and John Symons, "The Results are In: The Scope and Import of Hintikka’s Philosophy" in Daniel Kolak and John Symons, eds., Quantifiers, Questions, and Quantum Physics. Essays on the Philosophy of Jaakko Hintikka, Springer 2004, pp. 205-268 ISBN 1-4020-3210-2, doi:10.1007/978-1-4020-32110-0_11
• Solomon Feferman, "What kind of logic is “Independence Friendly” logic?", in The Philosophy of Jaakko Hintikka (Randall E. Auxier and Lewis Edwin Hahn, eds.); Library of Living Philosophers vol. 30, Open Court (2006), 453-469.
• Jouko Väänänen, 2007, 'Dependence Logic -- A New Approach to Independence Friendly Logic', Cambridge University Press, ISBN 978-0-521-87659-9
• Allen L. Mann, Gabriel Sandu, Merlijn Sevenster (2011) Independence-Friendly Logic. A Game-Theoretic Approach, Cambridge University Press, ISBN 0521149347
• Santiago Figueira, Daniel Gorín, and Rafael Grimson "On the Expressive Power of IF-Logic with Classical Negation", WoLLIC 2011 proceedings, pp. 135-145, ISBN 978-3-642-20919-2

• Tero Tulenheimo, 2009. 'Independence friendly logic'. Stanford Encyclopedia of Philosophy.
• Wilfrid Hodges, 2009. 'Logic and Games'. Stanford Encyclopedia of Philosophy.
• IF logic em Planet Math