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.

## Notas 
## Véxase tamén 
### Bibliografía 
* 
* 

### Outros artigos 
* Dupla carraca.
* Conectiva lóxica