En lógica matemática y metalógica , un sistema formal se denomina completo con respecto a una propiedad particular si cada fórmula que tiene la propiedad puede derivarse utilizando ese sistema, es decir, es uno de sus teoremas ; de lo contrario, el sistema se dice que es incompleto . El término "completo" también se utiliza sin calificación, con diferentes significados según el contexto, refiriéndose principalmente a la propiedad de validez semántica . Intuitivamente, un sistema se denomina completo en este sentido particular, si puede derivar cada fórmula que sea verdadera.
La propiedad inversa a la completitud se llama solidez : un sistema es sólido con respecto a una propiedad (principalmente validez semántica) si cada uno de sus teoremas tiene esa propiedad.
Un lenguaje formal es expresivamente completo si puede expresar el contenido al que está destinado.
Un conjunto de conectivos lógicos asociados a un sistema formal es funcionalmente completo si puede expresar todas las funciones proposicionales .
La completitud semántica es el inverso de la solidez para 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 los 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:
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 siga semánticamente de Γ es derivable de Γ. Es decir:
Un sistema formal S es refutable si es capaz de derivar algo falso de cada conjunto insatisfactorio de fórmulas. Es decir:
Todo sistema fuertemente completo es también refutación completa. Intuitivamente, completitud fuerte significa que, dado un conjunto de fórmulas , es posible calcular cada consecuencia semántica de , mientras que completitud de refutación significa que, dado un conjunto de fórmulas y una fórmula , es posible verificar si es una consecuencia semántica de .
Ejemplos de sistemas de refutación completa incluyen: resolución SLD en cláusulas de Horn , superposición en lógica de primer orden de cláusulas ecuacionales , resolución de Robinson en conjuntos de cláusulas. [3] Este último no es fuertemente completo: por ejemplo, se cumple incluso en el subconjunto proposicional de la lógica de primer orden, pero no se puede derivar de él por resolución. Sin embargo, se puede derivar.
Un sistema formal S es sintácticamente completo o deductivamente completo o máximamente completo si para cada oración (fórmula cerrada) φ del lenguaje del sistema, φ o ¬φ es un teorema de S. Esto también se llama completitud de negación y es más fuerte que la completitud semántica. En otro sentido, un sistema formal es sintácticamente completo si y solo si no se le puede agregar 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, el enunciado de lógica proposicional que consiste en una sola variable proposicional A no es un teorema, y tampoco lo es su negación). El teorema de incompletitud de Gödel muestra que cualquier sistema computable que sea suficientemente poderoso, como la aritmética de Peano , no puede ser a la vez consistente y sintácticamente completo.
En las lógicas superintuicionistas y modales , una lógica es estructuralmente completa si cada regla admisible es derivable.
Una teoría es modelo completo si y sólo si cada incrustación de sus modelos es una incrustación elemental .
