Saltar al contenido principal
LibreTexts Español

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}\)

    Template:MathJaxZach

    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.

    9.5.1.png

    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.

    9.5.2.png

    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:

    9.5.3.png

    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.

    9.5.4.png

    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í:

    9.5.5.png

    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í:

    9.5.6.png

    En cada una de las dos ramas de la derecha, queremos derivar\(A \lif B\), que se hace mejor usando\(\Intro{\lif}\).

    9.5.7.png

    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}\):

    9.5.8.png

    Mediante el uso\(\FalseInt\), podemos obtener\(B\) como conclusión y completar la rama.

    9.5.9.png

    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\).

    9.5.10.png

    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!

    9.5.11.png

    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:

    9.5.12.png

    Nuestra estrategia para encontrar una derivación de\(\lnot A\) convocatorias para una aplicación de\(\Intro{\lnot}\):

    9.5.13.png

    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}\):

    9.5.14.png

    En el lado derecho usamos la misma estrategia, excepto que nos las\(A\) arreglamos\(\FalseCl\):

    9.5.15.png

    Problema\(\PageIndex{1}\)

    Dar derivaciones de lo siguiente:

    1. \(\lnot(A \lif B) \lif (A \land \lnot B)\)

    2. \((A \lif C) \lor (B \lif C)\)de la suposición\((A \land B) \lif C\)

    3. \(\lnot \lnot A \lif A\)

    4. \(\lnot A \lif \lnot B\)de la suposición\(B \lif A\)

    5. \(\lnot A\)de la suposición\(( A \lif \lnot A )\)

    6. \(A\)a partir de los supuestos\(B \lif A\) y\(\lnot B \lif A\)


    This page titled 9.5: Ejemplos de Derivaciones is shared under a CC BY license and was authored, remixed, and/or curated by Richard Zach et al. (Open Logic Project) .