Saltar al contenido principal
Library homepage
 
LibreTexts Español

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.10: Derivabilidad y los conectivos proposicionales
    • 8.11: Derivabilidad y los cuantificadores
    • 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.
    • 8.15: Resumen


    This page titled 8: El Cálculo Secuente is shared under a CC BY license and was authored, remixed, and/or curated by Richard Zach et al. (Open Logic Project) .