7.1: Introducción
- Page ID
- 103511
\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)
\( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)
\( \newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\)
( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\)
\( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\)
\( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\)
\( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\)
\( \newcommand{\Span}{\mathrm{span}}\)
\( \newcommand{\id}{\mathrm{id}}\)
\( \newcommand{\Span}{\mathrm{span}}\)
\( \newcommand{\kernel}{\mathrm{null}\,}\)
\( \newcommand{\range}{\mathrm{range}\,}\)
\( \newcommand{\RealPart}{\mathrm{Re}}\)
\( \newcommand{\ImaginaryPart}{\mathrm{Im}}\)
\( \newcommand{\Argument}{\mathrm{Arg}}\)
\( \newcommand{\norm}[1]{\| #1 \|}\)
\( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\)
\( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\AA}{\unicode[.8,0]{x212B}}\)
\( \newcommand{\vectorA}[1]{\vec{#1}} % arrow\)
\( \newcommand{\vectorAt}[1]{\vec{\text{#1}}} % arrow\)
\( \newcommand{\vectorB}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)
\( \newcommand{\vectorC}[1]{\textbf{#1}} \)
\( \newcommand{\vectorD}[1]{\overrightarrow{#1}} \)
\( \newcommand{\vectorDt}[1]{\overrightarrow{\text{#1}}} \)
\( \newcommand{\vectE}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash{\mathbf {#1}}}} \)
\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)
\( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)
\(\newcommand{\avec}{\mathbf a}\) \(\newcommand{\bvec}{\mathbf b}\) \(\newcommand{\cvec}{\mathbf c}\) \(\newcommand{\dvec}{\mathbf d}\) \(\newcommand{\dtil}{\widetilde{\mathbf d}}\) \(\newcommand{\evec}{\mathbf e}\) \(\newcommand{\fvec}{\mathbf f}\) \(\newcommand{\nvec}{\mathbf n}\) \(\newcommand{\pvec}{\mathbf p}\) \(\newcommand{\qvec}{\mathbf q}\) \(\newcommand{\svec}{\mathbf s}\) \(\newcommand{\tvec}{\mathbf t}\) \(\newcommand{\uvec}{\mathbf u}\) \(\newcommand{\vvec}{\mathbf v}\) \(\newcommand{\wvec}{\mathbf w}\) \(\newcommand{\xvec}{\mathbf x}\) \(\newcommand{\yvec}{\mathbf y}\) \(\newcommand{\zvec}{\mathbf z}\) \(\newcommand{\rvec}{\mathbf r}\) \(\newcommand{\mvec}{\mathbf m}\) \(\newcommand{\zerovec}{\mathbf 0}\) \(\newcommand{\onevec}{\mathbf 1}\) \(\newcommand{\real}{\mathbb R}\) \(\newcommand{\twovec}[2]{\left[\begin{array}{r}#1 \\ #2 \end{array}\right]}\) \(\newcommand{\ctwovec}[2]{\left[\begin{array}{c}#1 \\ #2 \end{array}\right]}\) \(\newcommand{\threevec}[3]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \end{array}\right]}\) \(\newcommand{\cthreevec}[3]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \end{array}\right]}\) \(\newcommand{\fourvec}[4]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}\) \(\newcommand{\cfourvec}[4]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}\) \(\newcommand{\fivevec}[5]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}\) \(\newcommand{\cfivevec}[5]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}\) \(\newcommand{\mattwo}[4]{\left[\begin{array}{rr}#1 \amp #2 \\ #3 \amp #4 \\ \end{array}\right]}\) \(\newcommand{\laspan}[1]{\text{Span}\{#1\}}\) \(\newcommand{\bcal}{\cal B}\) \(\newcommand{\ccal}{\cal C}\) \(\newcommand{\scal}{\cal S}\) \(\newcommand{\wcal}{\cal W}\) \(\newcommand{\ecal}{\cal E}\) \(\newcommand{\coords}[2]{\left\{#1\right\}_{#2}}\) \(\newcommand{\gray}[1]{\color{gray}{#1}}\) \(\newcommand{\lgray}[1]{\color{lightgray}{#1}}\) \(\newcommand{\rank}{\operatorname{rank}}\) \(\newcommand{\row}{\text{Row}}\) \(\newcommand{\col}{\text{Col}}\) \(\renewcommand{\row}{\text{Row}}\) \(\newcommand{\nul}{\text{Nul}}\) \(\newcommand{\var}{\text{Var}}\) \(\newcommand{\corr}{\text{corr}}\) \(\newcommand{\len}[1]{\left|#1\right|}\) \(\newcommand{\bbar}{\overline{\bvec}}\) \(\newcommand{\bhat}{\widehat{\bvec}}\) \(\newcommand{\bperp}{\bvec^\perp}\) \(\newcommand{\xhat}{\widehat{\xvec}}\) \(\newcommand{\vhat}{\widehat{\vvec}}\) \(\newcommand{\uhat}{\widehat{\uvec}}\) \(\newcommand{\what}{\widehat{\wvec}}\) \(\newcommand{\Sighat}{\widehat{\Sigma}}\) \(\newcommand{\lt}{<}\) \(\newcommand{\gt}{>}\) \(\newcommand{\amp}{&}\) \(\definecolor{fillinmathshade}{gray}{0.9}\)Las lógicas suelen tener tanto una semántica como un sistema de derivación. La semántica se refiere a conceptos como la verdad, la satisfacción, la validez y la vinculación. El propósito de los sistemas de derivación es proporcionar un método puramente sintáctico para establecer la vinculación y validez. Son puramente sintácticos en el sentido de que una derivación en tal sistema es un objeto sintáctico finito, generalmente una secuencia (u otro arreglo finito) de oraciones o fórmulas. Los buenos sistemas de derivación tienen la propiedad de que cualquier secuencia o disposición dada de oraciones o fórmulas puede verificarse mecánicamente para que sea “correcta”.
Los sistemas de derivación más simples (e históricamente primeros) para la lógica de primer orden fueron axiomáticos. Una secuencia de fórmulas cuenta como derivación en dicho sistema si cada fórmula individual en ella está entre un conjunto fijo de “axiomas” o sigue de fórmulas que vienen antes de ella en la secuencia por una de un número fijo de “reglas de inferencia”, y se puede verificar mecánicamente si una fórmula es un axioma y si se desprende correctamente de otras fórmulas por una de las reglas de inferencia. Los sistemas de prueba axiomática son fáciles de describir y también fáciles de manejar meta-teóricamente, pero las derivaciones en ellos son difíciles de leer y entender, y también son difíciles de producir.
Se han desarrollado otros sistemas de derivación con el objetivo de facilitar la construcción de derivaciones o facilitar la comprensión de las derivaciones una vez que están completas. Los ejemplos son la deducción natural, los árboles de la verdad, también conocidos como pruebas tableaux, y el cálculo secuente. Algunos sistemas de derivación están diseñados especialmente teniendo en cuenta la mecanización, por ejemplo, el método de resolución es fácil de implementar en software (pero sus derivaciones son esencialmente imposibles de entender). La mayoría de estos otros sistemas de prueba representan derivaciones como árboles de fórmulas en lugar de secuencias. Esto hace que sea más fácil ver qué partes de una derivación dependen de qué otras partes.
Entonces, para una lógica dada, como la lógica de primer orden, los diferentes sistemas de derivación darán diferentes explicaciones de lo que es para una oración ser un teorema y lo que significa que una oración sea derivable de algunas otras. Sin embargo, eso se hace (vía derivaciones axiomáticas, deducciones naturales, derivaciones secuentes, árboles de la verdad, refutaciones de resolución), queremos que estas relaciones coincidan con las nociones semánticas de validez y vinculación. Escribamos\(\Proves A\) para “\(A\)es un teorema” y “\(\Gamma \Proves A\)” para “\(A\)es derivable de”\(\Gamma\). Sin embargo\(\Proves\) se define, queremos que coincida con\(\Entails\), es decir:
-
\(\Proves A\)si y solo si\(\Entails A\)
-
\(\Gamma \Proves A\)si y solo si\(\Gamma \Entails A\)
A la dirección “sólo si” de lo anterior se le llama solidez. Un sistema de derivación es sólido si la derivabilidad garantiza la vinculación (o validez). Todo sistema de derivación decente tiene que ser sólido; los sistemas de derivación incorrectos no son útiles en absoluto. Después de todo, todo el propósito de una derivación es proporcionar una garantía sintáctica de validez o vinculación. Demostraremos solidez para los sistemas de derivación que presentamos.
También es importante la dirección del “si” inverso: se llama integridad. Un sistema de derivación completo es lo suficientemente fuerte como para mostrar que\(A\) es un teorema siempre que\(A\) sea válido, y que\(\Gamma \Proves A\) cuando sea\(\Gamma \Entails A\). La completitud es más difícil de establecer y algunas lógicas no tienen sistemas completos de derivación. La lógica de primer orden sí. Kurt Gödel fue el primero en probar la integridad de un sistema de derivación de lógica de primer orden en su tesis de 1929.
Otro concepto que está conectado a los sistemas de derivación es el de consistencia. Un conjunto de oraciones se llama inconsistente si de ello se puede derivar algo en absoluto, y consistente de otra manera. La inconsistencia es la contraparte sintáctica de la insatisfiablidad: al igual que los conjuntos insatisfactibles, los conjuntos inconsistentes de oraciones no hacen buenas teorías, son defectuosos de manera fundamental. Los conjuntos consistentes de oraciones pueden no ser verdaderos o útiles, pero al menos pasan ese umbral mínimo de utilidad lógica. Para diferentes sistemas de derivación la definición específica de consistencia de conjuntos de oraciones puede diferir, pero al igual que\(\Proves\), queremos que la consistencia coincida con su contraparte semántica, la satisfacción. Queremos que siempre sea el caso que\(\Gamma\) sea consistente si y sólo si es satisfecha. Aquí, la dirección “si” equivale a integridad (la consistencia garantiza la satisfacción), y la dirección “solo si” equivale a solidez (la satisfacbilidad garantiza la consistencia). De hecho, para la lógica clásica de primer orden, las dos versiones de solidez e integridad son equivalentes.