Diferencia entre revisiones de «Consistencia (lógica)»
Contenido eliminado Contenido añadido
Sin resumen de edición |
Retiro pédido de fusión, 3 años y no ha sido defendida la fusión |
||
Línea 1:
En [[lógica matemática]], un [[sistema formal]] es '''coherente''' si no contiene una [[contradicción]], o, en forma más precisa, no existe una [[proposición]] φ tal que se puede demostrar o deducir simultáneamente la proposición φ y su contraria ¬φ o no-φ.
Referido a un [[argumento]], la coherencia es la necesidad de que todas las premisas tengan que ser necesariamente y a la vez, como producto, todas verdaderas, para que el argumento, si es coherente, pueda ser [[validez lógica|válido]] o no válido. Referido al discurso la '''coherencia''' tiene que ver con que las implicaciones lógicas del mismo no sean autocontradictorias.
Una '''demostración de coherencia''' (o prueba de coherencia) es una demostración formal de que un sistema formal es coherente. El desarrollo inicial de la [[teoría de la demostración]] matemática fue motivado por el deseo de proveer demostraciones de coherencia finita para toda la matemáticas como parte del [[programa de Hilbert]]. El programa de Hilbert cumple con las observaciones de Gödel, tal como se expresa en sus dos [[teoremas de incompletitud de Gödel]], de que las teorías de demostración robustas no son capaces de probar su propia coherencia.
A pesar de que es posible demostrar la coherencia mediante teoría de modelos, por lo general se realiza de una manera puramente sintáctica, sin la necesidad de proveer una referencia a algún modelo de la lógica. La [[eliminación de corte]] (o en forma equivalente la [[Normalization property|normalización]] del [[Curry-Howard|cálculo subyacente]] si es que existe uno) implica la coherencia del cálculo: dado que obviamente no existe prueba de falsedad que sea libre de corte, no existe por lo tanto contradicción en general.
==Coherencia y completitud==
Los principales resultados relacionados con la corencia y completitud fueron demostrados por [[Kurt Gödel]]:
* El [[teorema de completitud de Gödel]] indica que toda [[teoría de primer orden]] coherente es completa con respecto al [[conjunto consistente máximo]] de las fórmulas que se generan por medio del algoritmo de búsqueda de demostración.
* Los [[teoremas de la incompletitud de Gödel]] indican que las teorías capaces de expresar su propia relación de demostrabilidad y de desarrollar un argumento diagonal son capaces de demostrar su propia coherencia solo si son incoherentes. Estas teorías, si son coherentes, son denominadas ''teorías esencialmente incompletas''.
Mediante la aplicación de estas ideas, se pueden encontrar cuatro tipos distintos de teorías de primer orden:
#Teorías incoherentes, que no poseen modelos;
#Teorías que no pueden analizar su propia relación de demostración, tales como la axiomatización de Tarski de la geometría del punto y la linea, y la [[aritmética de Presburg]]. Dado que estas teorías son descriptas en forma satisfactoria por el modelo que se obtiene mediante el teorema de completitud, entonces estos sistemas son completos;
#Teorías capaces de analizar su propia coherencia, y que incluyen la negación de la proposición que asevera su propia coherencia. Este tipo de teorías son completas con respecto al modelo que se obtiene a partir del teorema de completitud, pero contienen como teorema la implicancia de una contradicción, en contradicción al hecho de que son coherentes;
#Teorías esencialmente incompletas.
En forma adicional, se ha descubierto recientemente que existe un quinto tipo de teoría, las [[teorías auto verificables]], que son lo suficientemente robustas como para analizar su propia relación de demostración, pero son demasiado débiles como para realizar una diagonalización de Gödel, y que por lo tanto pueden demostrar en forma coherente su propia coherencia. Sin embargo, una teoría que demuestra su propia coherencia no permite obtener ninguna información interesante, dado que las teorías incoherentes también demuestran su propia coherencia.
==Fórmulas==
Un conjunto de [[Fórmula matemática|fórmulas]] <math>\Phi</math> en lógica de primer orden es '''coherente''' (expresado como Con<math>\Phi</math>) si y solo si no existe una fórmula <math>\phi</math> tal que <math>\Phi \vdash \phi</math> y <math>\Phi \vdash \lnot\phi</math>. De lo contrario <math>\Phi</math> es '''incoherente''' y se expresa Inc<math>\Phi</math>.
<math>\Phi</math> es '''simplemente coherente''' si y solo si para ninguna fórmula <math>\phi</math> de <math>\Phi</math> son tanto <math>\phi</math> como la [[negación]] de <math>\phi</math> teoremas de <math>\Phi</math>.
<math>\Phi</math> es '''absolutamente coherente''' o '''Post coherente''' si por lo menos una fórmula de <math>\Phi</math> no es un teorema de <math>\Phi</math>.
<math>\Phi</math> es '''máximamente coherente''' si y solo si para toda fórmula <math>\phi</math>, si Con <math>\Phi \cup \phi</math> entonces <math>\phi \in \Phi</math>.
<math>\Phi</math> se dice '''contiene testigos''' si y solo si para cada fórmula de la forma <math>\exist x \phi</math> existe un término <math>t</math> tal que <math>(\exists x \phi \to \phi {t \over x}) \in \Phi</math>. Véase [[Lógica de primer orden]].
===Resultados básicos===
'''1.''' Los siguientes son equivalentes:
(a) Inc<math>\Phi</math>
(b) Para todo <math>\phi,\; \Phi \vdash \phi.</math>
'''2.''' Todo conjunto de fórmulas ''satisfiable'' es consistente, un conjunto de fórmulas <math>\Phi</math> es ''satisfiable'' si y solo si existe un modelo <math>\mathfrak{I}</math> tal que <math>\mathfrak{I} \vDash \Phi </math>.
'''3.''' Para todo <math>\Phi</math> y <math>\phi</math>:
(a) si no <math> \Phi \vdash \phi</math>, entonces Con<math> \Phi \cup \{\lnot\phi\}</math>;
(b) si Con <math>\Phi</math> y <math>\Phi \vdash \phi</math>, entonces Con<math> \Phi \cup \{\phi\}</math>;
(c) si Con <math>\Phi</math>, entonces Con<math> \Phi \cup \{\phi\}</math> o Con<math> \Phi \cup \{\lnot \phi\}</math>.
'''4.''' Sea <math>\Phi</math> un conjunto de fórmulas coherentes y que poseen testigos. Para todo <math>\phi</math> y <math> \psi </math>:
(a) si <math> \Phi \vdash \phi</math>, entonces <math>\phi \in \Phi</math>,
(b) o bien <math>\phi \in \Phi</math> o bien <math>\lnot \phi \in \Phi</math>,
(c) <math>(\phi \or \psi) \in \Phi</math> si y solo si <math>\phi \in \Phi</math> o <math>\psi \in \Phi</math>,
(d) si <math>(\phi\to\psi) \in \Phi</math> y <math>\phi \in \Phi </math>, entonces <math>\psi \in \Phi</math>,
(e) <math>\exists x \phi \in \Phi</math> si y solo si existe un término <math>t</math> tal que <math>\phi{t \over x}\in\Phi</math>.
===Teorema de Henkin===
Sea <math>\Phi</math> un conjunto de fórmulas máximamente coherentes testigos.
Define una relación binaria en el conjunto de términos S <math> t_0 \sim t_1 \!</math> si y solo si <math>\; t_0 = t_1 \in \Phi</math>; y sea <math>\overline t \!</math> la clase de términos de equivalencia conteniendo <math>t \!</math>; y sea <math>T_{\Phi} := \{ \; \overline t \; |\; t \in T^S \} </math> donde <math>T^S \!</math> es el conjunto de términos basados en el conjunto de símbolo <math>S \!</math>.
Define la estructura S <math>\mathfrak T_{\Phi} </math> sobre <math> T_{\Phi} \!</math> el '''término-estructura''' correspondiente a <math>\Phi</math> mediante:
(1) Para el <math>n</math>-ésimo <math>R \in S</math>, <math>R^{\mathfrak T_{\Phi}} \overline {t_0} \ldots \overline {t_{n-1}}</math> si y solo si <math>\; R t_0 \ldots t_{n-1} \in \Phi</math>,
(2) Para el <math>n</math>-ésimo <math>f \in S</math>, <math>f^{\mathfrak T_{\Phi}} (\overline {t_0} \ldots \overline {t_{n-1}}) := \overline {f t_0 \ldots t_{n-1}}</math>,
(3) Para <math>c \in S</math>, <math>c^{\mathfrak T_{\Phi}}:= \overline c</math>.
Sea <math>\mathfrak I_{\Phi} := (\mathfrak T_{\Phi},\beta_{\Phi})</math> el '''término interpretación''' asociado con <math>\Phi</math>, donde <math>\beta _{\Phi} (x) := \bar x</math>.
<center>
<math>(*) \;</math> Para todo <math>\phi</math>,<math>\; \mathfrak I_{\Phi} \vDash \phi</math> si y solo si <math> \; \phi \in \Phi</math>.</center>
<!--
===Sketch of Proof===
There are several things to verify. First, that <math>\sim</math> is an [[equivalence relation]]. Then, it needs to be verified that (1), (2), and (3) are well defined. This falls out of the fact that <math>\sim</math> is an equivalence relation and also requires a proof that (1) and (2) are independent of the choice of <math> t_0, \ldots ,t_{n-1} </math> class representatives. Finally, <math> \mathfrak I_{\Phi} \vDash \Phi </math> can be verified by induction on formulas.
-->
==Véase también==
*[[Lógica paraconsistente]]
*[[Equiconsistency]]
*[[Hilbert's second problem]]
*[[Hilbert's program]]
*[[Hilbert's problems]]
*[[Matiyasevich's theorem]]
*[[Emil Post]] (1920)
*[[Łukasiewicz]]
==Referencias==
* {{cita libro |apellido1= H. D. Ebbinghaus |apellido2= J. Flum |apellido3= W. Thomas |título= Mathematical Logic |idioma= inglés |edición= Second Edition |año= 1994 |editorial= Springer-Verlag |ubicación= |isbn= 0-387-94258-0 |capítulo= |páginas= |cita= }}
[[Categoría:Lógica matemática]]
[[Categoría:Metalógica]]
[[en:Consistency proof]]
[[zh:形式系統相容性]]
| |||