Ver o código fonte de «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 (lóxica)|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 (lóxica)|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 [[Conectivo lóxico|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 (lóxica)|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 [[Dupla carraca|semanticamente válidas]]: fórmulas que son verdadeiras baixo calquera interpretación da linguaxe do sistema) que é consistente coas regras do sistema. É dicir:

:: <math> \models_{\mathcal S} \varphi\ \to\ \vdash_{\mathcal S} \varphi.</math>{{Sfn|Hunter|1996|p=94}}

=== Completude forte ===
Un sistema formal <span class="mathcal" style="font-family: 'Lucida Calligraphy', 'Monotype Corsiva', 'URW Chancery L', 'Apple Chancery', serif;">S</span> é '''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:

::<math> \Gamma\models_{\mathcal S} \varphi \ \to\ \Gamma \vdash_{\mathcal S} \varphi.</math>

=== Refutación da completude ===
Un sistema formal <span class="mathcal" style="font-family: 'Lucida Calligraphy', 'Monotype Corsiva', 'URW Chancery L', 'Apple Chancery', serif;">S</span> é '''refutación completo''' se é posébel obter un falso de cada conxunto de fórmulas insatisfactíbel. É dicir,

:: <math> \Gamma \models_{\mathcal S} \bot \to\ \Gamma \vdash_{\mathcal S} \bot.</math>{{Sfn|Duffy|1991}}

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

=== Completude sintáctica ===
Un sistema formal <span class="mathcal" style="font-family: 'Lucida Calligraphy', 'Monotype Corsiva', 'URW Chancery L', 'Apple Chancery', serif;">S</span> é '''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 <span class="mathcal" style="font-family: 'Lucida Calligraphy', 'Monotype Corsiva', 'URW Chancery L', 'Apple Chancery', serif;">S.</span> 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. [[Lóxica proposicional|A lóxica proposicional verofuncional]] e [[Lóxica de primeira orde|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). [[Teorema da incompletude de Gödel|O Teorema da incompletude de Gödel]] mostra que calquera sistema recursivo que sexa suficientemente poderoso, como [[Axioma de Peano|o axioma de Peano]], non pode ser consistente e sintáctico completo ao mesmo tempo.

== Notas ==
{{Listaref|30em}} 

== Véxase tamén ==
=== Bibliografía ===
{{Refempeza}}

* {{Cita libro|apelidos=Duffy|nome=David A.|título=Principles of Automated Theorem Proving|ano=1991|editorial=Wiley|isbn=9780471927846|url=https://www.google.es/books/edition/Principles_of_Automated_Theorem_Proving/LO1QAAAAMAAJ?hl=es&gbpv=0&bsq=Principles%20of%20Automated%20Theorem%20Proving|lingua=en|ref=harv}}
* {{Cita libro|apelidos=Hunter|nome=Geoffrey|ligazón-autor=Geoffrey Hunter|título=Metalogic: An Introduction to the Metatheory of Standard First-Order Logic|data=1996|editorial=University of California Press|isbn=9780520023567|oclc=804708926|lingua=en|ref=harv}}

{{Reftermina}}

=== Outros artigos ===
* [[Dupla carraca]].
* [[Conectiva lóxica]]

{{Control de autoridades}}

[[Categoría:Lóxica matemática]]