9.14: Resumen

Última actualización
Guardar como PDF

Page ID: 103636

\( \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. La deducción natural es uno de esos sistemas de prueba. Una derivación en ella consiste en fórmulas de un árbol. Las fórmulas más altas en una derivación son los supuestos. Todas las demás fórmulas, para que la derivación sea correcta, deben justificarse correctamente por una de varias reglas de inferencia. Estos vienen en pares; una introducción y una regla de eliminación para cada conectivo y cuantificador. Por ejemplo, si una fórmula\(A\) se justifica por una\(\Elim{\lif}\) regla, las fórmulas anteriores (las premisas) deben ser\(B \lif A\) y\(B\) (para algunos\(B\)). Algunas reglas de inferencia también permiten que se descarguen los supuestos. Por ejemplo, si\(A \lif B\) se infiere del\(B\) uso\(\Intro{\lif}\), cualquier suceso de\(A\) como suposiciones en la derivación que conduce a la premisa\(B\) puede ser descargada, y se le da una etiqueta que también se registra en el inferencia.

Si hay una derivación con fórmula final\(A\) y se descargan todos los supuestos, decimos que\(A\) es un teorema y escribimos\(\Proves A\). Si todos los supuestos no descargados están en algún conjunto\(\Gamma\), decimos que\(A\) es derivable\(\Gamma\) y escribir\(\Gamma \Proves A\). Si\(\Gamma \Proves \lfalse\) decimos\(\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, demostrando que cada inferencia individual preserva la vinculación de su conclusión a partir de supuestos abiertos siempre que sus premisas sean constreñidas por sus supuestos no descargados.