8.5: Derivaciones

Última actualización
Guardar como PDF

Page ID: 103638

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

Template:MathJaxZach

Hemos dicho cómo es un secuente inicial, y hemos dado las reglas de inferencia. Derivaciones en el cálculo secuente se generan inductivamente a partir de estos: cada derivación es un secuente inicial por sí mismo, o consiste en una o dos derivaciones seguidas de una inferencia.

Definición\(\PageIndex{1}\): \(\Log{LK}\) derivation

Una\(\Log{LK}\) derivación de un secuente\(S\) es un árbol de secuentes que satisface las siguientes condiciones:

Los secuentes superiores del árbol son los secuentes iniciales.
El secuente más bajo del árbol es\(S\).
Cada secuencia en el árbol excepto\(S\) es una premisa de una correcta aplicación de una regla de inferencia cuya conclusión se encuentra directamente debajo de esa secuencia en el árbol.

Entonces decimos que\(S\) es el secuente final de la derivación y que\(S\) es derivable en\(\Log{LK}\) (o\(\Log{LK}\) -derivable).

Ejemplo\(\PageIndex{1}\)

Cada secuencia inicial, p. ej.,\(C \Sequent C\) es una derivación. Podemos obtener una nueva derivación de esto aplicando, digamos, la\(\LeftR{\Weakening}\) regla,

8.5.1.png

La regla, sin embargo, pretende ser general: podemos sustituir el\(A\) en la regla por cualquier frase, por ejemplo, también con\(D\). Si la premisa coincide con nuestro secuente inicial\(C \Sequent C\), eso significa que ambos\(\Gamma\) y\(\Delta\) son justos\(C\), y la conclusión sería entonces\(D, C \Sequent C\). Entonces, lo siguiente es una derivación:

8.5.2.png

Ahora podemos aplicar otra regla, digamos\(\LeftR{\Exchange}\), que nos permite cambiar dos oraciones a la izquierda. Entonces, lo siguiente también es una derivación correcta:

8.5.3.png

En esta aplicación de la norma, la cual se dio como

8.5.4.png

ambos\(\Gamma\) y\(\Pi\) estaban vacíos,\(\Delta\) es\(C\), y los papeles de\(A\) y\(B\) son interpretados por\(D\) y\(C\), respectivamente. De la misma manera, también vemos que

8.5.5.png

es una derivación. Ahora podemos tomar estas dos derivaciones, y combinarlas usando\(\RightR{\land}\). Esa regla era

8.5.6.png

En nuestro caso, los locales deben coincidir con los últimos secuentes de las derivaciones que terminan en las premisas. Eso quiere decir que\(\Gamma\) es\(C, D\),\(\Delta\) está vacío,\(A\) es\(C\) y\(B\) es\(D\). Entonces la conclusión, si la inferencia debe ser correcta, es\(C, D \Sequent C \land D\).

8.5.7.png

Por supuesto, también podemos revertir las premisas, entonces\(A\) sería\(D\) y\(B\) sería\(C\).

8.5.8.png