Completitud (lógica)

Un lenguaje formal es expresivamente completo si puede expresar el tema para el que está destinado.

Un conjunto de conectores lógicos asociados a un sistema formal es funcionalmente completo si puede expresar todas las funciones proposicionales .

La completitud semántica es lo opuesto a la solidez en los sistemas formales. Un sistema formal es completo con respecto a la tautología o "semánticamente completo" cuando todas sus tautologías son teoremas , mientras que un sistema formal es "sólido" cuando todos sus teoremas son tautologías (es decir, son fórmulas semánticamente válidas: fórmulas que son verdaderas bajo cualquier interpretación del lenguaje del sistema que sea consistente con las reglas del sistema). Es decir, un sistema formal es semánticamente completo si:

${\displaystyle \models _{\mathcal {S}}\varphi \ \implica \ \vdash _{\mathcal {S}}\varphi .}$^{[ 1 ]}

Por ejemplo, el teorema de completitud de Gödel establece la completitud semántica para la lógica de primer orden .

Un sistema formal S es fuertemente completo o completo en sentido fuerte si para cada conjunto de premisas Γ, cualquier fórmula que se derive semánticamente de Γ se puede derivar de Γ. Es decir:

${\displaystyle \Gamma \models _{\mathcal {S}}\varphi \ \implica \ \Gamma \vdash _{\mathcal {S}}\varphi .}$

Un sistema formal S es refutablemente completo si es capaz de derivar falsedades de todo conjunto de fórmulas insatisfacibles . Es decir:

${\displaystyle \Gamma \models _{\mathcal {S}}\bot \ \implica \ \Gamma \vdash _{\mathcal {S}}\bot .}$^{[ 2 ]}

Todo sistema fuertemente completo es también refutablemente completo. Intuitivamente, la fuerte completitud significa que, dado un conjunto de fórmulas${\displaystyle \Gamma }$Es posible calcular cada consecuencia semántica.${\displaystyle \varphi }$de${\displaystyle \Gamma }$, mientras que la completitud de la refutación significa que, dado un conjunto de fórmulas${\displaystyle \Gamma }$y una fórmula${\displaystyle \varphi }$, es posible comprobar si${\displaystyle \varphi }$es una consecuencia semántica de${\displaystyle \Gamma }$.

Ejemplos de sistemas refutables incluyen: resolución SLD en cláusulas de Horn , superposición en lógica de primer orden clausal ecuacional y resolución de Robinson en conjuntos de cláusulas. ^{[ 3 ]} Este último no es fuertemente completo: p. ej.${\displaystyle \{a\}\models a\lor b}$Se cumple incluso en el subconjunto proposicional de la lógica de primer orden, pero${\displaystyle a\lor b}$no se puede derivar de${\displaystyle \{a\}}$por resolución. Sin embargo,${\displaystyle \{a,\lnot (a\lor b)\}\vdash \bot }$puede derivarse.

Un sistema formal S es sintácticamente completo , deductivamente completo , máximamente completo o de negación completa si para cada oración (fórmula cerrada) φ del lenguaje del sistema, φ o ¬φ es un teorema de S. La completitud sintáctica es una propiedad más fuerte que la completitud semántica. Si un sistema formal es sintácticamente completo, una teoría formal correspondiente se denomina completa si es una teoría consistente . El teorema de incompletitud de Gödel demuestra que cualquier sistema computable suficientemente potente, como la aritmética de Peano , no puede ser a la vez consistente y sintácticamente completo.

La completitud sintáctica también puede referirse a otro concepto no relacionado, denominado postcompletitud o postcompletitud de Hilbert . En este sentido, un sistema formal es sintácticamente completo si y solo si no se le puede añadir ninguna oración indemostrable sin introducir una inconsistencia . La lógica proposicional veritativo-funcional y la lógica de predicados de primer orden son semánticamente completas, pero no sintácticamente completas (por ejemplo, la proposición lógica proposicional que consta de una sola variable proposicional A no es un teorema, ni tampoco lo es su negación).

En las lógicas superintuicionistas y modales , una lógica es estructuralmente completa si toda regla admisible es una implicación derivable.

Una teoría es modelo completa si y solo si cada incrustación de sus modelos es una incrustación elemental .