Completude (lóxica)

En lóxica matemática e metalóxica, un sistema formal chámase completo en relación a unha propiedade específica se todas as fórmulas que teñan a propiedade poden obterse usando ese sistema, é dicir, é un dos seus teoremas; en caso contrario, dise que o sistema é incompleto. O termo "completo" tamén se usa sen cualificación, con diferentes significados segundo o contexto, normalmente referíndose á propiedade de validez semántica. Intuitivamente, un sistema chámase completo neste sentido particular se pode obter todas as fórmulas verdadeiras. Kurt Gödel, Leon Henkin e Emil Leon Post publicaron probas de completude.

Outras propiedades relacionadas coa completude

A propiedade recíproca da completude chámase corrección: un sistema é correcto en relación a unha propiedade (principalmente validez semántica) se cada un dos seus teoremas posúe esa propiedade.

Formas de completude

Completude expresiva

Unha linguaxe formal é expresivamente completa se pode expresar o obxecto que é destinado.

Completude funcional

Un conxunto de conectivas lóxicas asociadas ao sistema formal é funcionalmente completo se pode expresar todas as funcións proposicionais.

Completude semántica

A completude semántica é o recíproco da correcciónpara sistemas formais. Un sistema formal é completo en relación á tautoloxía cando todas as súas tautoloxías son teoremas, mentres que un sistema formal é correcto cando todos os teoremas son tautoloxías (é dicir, son fórmulas semanticamente válidas: fórmulas que son verdadeiras baixo calquera interpretación da linguaxe do sistema) que é consistente coas regras do sistema. É dicir:

$\models _{\mathcal {S}}\varphi \ \to \ \vdash _{\mathcal {S}}\varphi .$

Completude forte

Un sistema formal S é fortemente completo ou completo no sentido forte se para todo conxunto de premisas Γ, calquera fórmula que semánticamente segue de Γ se obtén de Γ. É dicir:

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

Refutación da completude

Un sistema formal S é refutación completo se é posébel obter un falso de cada conxunto de fórmulas insatisfactíbel. É dicir,

$\Gamma \models _{\mathcal {S}}\bot \to \ \Gamma \vdash _{\mathcal {S}}\bot .$

Todo sistema fortemente completo tamén é refutación completo. Indutivamente, a completude fore significa que, dado un conxunto de fórmulas $\Gamma$, é posíbel calcular todas as consecuencias semánticas $\varphi$ de $\Gamma$, mentres que a refutación completude significa que, dado un conxunto de fórmulas $\Gamma$ e a fórmula $\varphi$, é posíbel comprobar se $\varphi$ é unha consecuencia semántica de $\Gamma$.

Completude sintáctica

Un sistema formal S é sintácticamente completo ou dedutivamente completo ou máximamente completo se para cada sentenza (fórmula pechada) φ da linguaxe do sistema, φ ou ¬φ é un teorema de S. Isto tamén se chama negación-completude. Noutro sentido, un sistema formal é sintácticamente completo se e só se non é posíbel engadir unha oración non demostrábel sen introducir unha inconsistencia. A lóxica proposicional verofuncional e a lóxica de predicados de primeira orde son semanticamente completas mais non sintácticamente completas (por exemplo, o enunciado da lóxica proposicional que consiste nunha única variábel proposicional A non é un teorema, nin a súa negación, mais estes non son tautoloxías). O Teorema da incompletude de Gödel mostra que calquera sistema recursivo que sexa suficientemente poderoso, como o axioma de Peano, non pode ser consistente e sintáctico completo ao mesmo tempo.

Véxase tamén

Bibliografía

• Duffy, David A. (1991). Principles of Automated Theorem Proving (en inglés). Wiley. ISBN 9780471927846. 
• Hunter, Geoffrey (1996). Metalogic: An Introduction to the Metatheory of Standard First-Order Logic (en inglés). University of California Press. ISBN 9780520023567. OCLC 804708926. 

Outros artigos

• Dupla carraca.
• Conectiva lóxica