124. Lógica IF (independence-friendly)

Idea central

La lógica IF parte de una asimetría de la sintaxis de primer orden: el orden lineal de los cuantificadores obliga a que cada cuantificador dependa de todos los que lo preceden. No se puede escribir, por ejemplo, «para todo \(x\) hay un \(y\), y para todo \(z\) hay un \(w\) que depende solo de \(z\)». Henkin (1961) había introducido cuantificadores ramificados para expresar esas dependencias parciales. Hintikka y Sandu generalizaron la idea con una notación de barra: \((\exists y/\forall x)\) indica que la elección de \(y\) se hace sin conocer el valor de \(x\). El gesto distintivo es semántico: la verdad se define mediante juegos entre un verificador y un falsador, y la independencia se interpreta como información imperfecta. Hintikka sostuvo que esta, y no la de Frege y Russell, es la verdadera lógica elemental.

Principios, axiomas y reglas de inferencia

Sintaxis. Fórmulas de primer orden en forma normal de negación, con cuantificadores y conectivas que pueden llevar un conjunto de variables tras la barra: \((\exists y/W)\), \((\lor/W)\), donde \(W\) es un conjunto de variables de las que el movimiento es independiente. La negación \(\sim\) es dual (intercambia los papeles de los jugadores), no la negación contradictoria.

Semántica de juegos (Hintikka, 1968; para IF, Hintikka y Sandu, 1989). Dado un modelo \(M\), un enunciado \(\varphi\) y una asignación:

• \(\forall x\,\psi\): el falsador elige un valor para \(x\).
• \(\exists x\,\psi\): el verificador elige un valor para \(x\).
• \(\psi \land \chi\): el falsador elige un conyunto; \(\psi \lor \chi\): el verificador elige.
• \(\sim\psi\): los jugadores intercambian papeles.
• Atómica: gana el verificador si es verdadera en \(M\).
• Un movimiento \((\exists y/W)\) se hace sin conocer los valores elegidos para las variables de \(W\).

\(\varphi\) es verdadero si el verificador tiene estrategia ganadora; falso si la tiene el falsador; indeterminado si ninguno.

Skolemización. Un enunciado IF es verdadero si y solo si su forma de Skolem, en la que la función testigo de \(y\) no toma como argumentos las variables de \(W\), es satisfacible en \(M\). Así \(\forall x \forall z (\exists y/\forall z)(\exists w/\forall x)\,\varphi\) equivale a \(\exists f \exists g\, \forall x \forall z\, \varphi(x, f(x), z, g(z))\), que es el cuantificador de Henkin.

Ejemplo. En un dominio con al menos dos elementos, \(\forall x (\exists y/\forall x)\, x = y\) no es verdadero (el verificador tendría que acertar \(x\) sin conocerlo) ni falso (el falsador no puede ganar con seguridad si el verificador puede elegir cualquier \(y\)). Su «negación» \(\sim\) tampoco es verdadera. El tercio excluso falla.

Metateoría.

• Expresividad: IF equivale a la lógica existencial de segundo orden (\(\Sigma^1_1\)), resultado que procede de Enderton (1970) y Walkoe (1970) para cuantificadores ramificados.
• Valen la compacidad y el teorema de Löwenheim–Skolem descendente, heredados de \(\Sigma^1_1\).
• Puede expresar enunciados que no son de primer orden: «el dominio es infinito», «hay tantos \(P\) como \(Q\)».
• El conjunto de enunciados válidos no es recursivamente enumerable, y no hay cálculo completo.
• Definición de la verdad: en IF aritmética existe un predicado que define la verdad de los enunciados IF del propio lenguaje (Hintikka 1996). No contradice a Tarski, porque la negación contradictoria no está disponible dentro del lenguaje.

Semántica composicional (Hodges, 1997). Las fórmulas se evalúan en conjuntos de asignaciones (trumps, luego «equipos»), no en asignaciones individuales. Cameron y Hodges probaron que no hay semántica composicional basada en asignaciones individuales. De ahí salió la lógica de dependencia de Väänänen (2007).

Genealogía

La lógica IF extiende la sintaxis de la lógica de primer orden clásica: sin barras, coincide con ella, y la lectura de juegos reproduce entonces la definición de verdad habitual. Recibe su semántica de la tradición de los juegos: la semántica de juegos de Hintikka (finales de los sesenta), paralela a la lógica dialógica de Lorenzen pero centrada en la verdad y no en la prueba, proporciona el marco en que la independencia se lee como información imperfecta. Con la semántica tarskiana la relación es de reacción: Hintikka presentó la lógica IF como una lógica capaz de definir su propia verdad y, por tanto, como argumento contra la necesidad de la jerarquía de metalenguajes de Tarski y contra la tesis de que la verdad es indefinible en el propio lenguaje.

Contexto y relevancia

Hintikka defendió en The Principles of Mathematics Revisited (1996) que la lógica IF debía sustituir a la de primer orden como lógica básica, que permitía reconstruir parte de la matemática sin teoría de conjuntos y que hacía innecesaria la lógica de segundo orden. La recepción fue más cauta: Feferman, Väänänen y otros señalaron que la definición de verdad depende de una negación débil y que la lógica IF se comporta como un fragmento de segundo orden encubierto. Técnicamente su legado principal es la lógica de equipos. Para la pregunta «¿una lógica o muchas?» aporta un caso en que el tercio excluso falla no por consideraciones constructivistas o de vaguedad, sino por la estructura de la información en un juego. La elección entre bivalencia y su abandono aparece ligada a qué dependencias se quieren expresar.

Fuentes

• Jaakko Hintikka y Gabriel Sandu, «Informational independence as a semantical phenomenon», en J. E. Fenstad et al. (eds.), Logic, Methodology and Philosophy of Science VIII, Ámsterdam, North-Holland, 1989, 571–589.
• Jaakko Hintikka, The Principles of Mathematics Revisited, Cambridge University Press, 1996.
• Wilfrid Hodges, «Compositional semantics for a language of imperfect information», Logic Journal of the IGPL 5 (1997), 539–563.
• Allen L. Mann, Gabriel Sandu y Merlijn Sevenster, Independence-Friendly Logic: A Game-Theoretic Approach, Cambridge University Press, 2011.

← Índice de lógicas