Sección 09: Solidez e integridad
- Page ID
- 101663
\( \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}\)Este kit de herramientas es increíblemente conveniente. También es intuitivo, porque parece natural que la demostrabilidad y la vinculación semántica estén de acuerdo. Sin embargo, no se deje engañar por la similitud de los símbolos '' y ''. El hecho de que estos dos sean realmente intercambiables no es algo sencillo de probar.
¿Por qué deberíamos pensar que un argumento que puede probarse es necesariamente un argumento válido? Es decir, ¿por qué\(\mathcal{A}\) pensar que\(\mathcal{B}\)\(\mathcal{A}\) implica\(\mathcal{B}\)?
Este es el problema de la solidez. Un sistema de prueba es sólido si no hay pruebas de argumentos inválidos. Demostrar que el sistema de prueba es sólido requeriría demostrar que cualquier prueba posible es la prueba de un argumento válido. No bastaría simplemente con tener éxito al tratar de probar muchos argumentos válidos y fallar al intentar probar los inválidos.
Afortunadamente, hay una manera de abordar esto de manera escalonada. Si el uso de la regla &E en la última línea de una prueba nunca podría cambiar un argumento válido por uno no válido, entonces usar la regla muchas veces no podría hacer que un argumento sea inválido. Del mismo modo, si usar las reglas &E y E individualmente en la última línea de una prueba nunca podría cambiar un argumento válido por uno inválido, entonces usarlos en combinación tampoco podría.
La estrategia es mostrar para cada regla de inferencia que por sí sola no pudo convertir un argumento válido en uno inválido. De ello se deduce que las reglas utilizadas en combinación no harían inválido un argumento válido. Dado que una prueba es solo una serie de líneas, cada una justificada por una regla de inferencia, esto demostraría que todo argumento demostrable es válido.
Consideremos, por ejemplo, la regla &I. Supongamos que lo usamos para agregar\(\mathcal{A}\) &\(\mathcal{B}\) a un argumento válido. Para que se aplique la regla,\(\mathcal{A}\) y\(\mathcal{B}\) deberá estar ya disponible en el comprobante. Ya que el argumento hasta el momento es válido,\(\mathcal{A}\) y\(\mathcal{B}\) son premisas del argumento o consecuencias válidas de las premisas. Como tal, cualquier modelo en el que las premisas sean verdaderas debe ser un modelo en el que\(\mathcal{A}\) y\(\mathcal{B}\) son verdaderas. Según la definición de la verdad en ql, esto significa que\(\mathcal{A}\) & también\(\mathcal{B}\) es cierto en tal modelo. Por lo tanto,\(\mathcal{A}\) &\(\mathcal{B}\) válidamente se desprende de las premisas. Esto significa que el uso de la regla &E para extender una prueba válida produce otra prueba válida.
Para demostrar que el sistema de prueba es sólido, necesitaríamos mostrar esto para las otras reglas de inferencia. Dado que las reglas derivadas son consecuencias de las reglas básicas, sería suficiente proporcionar argumentos similares para las otras 16 reglas básicas. Este tedioso ejercicio va más allá del alcance de este libro.
Ante una prueba de que el sistema de prueba es sólido, se deduce que cada teorema es una tautología.
Todavía es posible preguntar: ¿Por qué pensar que todo argumento válido es un argumento que se puede probar? Es decir, ¿por qué\(\mathcal{A}\) pensar que\(\mathcal{B}\)\(\mathcal{A}\) implica\(\mathcal{B}\)?
Este es el problema de la integridad. Un sistema de prueba está completo si hay una prueba de cada argumento válido. La integridad para un lenguaje como QL fue probada por primera vez por Kurt Gödel en 1929. La prueba está más allá del alcance de este libro.
El punto importante es que, felizmente, el sistema de prueba para QL es a la vez sólido y completo. Este no es el caso de todos los sistemas de prueba y de todos los lenguajes formales. Debido a que es cierto para QL, podemos optar por dar pruebas o construir modelos, lo que sea más fácil para la tarea en cuestión.
Resumen de definitions
- Una frase A es un teorema si y solo si\(\mathcal{A}\).
- Dos oraciones\(\mathcal{A}\) y\(\mathcal{B}\) son probablemente equivalentes si y\(\mathcal{A}\) sólo si\(\mathcal{B}\)\(\mathcal{B}\) y\(\mathcal{A}\).
- {\(\mathcal{A}\)1,\(\mathcal{A}\) 2,...} es demostrablemente inconsistente si y solo si, para alguna frase\(\mathcal{B}\), {\(\mathcal{A}\)1,\(\mathcal{A}\) 2,...} (\(\mathcal{B}\)&¬\(\mathcal{B}\)).