7.3: Deducción natural
- Page ID
- 103507
\( \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}\)La deducción natural es un sistema de derivación destinado a reflejar el razonamiento real (especialmente el tipo de razonamiento regido empleado por los matemáticos). El razonamiento real procede por una serie de patrones “naturales”. Por ejemplo, la prueba por casos nos permite establecer una conclusión sobre la base de una premisa disyuntiva, estableciendo que la conclusión se deriva de cualquiera de los disjuntos. La prueba indirecta nos permite establecer una conclusión demostrando que su negación conduce a una contradicción. La prueba condicional establece una pretensión condicional “si... entonces...” demostrando que el consecuente se desprende del antecedente. La deducción natural es una formalización de algunas de estas inferencias naturales. Cada una de las conectivas lógicas y cuantificadores viene con dos reglas, una regla de introducción y una de eliminación, y cada una de ellas corresponde a uno de esos patrones de inferencia natural. Por ejemplo,\(\Intro{\lif}\) corresponde a prueba condicional, y\(\Elim{\lor}\) a prueba por casos. Una regla particularmente simple es la\(\Elim{\land}\) que permite la inferencia de\(A \land B\) a\(A\) (o\(B\)).
Una característica que distingue a la deducción natural de otros sistemas de derivación es su uso de suposiciones. Una derivación en deducción natural es un árbol de fórmulas. Una sola fórmula se encuentra en la raíz del árbol de fórmulas, y las “hojas” del árbol son fórmulas de las que se deriva la conclusión. En la deducción natural, algunas fórmulas foliares juegan un papel dentro de la derivación pero se “utilizan” para cuando la derivación llega a la conclusión. Esto corresponde a la práctica, en el razonamiento real, de introducir hipótesis que sólo permanecen vigentes por un corto tiempo. Por ejemplo, en una prueba por casos, asumimos la verdad de cada uno de los disjuntos; en la prueba condicional, asumimos la verdad del antecedente; en la prueba indirecta, asumimos la verdad de la negación de la conclusión. Esta forma de introducir supuestos hipotéticos y luego eliminarlos al servicio de establecer un paso intermedio es un sello de deducción natural. Las fórmulas a las hojas de una derivación de deducción natural se denominan supuestos, y algunas de las reglas de inferencia pueden “descargarlas”. Por ejemplo, si tenemos una derivación\(B\) de algunos supuestos que incluyen\(A\), entonces la\(\Intro{\lif}\) regla nos permite inferir\(A \lif B\) y descargar cualquier suposición de la forma\(A\). (Para realizar un seguimiento de qué supuestos se descargan en qué inferencias, etiquetamos la inferencia y los supuestos que descarga con un número). Los supuestos que permanecen sin descargar al final de la derivación son en conjunto suficientes para la verdad de la conclusión, por lo que una derivación establece que sus supuestos no descargados conllevan su conclusión.
La relación\(\Gamma \Proves A\) basada en la deducción natural sostiene si hay una derivación en la que\(A\) se encuentra la última frase en el árbol, y cada hoja que no está descargada está en\(\Gamma\). \(A\)es un teorema en deducción natural si hay una derivación en la que\(A\) se encuentra la última frase y se descargan todos los supuestos. Por ejemplo, aquí hay una derivación que muestra que\(\Proves (A \land B) \lif A\):
La etiqueta\(1\) indica que la suposición\(A \land B\) se descarga a la\(\Intro{\lif}\) inferencia.
Un conjunto\(\Gamma\) es inconsistente iff\(\Gamma \Proves \lfalse\) en deducción natural. La regla\(\FalseInt{}\) hace que a partir de un conjunto inconsistente, se pueda derivar cualquier oración.
Los sistemas naturales de deducción fueron desarrollados por Gerhard Gentzen y Stanisław Jaśkowski en la década de 1930, y más tarde desarrollados por Dang Prawitz y Frederic Fitch. Debido a que sus inferencias reflejan métodos naturales de prueba, es favorecida por los filósofos. Las versiones desarrolladas por Fitch se utilizan a menudo en libros de texto de lógica introductoria. En la filosofía de la lógica, las reglas de deducción natural a veces se han tomado para dar los significados de los operadores lógicos (“semántica probadora-teórica”).