# 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 ($\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 ( $\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.

## Semântica

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.

## Lógica IF expandida

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 $\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".

## Propriedades e críticas

Um número de propriedades da lógica IF segue da equivalência lógica com $\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$^2$). Posteriormente Väänänen mostrou que Val$^2$ é o Π$_2$-definível conjunto completo de integrais, e que é Val$^2$ não em $\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 | $\Sigma _{1}^{0}$ (r.e.) | $\Pi _{2}$ |
| Não-validade | $\Pi _{1}^{0}$ (co-r.e.) | $\Sigma _{2}$ |
| Consistência | $\Pi _{1}^{0}$ | $\Pi _{1}^{0}$ |
| Inconsistencia | $\Sigma _{1}^{0}$ | $\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 $\Pi _{1}^{1}$ não admitem uma interpretação na teoria dos jogos.

## Veja também

* Lógica do diálogo