Conclusión natural

La inferencia natural ( inferencia natural ) es un tipo de cálculo lógico que usa reglas de inferencia para probar declaraciones que están cerca de los métodos de razonamiento significativos habituales.

Por primera vez, tales cálculos fueron creados en 1934 de forma independiente por Gentsen y Yaskovsky . Junto con el cálculo secuente , pertenecen al tipo Gentzen , ya que se basan en un enfoque no axiomático (a diferencia del cálculo de Hilbert , que utiliza conjuntos desarrollados de axiomas y un mínimo de reglas de inferencia). Los sistemas de inferencia natural más famosos son los desarrollados por Gentzen (para la versión clásica del cálculo de predicados ) y (para el cálculo de predicados intuicionista ). $\mathbf {NK}$ ${\ estilo de visualización \ mathbf {NJ}}$

Reglas de inferencia en cálculo : ${\ estilo de visualización \ mathbf {NJ}}$

introducción de la conjunción : ${\cfrac {A\quad B}{A\cuña B}}$ (“si es cierto y , entonces podemos concluir ”); $A$ $B$ $A \ cuña B$
excepción de conjunción: ${\cfrac {A\cuña B}{A}}$ y ; ${\cfrac {A\cuña B}{B}}$
Introducción a la disyunción : ${\cfrac {A}{A\vee B}}$ y ; ${\cfrac {B}{A\vee B}}$
excepción de disyunción: ${\begin{alineado}A\quad B\\\vdots \;\quad \vdots \;\\{\cfrac {A\vee B\quad C\quad C}{C))\end{alineado }}$ (“si es cierto , de se deduce y de se deduce , entonces podemos concluir ”); $A\vee B$ $A$ $C$ $B$ $C$ $C$
introducción del cuantificador universal : ${\ Displaystyle {\ cfrac {Fa} {\ forall {x} Fx}}}$ ;
excepción del cuantificador universal: ${\cfrac {\forall{x}Fx}{Fa))$ ;
introducción del cuantificador existencial : ${\cfrac {Fa}{\existe {x}Fx))$ ;
exclusión del cuantificador existencial: ${\begin{alineado}Fa\\\vdots \;\\{\cfrac {\existe {x}Fx\quad C}{C))\end{alineado))$ ;
introducción de la implicación : ${\cfrac {B}{A\Flecha derecha B}}$ ;
eliminación de implicación ( modus ponens ): ${\cfrac {A\quad A\Rightarrow B}{B}}$ ;
introducción de la negación : ${\begin{alineado}A\\\vdots \;\\{\cfrac {\quad \bot }{\neg A))\end{alineado))$ ;
excepción de negación: ${\cfrac {A\quad\neg A}{\bot}}$ ;
Derivación de un enunciado falso : ${\cfrac {\bot}{A}}$ .

El sistema clásico se obtiene añadiendo un axioma a estas reglas de inferencia, o añadiendo la regla de la doble negación . $\mathbf {NK}$ $A\vee\neg A$ ${\cfrac {\neg \neg A}{A))$

Literatura

Gentzen G. Estudios de inferencia = Untersuchungen über das logische Schließen // Mathematische Zeitschrift, Bd. 39 (1934–1935), S. 405–431 // Idelson A. V., Mints G. E. Teoría matemática de la inferencia / traducido por A. V. Idelson. - M. : Nauka, 1967. - S. 9-76 .
Getmanova A. D. Lógica. - Casa del Libro "Universidad", 1998. - 480 p.
Zinoviev A. A. Lógica proposicional y teoría de la inferencia. - Pedro, 2015. - 937 p.
Pravits D. conclusión natural. Investigación basada en evidencia / traducción por P. Bystrov. —Laurie, 1997.

Lógicas

Filosofía • Semántica • Sintaxis • Historia

Grupos lógicos

lógica clásica	lógica aristotélica Lógica proposicional Lógica de primer orden Lógica de segundo orden lógica de orden superior
lógica matemática	teoría de conjuntos Teoría del modelo teoría de la computabilidad Teoría de la prueba y matemáticas constructivas lógica lineal sistema formal conclusión natural cálculo de secuencias Álgebra de la lógica Lógica relevante lógica deóntica lógica intuicionista cálculo de Lambek
Lógica no clásica	intuicionismo lógica difusa Lógica subestructural lógica Descripción lógica Lógica multivaluada Síntesis lógica Lógica vinculante Lógica temporal Lógica modal ( Lógica híbrida ) lógica epistémica
lógica filosófica	Pensamiento crítico lógica informal razonamiento deductivo

Componentes

Lista de símbolos booleanos