8: El Cálculo Secuente
- Page ID
- 103611
\( \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}}\)
- 8.1: Reglas y Derivaciones
- Un secuente es una expresión de la forma\(\Gamma \Rightarrow \Delta\). \(\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.
- 8.2: Reglas proposicionales
- Reglas para\(\lnot\),\(\land\),\(\lor\), y\(\rightarrow\)
- 8.3: Reglas del cuantificador
- Reglas para\(\forall\) y\(\exists\)
- 8.4: Reglas Estructurales
- También necesitamos unas reglas que nos permitan reorganizar oraciones en el lado izquierdo y derecho de una secuencia.
- 8.5: Derivaciones
- 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.
- 8.6: Ejemplos de Derivaciones
- Ejemplos de\(\mathbf{LK}\) -derivaciones para los secuentes\(A \land B \Rightarrow A\), y\(\lnot A \lor B \Rightarrow A \rightarrow B\)\(\lnot A \lor \lnot B \Rightarrow \lnot (A \land B)\), y un ejemplo de la regla de contracción
- 8.7: Derivaciones con cuantificadores
- Un ejemplo de una\(\mathbf{LK}\) -derivación de la secuencia\(\exists{x}\,{\lnot A(x)} \Rightarrow \lnot \forall{x}\,{A(x)}\)
- 8.8: Nociones teóricas de prueba
- Así como hemos definido una serie de nociones semánticas importantes (validez, vinculación, satisfacción), ahora definimos nociones teóricas de prueba correspondientes. Estos no se definen por la apelación a la satisfacción de las sentencias en las estructuras, sino por la apelación a la derivabilidad o no derivabilidad de ciertos secuentes. Fue un descubrimiento importante que estas nociones coincidan. Lo que hacen es el contenido del teorema de solidez e integridad.
- 8.9: Derivabilidad y consistencia
- Ahora estableceremos una serie de propiedades de la relación de derivabilidad. Son independientemente interesantes, pero cada uno jugará un papel en la prueba del teorema de integridad.
- 8.12: Solidez
- Un sistema de derivación, como el cálculo secuente, es sólido si no puede derivar cosas que realmente no se sostienen.
- 8.13: Derivaciones con predicado de identidad
- Las derivaciones con predicado de identidad requieren secuestros iniciales adicionales y reglas de inferencia.
- 8.14: Validez con predicado de identidad
- \(\mathbf{LK}\)con secuentes iniciales y reglas para la identidad es sólida.