Lógica favorable a la independencia

El juego semántico${\displaystyle G(\varphi ,{\mathcal {M}},s)}$Tiene dos jugadores, llamados Eloise (o Verificadora) y Abelardo (o Falsificador).

Los movimientos permitidos en el juego semántico${\displaystyle G(\varphi ,{\mathcal {M}},s)}$están determinadas por la estructura sintáctica de la fórmula en consideración. Para simplificar, primero asumimos que${\displaystyle \varphi }$está en forma normal de negación, con símbolos de negación que aparecen solo delante de las subfórmulas atómicas.

1. Si${\displaystyle \varphi }$es literal, el juego termina y, si${\displaystyle \varphi }$es cierto en${\displaystyle {\mathcal {M}}}$(en el sentido de primer orden), entonces gana Eloísa; de lo contrario, gana Abelardo.
2. Si${\displaystyle \varphi =\psi _{1}\land \psi _{2}}$, entonces Abelardo elige una de las subfórmulas${\displaystyle \psi _{i}}$y el juego correspondiente${\displaystyle G(\psi _ {i},{\mathcal {M}},s)}$se juega.
3. Si${\displaystyle \varphi =\psi _{1}\lor \psi _{2}}$, entonces Eloises elige una de las subfórmulas${\displaystyle \psi _{i}}$y el juego correspondiente${\displaystyle G(\psi _ {i},{\mathcal {M}},s)}$se juega.
4. Si${\displaystyle \varphi =(\forall v/V)\psi }$, entonces Abelardo elige un elemento${\displaystyle a}$de${\displaystyle {\mathcal {M}}}$y juego${\displaystyle G(\psi ,{\mathcal {M}},s(a/v))}$se juega.
5. Si${\displaystyle \varphi =(\existe v/V)\psi }$, entonces Eloise elige un elemento${\displaystyle a}$de${\displaystyle {\mathcal {M}}}$y juego${\displaystyle G(\psi ,{\mathcal {M}},s(a/v))}$se juega.

En términos más generales, si${\displaystyle \varphi }$no está en forma normal de negación, podemos afirmar, como regla para la negación, que, cuando un juego${\displaystyle G(\lnot \varphi ,{\mathcal {M}},s)}$Cuando se alcanza ese nivel, los jugadores comienzan a jugar un juego doble.${\displaystyle G^{*}(\varphi,{\mathcal {M}},s)}$en la que se intercambian los roles de Verificadores y Falsificadores.

De manera informal, una secuencia de movimientos en un juego.${\displaystyle G(\varphi ,{\mathcal {M}},s)}$es una historia. Al final de cada historia${\displaystyle h}$, algún subjuego${\displaystyle G(\psi _{h},{\mathcal {M}},s_{h})}$se juega; llamamos${\displaystyle s_{h}}$la asignación asociada a${\displaystyle h}$, y${\displaystyle \psi _{h}}$la ocurrencia de la subfórmula asociada a${\displaystyle h}$. El jugador asociado a${\displaystyle h}$¿Es Eloise en caso de que el operador lógico más externo en${\displaystyle \psi _{h}}$es${\displaystyle \lor }$o${\displaystyle \exists }$y Abelardo en caso de que sea${\displaystyle \land }$o${\displaystyle \forall }$.

El conjunto${\displaystyle h}$de movimientos permitidos en una historia${\displaystyle h}$es${\displaystyle {\mathcal {M}}}$si el operador más externo de${\displaystyle \psi _{h}}$es${\displaystyle \exists }$o${\displaystyle \forall }$; es${\displaystyle \{L,R\}}$(${\displaystyle L,R}$siendo cualesquiera dos objetos distintos, que simbolizan 'izquierda' y 'derecha') en caso de que el operador más externo de${\displaystyle \psi _{h}}$es${\displaystyle \lor }$o${\displaystyle \land }$.

Dadas dos tareas${\displaystyle s,t}$del mismo dominio y${\displaystyle V\subseteq dom(s)}$escribimos${\displaystyle s\sim _{V}t}$si${\displaystyle s(w)=t(w)}$en cualquier variable${\displaystyle w\in dom(s)\setminus V}$.

La información imperfecta se introduce en los juegos al estipular que ciertas historias son indistinguibles para el jugador asociado; se dice que las historias indistinguibles forman un "conjunto de información". Intuitivamente, si la historia${\displaystyle h}$está en el conjunto de información${\displaystyle I}$, el jugador asociado a${\displaystyle h}$no sabe si está en${\displaystyle h}$o en alguna otra historia de${\displaystyle I}$Consideremos dos historias.${\displaystyle h,h'}$de tal manera que el asociado${\displaystyle \psi _{h},\psi _{h'}}$son ocurrencias idénticas de subfórmulas de la forma${\displaystyle (Qv/V)\chi }$(${\displaystyle Q=\exists }$o${\displaystyle \forall }$); si además${\displaystyle s_{h}\sim _{V}s_{h'}}$, escribimos${\displaystyle h\sim _{\exists }h'}$(En caso${\displaystyle Q=\exists }$) o${\displaystyle h\sim _{\forall }h'}$(En caso${\displaystyle Q=\forall }$), para especificar que las dos historias son indistinguibles para Eloísa, respectivamente, para Abelardo. También estipulamos, en general, la reflexividad de esta relación: si${\displaystyle \psi =\chi _{1}\lor \chi _{2}}$, entonces${\displaystyle h\sim _{\exists }h'}$; y si${\displaystyle \psi =\chi _{1}\land \chi _{2}}$, entonces${\displaystyle h\sim _{\forall }h'}$.

Para un juego amañado${\displaystyle G(\varphi ,{\mathcal {M}},s)}$, escribir${\displaystyle H_{\exists }}$para el conjunto de historias con las que Eloise está asociada, y de manera similar${\displaystyle H_{\forall }}$para el conjunto de historias de Abelardo.

Una estrategia para Eloise en el juego${\displaystyle G(\varphi ,{\mathcal {M}},s)}$es cualquier función que asigna, a cualquier posible historial en el que sea el turno de Eloise de jugar, un movimiento legal; más precisamente, cualquier función${\displaystyle \sigma :H_{\exists }\rightarrow \prod _{h\in H_{\exists }}A(h)}$de tal manera que${\displaystyle \sigma (h)\in A(h)}$para cada historia${\displaystyle h\in H_{\exists }}$Las estrategias de Abelardo pueden definirse de forma dual.

Una estrategia para Eloise es uniforme si, siempre que${\displaystyle h\sim _{\exists }h'}$,${\displaystyle \sigma (h)=\sigma (h')}$; para Abelardo, si${\displaystyle h\sim _{\forall }h'}$implica${\displaystyle \sigma (h)=\sigma (h')}$.

Una estrategia${\displaystyle \sigma }$para Eloise es ganar si Eloise gana en cada historial de terminal que se puede alcanzar jugando de acuerdo con${\displaystyle \sigma }$. Lo mismo ocurre con Abelardo.

Una sentencia IF${\displaystyle \varphi }$es cierto en una estructura${\displaystyle {\mathcal {M}}}$(${\displaystyle {\mathcal {M}}\models _{GTS}^{+}\varphi }$) si Eloise tiene una estrategia ganadora uniforme en el juego${\displaystyle G(\varphi ,{\mathcal {M}},\emptyset )}$Es falso (${\displaystyle {\mathcal {M}}\models _{GTS}^{-}\varphi }$) si Abelardo tiene una estrategia ganadora. Es indeterminado si ni Eloísa ni Abelardo tienen una estrategia ganadora.

La semántica de la lógica IF así definida es una extensión conservadora de la semántica de primer orden, en el siguiente sentido. Si${\displaystyle \varphi }$es una sentencia IF con conjuntos de barras vacías, asocie a ella la fórmula de primer orden${\displaystyle \varphi '}$que es idéntico a él, excepto en que cada cuantificador IF${\displaystyle (Qv/\emptyset )}$se reemplaza por el cuantificador de primer orden correspondiente${\displaystyle Qv}$. Entonces${\displaystyle {\mathcal {M}}\models _{GTS}^{+}\varphi }$si y solo si${\displaystyle {\mathcal {M}}\models \varphi '}$en el sentido tarskiano; y${\displaystyle {\mathcal {M}}\models _{GTS}^{-}\varphi }$si y solo si${\displaystyle {\mathcal {M}}\not \models \varphi '}$en el sentido tarskiano.

Se pueden utilizar juegos más generales para asignar un significado a fórmulas IF (posiblemente abiertas); más exactamente, es posible definir qué significa para una fórmula IF.${\displaystyle \varphi }$estar satisfecho, en una estructura${\displaystyle {\mathcal {M}}}$, por un equipo${\displaystyle X}$(un conjunto de asignaciones de dominio de variable común)${\displaystyle dom(X)}$y codominio${\displaystyle {\mathcal {M}}}$). Los juegos asociados${\displaystyle G(\varphi ,M,X)}$comenzar con la elección aleatoria de una asignación${\displaystyle s\in X}$; después de este movimiento inicial, el juego ${\displaystyle G(\varphi ,M,s)}$se juega. La existencia de una estrategia ganadora para Eloise define la satisfacción positiva (${\displaystyle M,X\models _{GTS}^{+}\varphi }$), y la existencia de una estrategia ganadora para Abelardo define la satisfacción negativa (${\displaystyle M,X\models _{GTS}^{-}\varphi }$). A este nivel de generalidad, la semántica de la teoría de juegos puede ser reemplazada por un enfoque algebraico, la semántica de equipos (definida más adelante).

Dada una fórmula IF${\displaystyle \varphi }$, primero definimos su skolemización relativizada a un conjunto finito${\displaystyle U\supseteq {\mbox{Free}}(\varphi )}$de variables. Para cada cuantificador existencial${\displaystyle (\exists v/V)}$ocurriendo en${\displaystyle \varphi }$, dejar${\displaystyle f_{v}}$sea ​​un nuevo símbolo de función (una "función de Skolem"). Escribimos${\displaystyle Subst(\varphi ,v,t)}$para la fórmula que se obtiene sustituyendo, en${\displaystyle \varphi }$, todas las ocurrencias libres de la variable${\displaystyle v}$con el término${\displaystyle t}$. La skolemización de${\displaystyle \varphi }$relativo a${\displaystyle U}$, denotado${\displaystyle {\mbox{Sk}}_{U}(\varphi )}$, se define mediante las siguientes cláusulas inductivas:

1. ${\displaystyle \operatorname {Sk} _{U}(\varphi )=\varphi }$si${\displaystyle \varphi }$es literal.
2. ${\displaystyle \operatorname {Sk} _{U}(\psi \lor \chi )=\operatorname {Sk} _{U}(\psi )\lor \operatorname {Sk} _{U}(\chi )}$.
3. ${\displaystyle \operatorname {Sk} _{U}(\psi \land \chi )=\operatorname {Sk} _{U}(\psi )\land \operatorname {Sk} _{U}(\chi )}$.
4. ${\displaystyle \operatorname {Sk} _{U}((\forall v/V)\psi )=\forall v\operatorname {Sk} _{U\cup \{v\}}(\psi )}$.
5. ${\displaystyle \operatorname {Sk} _{U}((\exists v/V)\psi )=Subst(\operatorname {Sk} _{U\cup \{v\}}(\psi ),v,f_{v}(y_{1},...,y_{n}))}$, dónde${\displaystyle y_{1},...,y_{n}}$es una lista de las variables en${\displaystyle U\setminus V}$.

Si${\displaystyle \varphi }$es una sentencia IF, su skolemización (no relativizada) se define como${\displaystyle {\mbox{Sk}}(\varphi )={\mbox{Sk}}_{\varnothing }(\varphi )}$.

Dada una fórmula IF${\displaystyle \varphi }$, asociar, a cada cuantificador universal${\displaystyle (\forall v/V)}$que aparece en él, un nuevo símbolo de función${\displaystyle g_{v}}$(una "función Kreisel"). Entonces, la Kreiselización${\displaystyle {\mbox{Kr}}_{U}(\varphi )}$de${\displaystyle \varphi }$en relación con un conjunto finito de variables${\displaystyle U\supseteq {\mbox{Free}}(\varphi )}$, se define mediante las siguientes cláusulas inductivas:

1. ${\displaystyle \operatorname {Kr} _{U}(\varphi )=\lnot \varphi }$si${\displaystyle \varphi }$es literal.
2. ${\displaystyle \operatorname {Kr} _{U}(\psi \land \chi )=\operatorname {Kr} _{U}(\psi )\lor \operatorname {Kr} _{U}(\chi )}$.
3. ${\displaystyle \operatorname {Kr} _{U}(\psi \lor \chi )=\operatorname {Kr} _{U}(\psi )\land \operatorname {Kr} _{U}(\chi )}$.
4. ${\displaystyle \operatorname {Kr} _{U}((\forall v/V)\psi )=Subst(\operatorname {Kr} _{U\cup \{v\}}(\psi ),v,g_{v}(y_{1},...,y_{n}))}$, dónde${\displaystyle y_{1},...,y_{n}}$es una lista de las variables en${\displaystyle U\setminus V}$.
5. ${\displaystyle \operatorname {Kr} _{U}((\exists v/V)\psi )=\forall v\operatorname {Kr} _{U\cup \{v\}}(\psi )}$

Si${\displaystyle \varphi }$es una sentencia IF, su Kreiselización (no relativizada) se define como${\displaystyle {\mbox{Kr}}(\varphi )={\mbox{Kr}}_{\varnothing }(\varphi )}$.

Dada una sentencia IF${\displaystyle \varphi }$con${\displaystyle n}$cuantificadores existenciales, una estructura${\displaystyle {\mathcal {M}}}$y una lista${\displaystyle {\vec {f}}}$de${\displaystyle n}$funciones de aridades apropiadas, las denotamos como${\displaystyle ({\mathcal {M}},{\vec {f}})}$la expansión de${\displaystyle {\mathcal {M}}}$que asigna las funciones${\displaystyle {\vec {f}}}$como interpretaciones para las funciones de Skolem de${\displaystyle \varphi }$.

Una sentencia IF es verdadera en una estructura${\displaystyle {\mathcal {M}}}$, escrito${\displaystyle {\mathcal {M}}\models _{\mbox{Sk}}^{+}\varphi }$, si hay una tupla${\displaystyle {\vec {f}}}$de funciones tales que${\displaystyle ({\mathcal {M}},{\vec {f}})\models {\mbox{Sk}}(\varphi )}$. Similarmente,${\displaystyle {\mathcal {M}}\models _{\mbox{Sk}}^{-}\varphi }$si hay una tupla${\displaystyle {\vec {f}}}$de funciones tales que${\displaystyle ({\mathcal {M}},{\vec {f}})\models {\mbox{Kr}}(\varphi )}$; y${\displaystyle {\mathcal {M}}\models _{\mbox{Sk}}^{0}\varphi }$si y solo si no se cumple ninguna de las condiciones anteriores.

Para cualquier sentencia IF, la semántica de Skolem devuelve los mismos valores que la semántica de la teoría de juegos.

Dejar ${\displaystyle {\mathcal {M}}}$ser una estructura y dejar${\displaystyle V=\{v_{1},\ldots ,v_{n}\}}$ser un conjunto finito de variables. Entonces un equipo más${\displaystyle {\mathcal {M}}}$con dominio${\displaystyle V}$es un conjunto de asignaciones sobre${\displaystyle {\mathcal {M}}}$con dominio${\displaystyle V}$, es decir, un conjunto de funciones${\displaystyle s}$de${\displaystyle V}$a${\displaystyle {\mathcal {M}}}$.

La duplicación y la suplementación son dos operaciones en equipos que están relacionadas con la semántica de la cuantificación universal y existencial .

1. Dado un equipo${\displaystyle X}$sobre una estructura${\displaystyle {\mathcal {M}}}$y una variable${\displaystyle v}$, el equipo de duplicación${\displaystyle X[{\mathcal {M}}/v]}$es el equipo${\displaystyle \{s(a/v)|s\in X,a\in {\mathcal {M}}\}}$. ^{[ 12 ]}
2. Dado un equipo${\displaystyle X}$sobre una estructura${\displaystyle {\mathcal {M}}}$, una función${\displaystyle F:X\rightarrow {\mathcal {M}}}$y una variable${\displaystyle v}$, el equipo de suplementación${\displaystyle X[F/v]}$es el equipo${\displaystyle \{s(F(s)/v)|s\in X\}}$.

Es habitual reemplazar las aplicaciones repetidas de estas dos operaciones con notaciones más concisas, como por ejemplo:${\displaystyle X[{\mathcal {M}}F/uv]}$para${\displaystyle (X[{\mathcal {M}}/u])[F/v]}$.

Como se indicó anteriormente, dadas dos asignaciones${\displaystyle s,t}$con el mismo dominio de variables, escribimos${\displaystyle s\sim _{V}t}$si${\displaystyle s(w)=t(w)}$para cada variable${\displaystyle w\in dom(s)\setminus V}$.

Dado un equipo${\displaystyle X}$en una estructura${\displaystyle {\mathcal {M}}}$y un conjunto finito${\displaystyle V}$de variables, decimos que una función${\displaystyle F:X\rightarrow {\mathcal {M}}}$es${\displaystyle V}$-uniforme si${\displaystyle F(s)=F(t)}$cuando sea${\displaystyle s\sim _{V}t}$.

La semántica de equipo es trivalente, en el sentido de que una fórmula puede resultar satisfactoria para un equipo en una estructura dada, negativamente satisfecha o ninguna de las dos. Las cláusulas semánticas para la satisfacción positiva y negativa se definen mediante inducción simultánea sobre la estructura sintáctica de las fórmulas IF.

Satisfacción positiva:

1. ${\displaystyle \!{\mathcal {M}},X\models ^{+}Rt_{1}\ldots t_{n}}$si y solo si , para cada asignación${\displaystyle s\in X}$,${\displaystyle \!{\mathcal {M}},s\models Rt_{1}\ldots t_{n}}$en el sentido de la lógica de primer orden (es decir, la tupla)${\displaystyle \!(s(t_{1})\ldots s(t_{n}))}$está en la interpretación${\displaystyle R^{\mathcal {M}}}$de${\displaystyle R}$).
2. ${\displaystyle \!{\mathcal {M}},X\models ^{+}t_{1}=t_{2}}$si y solo si, para cada asignación${\displaystyle s\in X}$,${\displaystyle \!{\mathcal {M}},s\models t_{1}=t_{2}}$en el sentido de la lógica de primer orden (es decir,${\displaystyle s(t_{1})=s(t_{2})}$).
3. ${\displaystyle \!{\mathcal {M}},X\models ^{+}\lnot \phi }$si y solo si${\displaystyle \!{\mathcal {M}},X\models ^{-}\phi }$.
4. ${\displaystyle \!{\mathcal {M}},X\models ^{+}\varphi \wedge \psi }$si y solo si${\displaystyle \!{\mathcal {M}},X\models ^{+}\varphi }$y${\displaystyle \!{\mathcal {M}},X\models ^{+}\psi }$.
5. ${\displaystyle \!{\mathcal {M}},X\models ^{+}\varphi \vee \psi }$si y solo si existen equipos${\displaystyle \!Y}$y${\displaystyle \!Z}$de tal manera que${\displaystyle X=Y\cup Z}$y${\displaystyle \!{\mathcal {M}},Y\models ^{+}\varphi }$y ${\displaystyle \!{\mathcal {M}},Z\models ^{+}\psi }$.
6. ${\displaystyle \!{\mathcal {M}},X\models ^{+}(\forall v/V)\varphi }$si y solo si${\displaystyle \!{\mathcal {M}},X[M/v]\models ^{+}\varphi }$.
7. ${\displaystyle \!{\mathcal {M}},X\models ^{+}(\exists v/V)\varphi }$si y solo si existe un${\displaystyle V}$-función uniforme${\displaystyle F:X\rightarrow M}$de tal manera que${\displaystyle \!{\mathcal {M}},X[F/v]\models ^{+}\phi }$.

Satisfacción negativa:

1. ${\displaystyle \!{\mathcal {M}},X\models ^{-}Rt_{1}\ldots t_{n}}$si y solo si, para cada asignación${\displaystyle s\in X}$, la tupla${\displaystyle \!(s(t_{1})\ldots s(t_{n}))}$no está en la interpretación${\displaystyle R^{\mathcal {M}}}$de${\displaystyle R}$.
2. ${\displaystyle \!{\mathcal {M}},X\models ^{-}t_{1}=t_{2}}$si y solo si, para cada asignación${\displaystyle s\in X}$, ${\displaystyle s(t_{1})\neq s(t_{2})}$.
3. ${\displaystyle \!{\mathcal {M}},X\models ^{-}\lnot \phi }$si y solo si${\displaystyle \!{\mathcal {M}},X\models ^{+}\phi }$.
4. ${\displaystyle \!{\mathcal {M}},X\models ^{-}\varphi \wedge \psi }$si y solo si existen equipos${\displaystyle \!Y}$y${\displaystyle \!Z}$de tal manera que${\displaystyle X=Y\cup Z}$y${\displaystyle \!{\mathcal {M}},Y\models ^{-}\varphi }$y ${\displaystyle \!{\mathcal {M}},Z\models ^{-}\psi }$.
5. ${\displaystyle \!{\mathcal {M}},X\models ^{-}\varphi \vee \psi }$si y solo si${\displaystyle \!{\mathcal {M}},X\models ^{-}\varphi }$y${\displaystyle \!{\mathcal {M}},X\models ^{-}\psi }$.
6. ${\displaystyle \!{\mathcal {M}},X\models ^{-}(\forall v/V)\varphi }$si y solo si existe un${\displaystyle V}$-función uniforme${\displaystyle F:X\rightarrow M}$de tal manera que${\displaystyle \!{\mathcal {M}},X[F/v]\models ^{-}\phi }$.
7. ${\displaystyle \!{\mathcal {M}},X\models ^{-}(\exists v/V)\varphi }$si y solo si${\displaystyle \!{\mathcal {M}},X[M/v]\models ^{-}\varphi }$.

Según la semántica del equipo, una oración IF${\displaystyle \varphi }$Se dice que es cierto (${\displaystyle {\mathcal {M}}\models ^{+}\varphi }$) en una estructura${\displaystyle {\mathcal {M}}}$si se satisface en${\displaystyle {\mathcal {M}}}$por el equipo singleton${\displaystyle \{\emptyset \}}$, en símbolos:${\displaystyle {\mathcal {M}},\{\emptyset \}\models ^{+}\varphi }$. Similarmente,${\displaystyle \varphi }$Se dice que es falso (${\displaystyle {\mathcal {M}}\models ^{-}\varphi }$) en${\displaystyle {\mathcal {M}}}$si${\displaystyle {\mathcal {M}},\{\emptyset \}\models ^{-}\varphi }$; se dice que es indeterminado (${\displaystyle {\mathcal {M}}\models ^{0}\varphi }$) si${\displaystyle {\mathcal {M}},\{\emptyset \}\not \models ^{+}\varphi }$y${\displaystyle {\mathcal {M}},\{\emptyset \}\not \models ^{-}\varphi }$.

Para cualquier equipo${\displaystyle X}$en una estructura${\displaystyle {\mathcal {M}}}$y cualquier fórmula SI${\displaystyle \varphi }$, tenemos: ${\displaystyle {\mathcal {M}},X\models ^{+}\varphi }$si y solo si${\displaystyle {\mathcal {M}},X\models _{GTS}^{+}\varphi }$ y ${\displaystyle {\mathcal {M}},X\models ^{-}\varphi }$si y solo si${\displaystyle {\mathcal {M}},X\models _{GTS}^{-}\varphi }$.

De esto se deduce inmediatamente que, para oraciones${\displaystyle \varphi }$,${\displaystyle {\mathcal {M}}\models ^{+}\varphi \Leftrightarrow {\mathcal {M}}\models _{GTS}^{+}\varphi }$,${\displaystyle {\mathcal {M}}\models ^{-}\varphi \Leftrightarrow {\mathcal {M}}\models _{GTS}^{-}\varphi }$y${\displaystyle {\mathcal {M}}\models ^{0}\varphi \Leftrightarrow {\mathcal {M}}\models _{GTS}^{0}\varphi }$.