9.1: Reglas y Derivaciones

Última actualización
Guardar como PDF

Page ID: 103651

\( \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 naturales de deducción están destinados a ser paralelos estrechamente al razonamiento informal utilizado en la prueba matemática (de ahí que sea algo “natural”). Las pruebas naturales de deducción comienzan con suposiciones. Luego se aplican las reglas de inferencia. Los supuestos son “descargados” por las reglas\(\Intro{\lnot}\)\(\Intro{\lif}\),,\(\Elim{\lor}\) e\(\Elim{\lexists{}{}}\) inferencia, y la etiqueta de la suposición descargada se coloca al lado de la inferencia para mayor claridad.

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

Una suposición es cualquier oración en la posición más alta de cualquier rama.

Las derivaciones en deducción natural son ciertos árboles de oraciones, donde las oraciones más altas son suposiciones, y si una oración se encuentra por debajo de una, dos o tres secuentes, debe seguir correctamente por una regla de inferencia. Las oraciones en la parte superior de la inferencia se denominan premisas y la oración por debajo de la conclusión de la inferencia. Las reglas vienen en pares, una introducción y una regla de eliminación para cada operador lógico. Introducen un operador lógico en la conclusión o eliminan a un operador lógico de una premisa de la regla. Algunas de las reglas permiten dar de alta una suposición de cierto tipo. Para indicar qué suposición se descarga por qué inferencia, también asignamos etiquetas tanto a la suposición como a la inferencia. Esto se indica escribiendo el supuesto como “\(\Discharge{A}{n}\).”

Es costumbre considerar reglas para todos los operadores lógicos\(\land\), \(\lor\), \(\lif\), \(\lnot\), and \(\lfalse\), even if some of those are considered as defined.