9.5: Ejemplos de Derivaciones
- Page ID
- 103627
\( \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}\)Ejemplo\(\PageIndex{1}\)
Demos una derivación de la oración\((A \land B) \lif A\).
Comenzamos por escribir la conclusión deseada en la parte inferior de la derivación.
A continuación, necesitamos averiguar qué tipo de inferencia podría resultar en una oración de esta forma. El principal operador de la conclusión es\(\lif\), así que intentaremos llegar a la conclusión usando la\(\Intro{\lif}\) regla. Lo mejor es anotar los supuestos involucrados y etiquetar las reglas de inferencia a medida que avanza, por lo que es fácil ver si todos los supuestos han sido dados de alta al final de la prueba.
Ahora necesitamos rellenar los pasos desde el supuesto\(A \land B\) hasta\(A\). Ya que solo tenemos un conectivo con el que lidiar\(\land\),, debemos usar la regla\(\land\) elim. Esto nos da la siguiente prueba:
Ahora tenemos una correcta derivación de\((A \land B) \lif A\).
Ejemplo\(\PageIndex{2}\)
Ahora vamos a dar una derivación de\((\lnot A \lor B) \lif (A \lif B)\).
Comenzamos por escribir la conclusión deseada en la parte inferior de la derivación.
Para encontrar una regla lógica que nos pudiera dar esta conclusión, miramos las conectivas lógicas en la conclusión:\(\lnot\),\(\lor\), y\(\lif\). Solo nos importa en este momento la primera ocurencia de\(\lif\) porque es el operador principal de la oración en el final secuente, mientras que\(\lnot\),\(\lor\) y la segunda ocurre de\(\lif\) están dentro del alcance de otro conectivo, por lo que vamos a encargarse de esos más tarde. Por lo tanto, comenzamos con la\(\Intro{\lif}\) regla. Una aplicación correcta debe verse así:
Esto nos deja con dos posibilidades para continuar. O podemos seguir trabajando de abajo hacia arriba y buscar otra aplicación de la\(\Intro{\lif}\) regla, o podemos trabajar de arriba hacia abajo y aplicar una\(\Elim{\lor}\) regla. Apliquemos este último. Utilizaremos la suposición\(\lnot A \lor B\) como la premisa más a la izquierda de\(\Elim{\lor}\). Para una aplicación válida de\(\Elim{\lor}\), las otras dos premisas deben ser idénticas a la conclusión\(A \lif B\), pero cada una puede derivarse a su vez de otra suposición, a saber, los dos desjuntos de\(\lnot A \lor B\). Entonces nuestra derivación se verá así:
En cada una de las dos ramas de la derecha, queremos derivar\(A \lif B\), que se hace mejor usando\(\Intro{\lif}\).
Para las dos partes faltantes de la derivación, necesitamos derivaciones de\(B\) desde\(\lnot A\) y\(A\) en el medio, y desde\(A\) y\(B\) por la izquierda. Tomemos primero el primero. \(\lnot A\)y\(A\) son las dos premisas de\(\Elim{\lnot}\):
Mediante el uso\(\FalseInt\), podemos obtener\(B\) como conclusión y completar la rama.
Veamos ahora la rama más a la derecha. Aquí es importante darse cuenta de que la definición de derivación permite que los supuestos sean dados de alta pero no requiere que sean. Es decir, si podemos\(B\) derivar de uno de los supuestos\(A\) y\(B\) sin usar el otro, está bien. Y\(B\) derivar de\(B\) ello es trivial:\(B\) por sí misma es tal derivación, y no se necesitan inferencias. Entonces podemos simplemente borrar la suposición\(A\).
Obsérvese que en la derivación terminada, la\(\Intro{\lif}\) inferencia más a la derecha en realidad no descarga ningún supuesto.
Ejemplo\(\PageIndex{3}\)
Hasta el momento no hemos necesitado la\(\FalseCl{}\) regla. Es especial en que nos permite descargar una suposición que no es una subfórmula de la conclusión de la regla. Está estrechamente relacionado con la\(\FalseInt{}\) regla. De hecho, la\(\FalseInt{}\) regla es un caso especial de la\(\FalseCl{}\) regla—hay una lógica llamada “lógica intuicionista” en la que sólo\(\FalseInt{}\) se permite. La\(\FalseCl{}\) regla es un último recurso cuando nada más funciona. Por ejemplo, supongamos que queremos derivar\(A \lor \lnot A\). Nuestra estrategia habitual sería intentar derivar\(A \lor \lnot A\) usando\(\Intro{\lor}\). Pero esto requeriría que deriváramos\(A\) o\(\lnot A\) de ninguna suposición, y esto no se puede hacer. \(\FalseCl{}\)al rescate!
Ahora estamos buscando una derivación\(\lfalse\) de\(\lnot(A \lor \lnot A)\). Ya que\(\lfalse\) es la conclusión de que\(\Elim{\lnot}\) podríamos intentar que:
Nuestra estrategia para encontrar una derivación de\(\lnot A\) convocatorias para una aplicación de\(\Intro{\lnot}\):
Aquí, podemos obtener\(\lfalse\) fácilmente aplicándonos\(\Elim{\lnot}\) a la suposición\(\lnot(A \lor \lnot A)\) y\(A \lor \lnot A\) que se desprende de nuestra nueva suposición\(A\) por\(\Intro{\lor}\):
En el lado derecho usamos la misma estrategia, excepto que nos las\(A\) arreglamos\(\FalseCl\):
Problema\(\PageIndex{1}\)
Dar derivaciones de lo siguiente:
-
\(\lnot(A \lif B) \lif (A \land \lnot B)\)
-
\((A \lif C) \lor (B \lif C)\)de la suposición\((A \land B) \lif C\)
-
\(\lnot \lnot A \lif A\)
-
\(\lnot A \lif \lnot B\)de la suposición\(B \lif A\)
-
\(\lnot A\)de la suposición\(( A \lif \lnot A )\)
-
\(A\)a partir de los supuestos\(B \lif A\) y\(\lnot B \lif A\)