Lógica de dependencia

En la lógica de dependencia, los términos se definen exactamente igual que en la lógica de primer orden .

En la lógica de dependencia existen tres tipos de fórmulas atómicas:

1. Un átomo relacional es una expresión de la forma${\displaystyle Rt_{1}\ldots t_{n}}$para cualquier relación n -aria${\displaystyle R}$en nuestra firma y para cualquier n - tupla de términos${\displaystyle (t_{1},\ldots ,t_{n})}$;
2. Un átomo de igualdad es una expresión de la forma${\displaystyle t_{1}=t_{2}}$, para cualesquiera dos términos${\displaystyle t_{1}}$y${\displaystyle t_{2}}$;
3. Un átomo de dependencia es una expresión de la forma${\displaystyle =\!\!(t_{1}\ldots t_{n})}$, para cualquier${\displaystyle n\in \mathbb {N} }$y para cualquier n -tupla de términos${\displaystyle (t_{1},\ldots ,t_{n})}$.

Nada más es una fórmula atómica de la lógica de la dependencia.

Los átomos relacionales y de igualdad también se denominan átomos de primer orden .

Para una signatura fija σ, el conjunto de todas las fórmulas${\displaystyle \phi }$de la lógica de dependencia y sus respectivos conjuntos de variables libres${\displaystyle {\mbox{Gratis}}(\phi )}$se definen de la siguiente manera:

1. Cualquier fórmula atómica${\displaystyle \phi }$es una fórmula, y${\displaystyle {\mbox{Gratis}}(\phi )}$es el conjunto de todas las variables que aparecen en él;
2. Si${\displaystyle \phi }$es una fórmula, también lo es${\displaystyle \lnot \phi }$y${\displaystyle {\mbox{Free}}(\lnot \phi )={\mbox{Free}}(\phi )}$;
3. Si${\displaystyle \phi }$y${\displaystyle \psi }$son fórmulas, así que es${\displaystyle \phi \vee \psi }$y${\displaystyle {\mbox{Libre}}(\phi \vee \psi )={\mbox{Libre}}(\phi )\cup {\mbox{Libre}}(\psi )}$;
4. Si${\displaystyle \phi }$es una fórmula y${\displaystyle x}$es una variable,${\displaystyle \exists x\phi }$También es una fórmula y${\displaystyle {\mbox{Free}}(\exists v\phi )={\mbox{Free}}(\phi )\backslash \{v\}}$.

Nada es una fórmula de lógica de dependencia a menos que pueda obtenerse mediante un número finito de aplicaciones de estas cuatro reglas.

Una fórmula${\displaystyle \phi }$de tal manera que${\displaystyle {\mbox{Libre}}(\phi )=\emptyset }$es una oración de lógica de dependencia.

Dejar${\displaystyle {\mathcal {A}}=(A,\sigma ,I)}$sea ​​una estructura de primer orden y deje que${\displaystyle V=\{v_{1},\ldots,v_{n}\}}$Sea A un conjunto finito de variables. Entonces, un equipo sobre A con dominio V es un conjunto de asignaciones sobre A con dominio V , es decir, un conjunto de funciones μ de V a A.

Puede resultar útil visualizar dicho equipo como una relación de base de datos con atributos.${\displaystyle v_{1},\ldots,v_{n}}$y con un solo tipo de datos , correspondiente al dominio A de la estructura: por ejemplo, si el equipo X consta de cuatro asignaciones${\displaystyle \mu _{1},\ldots ,\mu _{4}}$con dominio${\displaystyle \{v_{1},v_{2},v_{3}\}}$entonces se puede representar como la relación

${\displaystyle {\begin{array}{c|ccc}&v_{1}&v_{2}&v_{3}\\\hline \mu _{1}&\mu _{1}(v_{1})&\mu _{1}(v_{2})&\mu _{1}(v_{3})\\\mu _{2}&\mu _{2}(v_{1})&\mu _{2}(v_{2})&\mu _{2}(v_{3})\\\mu _{3}&\mu _{3}(v_{1})&\mu _{3}(v_{2})&\mu _{3}(v_{3})\\\mu _{4}&\mu _{4}(v_{1})&\mu _{4}(v_{2})&\mu _{4}(v_{3})\end{array}}}$

La semántica de equipo se puede definir en términos de dos relaciones.${\displaystyle {\mathcal {T}}}$y${\displaystyle {\mathcal {C}}}$entre estructuras, equipos y fórmulas.

Dada una estructura${\displaystyle {\mathcal {A}}}$, un equipo${\displaystyle X}$sobre ello y una fórmula de lógica de dependencia${\displaystyle \phi }$cuyas variables libres están contenidas en el dominio de${\displaystyle X}$, si${\displaystyle ({\mathcal {A}},X,\phi )\in {\mathcal {T}}}$decimos que${\displaystyle X}$es un triunfo para${\displaystyle \phi }$en${\displaystyle {\mathcal {A}}}$y escribimos que${\displaystyle {\mathcal {A}}\models _{X}^{+}\phi }$; y análogamente, si${\displaystyle ({\mathcal {A}},X,\phi )\in {\mathcal {C}}}$decimos que${\displaystyle X}$es un triunfo para${\displaystyle \phi }$en${\displaystyle {\mathcal {A}}}$y escribimos que${\displaystyle {\mathcal {A}}\models _{X}^{-}\phi }$.

Si${\displaystyle {\mathcal {A}}\models _{X}^{+}\phi }$También se puede decir que${\displaystyle \phi }$está positivamente satisfecho por${\displaystyle X}$en${\displaystyle {\mathcal {A}}}$y si en cambio${\displaystyle {\mathcal {A}}\models _{X}^{-}\phi }$se puede decir que${\displaystyle \phi }$está negativamente satisfecho por${\displaystyle X}$en${\displaystyle {\mathcal {A}}}$.

La necesidad de considerar la satisfacción positiva y negativa por separado es consecuencia del hecho de que en la lógica de dependencia, como en la lógica de cuantificadores ramificados o en la lógica IF , la ley del tercero excluido no se cumple; alternativamente, se puede suponer que todas las fórmulas están en forma normal de negación , utilizando las relaciones de De Morgan para definir la cuantificación universal y la conjunción a partir de la cuantificación existencial y la disyunción respectivamente, y considerar solo la satisfacción positiva.

Dada una oración${\displaystyle \phi }$, decimos que${\displaystyle \phi }$es cierto en${\displaystyle {\mathcal {A}}}$si y solo si${\displaystyle {\mathcal {A}}\models _{\{\emptyset \}}^{+}\phi }$y decimos que${\displaystyle \phi }$es falso en${\displaystyle {\mathcal {A}}}$si y solo si${\displaystyle {\mathcal {A}}\models _{\{\emptyset \}}^{-}\phi }$.

En cuanto al caso de la relación de satisfacibilidad de Alfred Tarski para fórmulas de primer orden, las relaciones de satisfacibilidad positiva y negativa de la semántica de equipo para la lógica de dependencia se definen por inducción estructural sobre las fórmulas del lenguaje. Dado que el operador de negación intercambia la satisfacibilidad positiva y negativa, las dos inducciones correspondientes a${\displaystyle \models ^{+}}$y${\displaystyle \models ^{-}}$deben realizarse simultáneamente:

La lógica de dependencia es una extensión conservadora de la lógica de primer orden: ^{[ 4 ]} en otras palabras, para cada oración de primer orden${\displaystyle \phi }$y estructura${\displaystyle {\mathcal {A}}}$tenemos eso${\displaystyle {\mathcal {A}}\models _{\{\emptyset \}}^{+}\phi }$si y solo si${\displaystyle \phi }$es cierto en${\displaystyle {\mathcal {A}}}$según la semántica habitual de primer orden. Además, para cualquier fórmula de primer orden${\displaystyle \phi }$,${\displaystyle {\mathcal {A}}\models _{X}^{+}\phi }$si y solo si todas las asignaciones${\displaystyle \mu \in X}$satisfacer${\displaystyle \phi }$en${\displaystyle {\mathcal {A}}}$según la semántica habitual de primer orden.

Sin embargo, la lógica de dependencia es estrictamente más expresiva que la lógica de primer orden: ^{[ 5 ]} por ejemplo, la oración

${\displaystyle \exists z\forall x_{1}\forall x_{2}\exists y_{1}\exists y_{2}(=\!\!(x_{1},y_{1})\wedge =\!\!(x_{2},y_{2})\wedge (x_{1}=x_{2}\leftrightarrow y_{1}=y_{2})\wedge y_{1}\not =z)}$

es cierto en un modelo${\displaystyle {\mathcal {A}}}$si y solo si el dominio de este modelo es infinito, aunque no exista ninguna fórmula de primer orden.${\displaystyle \phi }$tiene esta propiedad.

Cada enunciado de lógica de dependencia es equivalente a algún enunciado en el fragmento existencial de lógica de segundo orden , ^{[ 6 ]} es decir, a algún enunciado de segundo orden de la forma

${\displaystyle \exists R_{1}\ldots \exists R_{n}\psi (R_{1},\ldots ,R_{n})}$

dónde${\displaystyle \psi (R_{1},\ldots ,R_{n})}$no contiene cuantificadores de segundo orden. Por el contrario, toda oración de segundo orden en la forma anterior es equivalente a alguna oración de lógica de dependencia. ^{[ 7 ]}

En cuanto a las fórmulas abiertas, la lógica de dependencia corresponde al fragmento monótono descendente de la lógica existencial de segundo orden, en el sentido de que una clase no vacía de equipos es definible por una fórmula de lógica de dependencia si y solo si la clase de relaciones correspondiente es monótona descendente y definible por una fórmula existencial de segundo orden. ^{[ 8 ]}

Los cuantificadores ramificados se pueden expresar en términos de átomos de dependencia: por ejemplo, la expresión

${\displaystyle (Q_{H}x_{1},x_{2},y_{1},y_{2})\phi (x_{1},x_{2},y_{1},y_{2})\equiv {\begin{pmatrix}\forall x_{1}\exists y_{1}\\\forall x_{2}\exists y_{2}\end{pmatrix}}\phi (x_{1},x_{2},y_{1},y_{2})}$

es equivalente a la oración lógica de dependencia${\displaystyle \forall x_{1}\exists y_{1}\forall x_{2}\exists y_{2}(=\!\!(x_{1},y_{1})\wedge =\!\!(x_{2},y_{2})\wedge \phi )}$, en el sentido de que la primera expresión es verdadera en un modelo si y solo si la segunda expresión es verdadera.

Por el contrario, cualquier sentencia de lógica de dependencia es equivalente a alguna sentencia en la lógica de cuantificadores ramificados, ya que todas las sentencias existenciales de segundo orden se pueden expresar en la lógica de cuantificadores ramificados. ^{[ 9 ] [ 10 ]}

Cualquier sentencia lógica de dependencia es lógicamente equivalente a alguna sentencia lógica IF, y viceversa. ^{[ 11 ]}

Sin embargo, el problema es más sutil cuando se trata de fórmulas abiertas. Las traducciones entre fórmulas de lógica IF y lógica de dependencia, y viceversa, existen siempre que el dominio del equipo sea fijo: en otras palabras, para todos los conjuntos de variables.${\displaystyle V=\{v_{1}\ldots v_{n}\}}$y todas las fórmulas lógicas IF${\displaystyle \phi }$con variables libres en${\displaystyle V}$Existe una fórmula lógica de dependencia${\displaystyle \phi ^{D}}$de tal manera que

${\displaystyle {\mathcal {A}}\models _{X}^{+}\phi \Leftrightarrow {\mathcal {A}}\models _{X}^{+}\phi ^{D}}$

para todas las estructuras${\displaystyle {\mathcal {A}}}$y para todos los equipos${\displaystyle X}$con dominio${\displaystyle V}$y, a la inversa, para cada fórmula lógica de dependencia${\displaystyle \psi }$con variables libres en${\displaystyle V}$Existe una fórmula lógica IF.${\displaystyle \psi ^{I}}$de tal manera que

${\displaystyle {\mathcal {A}}\models _{X}^{+}\psi \Leftrightarrow {\mathcal {A}}\models _{X}^{+}\psi ^{I}}$

para todas las estructuras${\displaystyle {\mathcal {A}}}$y para todos los equipos${\displaystyle X}$con dominio${\displaystyle V}$Estas traducciones no pueden ser compositivas. ^{[ 12 ]}

La lógica de equipo ^{[ 19 ]} extiende la lógica de dependencia con una negación contradictoria.${\displaystyle \sim \!\!\phi }$Su poder expresivo es equivalente al de la lógica de segundo orden completa. ^{[ 20 ]}

El átomo de dependencia, o una variante adecuada del mismo, puede agregarse al lenguaje de la lógica modal , obteniendo así la lógica de dependencia modal . ^{[ 21 ] [ 22 ] [ 23 ]}

Tal como está, la lógica de la dependencia carece de implicación. La implicación intuicionista${\displaystyle \phi \rightarrow \psi }$, cuyo nombre deriva de la similitud entre su definición y la de la implicación de la lógica intuicionista , puede definirse de la siguiente manera: ^{[ 24 ]}

${\displaystyle {\mathcal {A}}\models _{X}\phi \rightarrow \psi }$si y solo si para todos${\displaystyle Y\subseteq X}$de tal manera que${\displaystyle {\mathcal {A}}\models _{Y}\phi }$sostiene que${\displaystyle {\mathcal {A}}\models _{Y}\psi }$.

La lógica de dependencia intuicionista, es decir, la lógica de dependencia complementada con la implicación intuicionista, es equivalente a la lógica de segundo orden. ^{[ 25 ]}

En lugar de átomos de dependencia, la lógica de independencia agrega átomos de independencia al lenguaje de la lógica de primer orden.${\displaystyle {\vec {t_{1}}}\bot _{\vec {t_{3}}}{\vec {t_{2}}}}$dónde${\displaystyle {\vec {t_{1}}}}$,${\displaystyle {\vec {t_{2}}}}$y${\displaystyle {\vec {t_{3}}}}$son tuplas de términos. La semántica de estos átomos se define de la siguiente manera:

${\displaystyle {\mathcal {A}}\models _{X}{\vec {t_{1}}}\bot _{\vec {t_{3}}}{\vec {t_{2}}}}$si y solo si para todos${\displaystyle s,s'\in X}$con${\displaystyle {\vec {t_{3}}}\langle s\rangle ={\vec {t_{3}}}\langle s'\rangle }$existe${\displaystyle s''\in X}$de tal manera que${\displaystyle {\vec {t_{3}}}\langle s''\rangle ={\vec {t_{3}}}\langle s\rangle }$,${\displaystyle {\vec {t_{1}}}\langle s''\rangle ={\vec {t_{1}}}\langle s\rangle }$y${\displaystyle {\vec {t_{2}}}\langle s''\rangle ={\vec {t_{2}}}\langle s'\rangle }$.

La lógica de independencia se corresponde con la lógica existencial de segundo orden, en el sentido de que una clase no vacía de equipos se puede definir mediante una fórmula de lógica de independencia si y solo si la clase correspondiente de relaciones se puede definir mediante una fórmula existencial de segundo orden. ^{[ 26 ]} Por lo tanto, a nivel de fórmulas abiertas, la lógica de independencia es estrictamente más potente en expresividad que la lógica de dependencia. Sin embargo, a nivel de oraciones, estas lógicas son equivalentes. ^{[ 27 ]}

La lógica de inclusión/exclusión extiende la lógica de primer orden con átomos de inclusión.${\displaystyle {\vec {t_{1}}}\subseteq {\vec {t_{2}}}}$y átomos de exclusión${\displaystyle {\vec {t_{1}}}\mid {\vec {t_{2}}}}$donde en ambas fórmulas${\displaystyle {\vec {t_{1}}}}$y${\displaystyle {\vec {t_{2}}}}$son tuplas de términos de la misma longitud. La semántica de estos átomos se define de la siguiente manera:

• ${\displaystyle {\mathcal {A}}\models _{X}{\vec {t_{1}}}\subseteq {\vec {t_{2}}}}$si y solo si para todos${\displaystyle s\in X}$existe${\displaystyle s'\in X}$de tal manera que${\displaystyle {\vec {t_{1}}}\langle s\rangle ={\vec {t_{2}}}\langle s'\rangle }$;
• ${\displaystyle {\mathcal {A}}\models _{X}{\vec {t_{1}}}\mid {\vec {t_{2}}}}$si y solo si para todos${\displaystyle s,s'\in X}$sostiene que${\displaystyle {\vec {t_{1}}}\langle s\rangle \neq {\vec {t_{2}}}\langle s'\rangle }$.

La lógica de inclusión/exclusión tiene el mismo poder expresivo que la lógica de independencia, incluso a nivel de fórmulas abiertas. ^{[ 28 ]} La lógica de inclusión y la lógica de exclusión se obtienen añadiendo átomos de inclusión o átomos de exclusión a la lógica de primer orden, respectivamente. Las sentencias de la lógica de inclusión corresponden en poder expresivo a las sentencias de la lógica de punto fijo mayor; por lo tanto, la lógica de inclusión captura la lógica de punto fijo (menor) en modelos finitos, y PTIME sobre modelos ordenados finitos. ^{[ 29 ]} La lógica de exclusión, a su vez, corresponde a la lógica de dependencia en poder expresivo. ^{[ 30 ]}

Otra forma de extender la lógica de dependencia es añadir cuantificadores generalizados a su lenguaje. Recientemente se ha estudiado la lógica de dependencia con cuantificadores generalizados monótonos ^{[ 31 ]} y la lógica de dependencia con un cuantificador de mayoría específico, lo que ha dado lugar a una nueva caracterización de la complejidad descriptiva de la jerarquía de conteo. ^{[ 32 ]}