8.15: Resumen

Última actualización
Guardar como PDF

Page ID: 103620

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

Los sistemas de prueba proporcionan métodos puramente sintácticos para caracterizar la consecuencia y la compatibilidad entre oraciones. El cálculo secuente es uno de esos sistemas de prueba. Una derivación en ella consiste en un árbol de secuentes (un secuente\(\Gamma \Sequent \Delta\) consiste en dos secuencias de fórmulas separadas por\(\Sequent\)). Los secuentes superiores en una derivación son los secuentes iniciales de la forma\(A \Sequent A\). Todos los demás secuentes, para que la derivación sea correcta, deben justificarse correctamente por una de varias reglas de inferencia. Estos vienen en pares; una regla para operar en el lado izquierdo y en el lado derecho de un secuente para cada conectivo y cuantificador. Por ejemplo, si un secuente\(\Gamma \Sequent \Delta, A \lif B\) está justificado por la\(\RightR{\lif}\) regla, el secuente anterior (la premisa) debe serlo\(A, \Gamma \Sequent \Delta, B\). Algunas reglas también permiten manipular el orden o número de oraciones en una secuencia, por ejemplo, la\(\RightR{\Exchange}\) regla permite cambiar dos fórmulas en el lado derecho de una secuencia.

Si hay una derivación del secuente\(\quad \Sequent A\), decimos que\(A\) es un teorema y escribimos\(\Proves A\). Si hay una derivación de\(\Gamma_0 \Sequent A\) donde se\(\Gamma_0\) encuentra cada\(B\) in\(\Gamma\), decimos que\(A\) es derivable\(\Gamma\) y escribimos\(\Gamma \Proves A\). Si hay una derivación de\(\Gamma_0 \Sequent \quad\) dónde está cada\(B\) in\(\Gamma\), decimos que\(\Gamma_0\)\(\Gamma\) es inconsistente, por lo demás consistente. Estas nociones están interrelacionadas, por ejemplo,\(\Gamma \Proves A\) iff\(\Gamma \cup \{\lnot A\}\) es inconsistente. También están relacionados con las nociones semánticas correspondientes, e.g., si\(\Gamma \Proves A\) entonces\(\Gamma \Entails A\). Esta propiedad de los sistemas de prueba —de lo que\(\Gamma\) se puede derivar está garantizada por\(\Gamma\) — se llama solidez. El teorema de solidez se prueba por inducción sobre la longitud de las derivaciones, mostrando que cada inferencia individual conserva la validez del secuente de conclusión siempre que los secuentes de premisa sean válidos.