7.5: Derivaciones axiomáticas
- Page ID
- 103493
\( \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 derivaciones axiomáticas son los sistemas de derivación lógica más antiguos y simples. Sus derivaciones son simplemente secuencias de oraciones. Una secuencia de oraciones cuenta como una derivación correcta si cada oración\(A\) en ella cumple una de las siguientes condiciones:
-
\(A\)es un axioma, o
-
\(A\)es un elemento de un conjunto dado\(\Gamma\) de oraciones, o
-
\(A\)se justifica por una regla de inferencia.
Para ser un axioma,\(A\) tiene que tener la forma de uno de una serie de esquemas de oraciones fijas. Existen muchos conjuntos de esquemas de axiomas que proporcionan un sistema de derivación satisfactorio (sonoro y completo) para la lógica de primer orden. Algunos se organizan según los conectivos que gobiernan, e.g., los esquemas\[A \lif (B \lif A) \qquad B \lif (B \lor C) \qquad (B \land C) \lif B\nonumber\] son axiomas comunes que gobiernan\(\lif\),\(\lor\) y\(\land\). Algunos sistemas de axiomas apuntan a un número mínimo de axiomas. Dependiendo de los conectivos que se toman como primitivos, incluso es posible encontrar sistemas de axiomas que consisten en un solo axioma.
Una regla de inferencia es una declaración condicional que da una condición suficiente para que una oración en una derivación sea justificada. Modus ponens es una regla muy común de este tipo: dice que si\(A\) y ya\(A \lif B\) están justificados, entonces\(B\) se justifica. Esto significa que\(B\) se justifica una línea en una derivación que contiene la oración, siempre que ambos\(A\) y\(A \lif B\) (para alguna oración\(A\)) aparezcan en la derivación anterior\(B\).
La\(\Proves\) relación basada en derivaciones axiomáticas se define de la siguiente manera:\(\Gamma \Proves A\) si existe una derivación con la oración\(A\) como su última fórmula (y\(\Gamma\) se toma como conjunto de oraciones en esa derivación las cuales se justifican por (2) arriba). \(A\)es un teorema si\(A\) tiene una derivación donde\(\Gamma\) está vacía, es decir, cada oración en la derivación es justada ya sea por (1) o (3). Por ejemplo, aquí hay una derivación que muestra que\(\Proves A \lif (B \lif (B \lor A))\):
1. \(B \lif (B \lor A)\)
2. \((B \lif (B \lor A)) \lif (A \lif (B \lif (B \lor A)))\)
3. \(A \lif (B \lif (B \lor A))\)
La frase en la línea 1 es de la forma del axioma\(A \lif (A \lor B)\) (con los papeles de\(A\) y\(B\) invertido). La frase de la línea 2 es de la forma del axioma\(A \lif (B \lif A)\). Así, ambas líneas están justificadas. La línea 3 se justifica por modus ponens: si la abreviamos como\(D\), entonces la línea 2 tiene la forma\(C \lif D\), donde\(C\) está\(B \lif (B \lor A)\), es decir, la línea 1.
Un conjunto\(\Gamma\) es inconsistente si\(\Gamma \Proves \lfalse\). Un sistema completo de axiomas también lo demostrará\(\lfalse \lif A\) para cualquiera\(A\), y así si\(\Gamma\) es inconsistente, entonces\(\Gamma \Proves A\) para cualquiera\(A\).
Los sistemas de derivaciones axiomáticas para la lógica fueron dados por primera vez por Gottlob Frege en su Begriffsschrift de 1879, que por esta razón a menudo se considera la primera obra de la lógica moderna. Fueron perfeccionados en Principia Mathematica de Alfred North Whitehead y Bertrand Russell y por David Hilbert y sus alumnos en la década de 1920. Por lo tanto, a menudo se les llama “sistemas Frege” o “sistemas Hilbert”. Son muy versátiles ya que muchas veces es fácil encontrar un sistema axiomático para una lógica. Debido a que las derivaciones tienen una estructura muy simple y sólo una o dos reglas de inferencia, también es relativamente fácil probar cosas sobre ellas. Sin embargo, son muy difíciles de usar en la práctica, es decir, es difícil encontrar y escribir pruebas.