8.1: Reglas y Derivaciones

Última actualización
Guardar como PDF

Page ID: 103619

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

Para lo siguiente, vamos a\(\Gamma, \Delta, \Pi, \Lambda\) representar secuencias finitas de oraciones.

Definición\(\PageIndex{1}\): Sequent

Un secuente es una expresión de la forma\[\Gamma \Sequent \Delta\nonumber\] donde\(\Gamma\) y\(\Delta\) son secuencias finitas (posiblemente vacías) de oraciones de la lengua\(\Lang L\). \(\Gamma\)se llama el antecedente, mientras que\(\Delta\) es el sucesivo.

La idea intuitiva detrás de un secuente es: si todas las oraciones en el antecedente se mantienen, entonces al menos una de las oraciones del sucesivo sostiene. Es decir, si\(\Gamma = \tuple{A_1, \dots, A_m}\) y\(\Delta = \tuple{B_1, \dots, B_n}\), entonces\(\Gamma \Sequent \Delta\) sostiene iff\[(A_1 \land \cdots \land A_m) \lif (B_1 \lor \cdots \lor B_n)\nonumber\] sostiene. Hay dos casos especiales: dónde\(\Gamma\) está vacío y cuándo\(\Delta\) está vacío. Cuando\(\Gamma\) está vacío, es decir,\(m = 0\),\(\quad \Sequent \Delta\) sostiene iff\(B_1 \lor \dots \lor B_n\) sostiene. Cuando\(\Delta\) está vacío, es decir,\(n = 0\),\(\Gamma \Sequent \quad\) sostiene iff\(\lnot(A_1 \land \dots \land A_m)\) hace. Decimos que un secuente es válido si la oración correspondiente es válida.

Si\(\Gamma\) es una secuencia de oraciones, escribimos\(\Gamma, A\) para el resultado de agregar\(A\) al extremo derecho de\(\Gamma\) (y\(A, \Gamma\) para el resultado de agregar\(A\) al extremo izquierdo de\(\Gamma\)). Si\(\Delta\) es una secuencia de oraciones también, entonces\(\Gamma, \Delta\) es la concatenación de las dos secuencias.

Definición\(\PageIndex{2}\): Initial Sequent

Un secuente inicial es un secuente de una de las siguientes formas:

\(A \Sequent A\)
\(\lfalse \Sequent \quad\)

para cualquier oración\(A\) en el idioma.

Las derivaciones en el cálculo secuente son ciertos árboles de secuentes, donde los secuentes superiores son secuentes iniciales, y si un secuente se encuentra por debajo de uno o dos secuentes, debe seguir correctamente por una regla de inferencia. Las reglas para\(\Log{LK}\) se dividen en dos tipos principales: reglas lógicas y reglas estructurales. Las reglas lógicas se nombran por el operador principal de la oración que contiene\(A\) y/o\(B\) en el secuente inferior. Cada una viene en dos versiones, una para inferir una secuencia con la oración que contiene el operador lógico a la izquierda, y otra con la oración a la derecha.