Sistema De Deducción Natural

Sistema de deducción natural
Como sistema de deducción natural, el juego de la lógica, o la puesta en funcionamiento del cálculo, consiste en ver si la conclusión de un razonamiento se deriva de las premisas mediante transformaciones de éstas según las reglas de transformación del cálculo. A este proceso le vamos a denominar derivación. Una derivación es una secuencia de transformacionesdesde las premisas de lasque partimos a la conclusión que queremos obtener. Las transformaciones posibles que se pueden realizar vienen delimitadas por el conjunto de reglas de transformación del cálculo. Diremos que un argumento es lógicamente válido si existe una derivación de la conclusión a partir de las premisas, empleando las reglas del cálculo, en otro caso diremos que el argumento eslógicamente incorrecto. ¿Cuá-les son las reglas de transformación de nuestro cálculo proposicional?. Si lo que tenemos que hacer es transformar fórmulas, estas transformaciones, teniendo en cuenta el vocabulario del que disponemos, consistirán en producir fórmulas más complejas a partir de tras más simples introduciendo nuevas conectivas entre ellas, o simplificarlas eliminando las conectivas que esténpresentes en las fórmulas dadas. Lógicamente entonces, para cada conectiva del cálculo existirán dos reglas una de introducción de la conectiva y otra de eliminación de la misma. Las reglas expresan las condiciones que tienen que ocurrir para pasar de unas fórmulas a otras. Estas condiciones quedan por encima de la raya que simboliza la transformación, la nueva fórmula se coloca por debajo de laraya. Es decir, una regla de transformación se puede leer de la siguiente manera: "si en el curso de una derivación, me encuentro con u obtengo las fórmulas que aparecen por encima de la raya, entonces en el siguiente paso de la derivación puedo escribir la fórmula que aparece debajo de la raya".

Reglas de inferencia: Una regla de inferencia es una función que va de conjuntos de fórmulas afórmulas. Al conjunto de fórmulas que la función toma como argumento se lo llama premisas, mientras que a la fórmula que devuelve como valor se la llama conclusión. En general se busca que las reglas de inferencia transmitan la verdad de las premisas a la conclusión. Es decir, que sea imposible que las premisas sean verdaderas y la conclusión falsa. En el caso de L, la única regla de inferenciaes el modus ponens, el cual dice: Recordando que y no son fórmulas, sino metavariables que pueden ser reemplazadas por cualquier fórmula bien formada.
Ejemplo de una demostración
A demostrar:

Paso Fórmula Razón
1
Instancia del primer axioma.
2
Instancia del primer axioma.
3
Instancia del segundo axioma.
4
Desde (2) y (3) por modus ponens.
5
Desde (1) y (4) pormodus ponens. QED

La deducción natural es una aproximación a la teoría de la demostración en la que se busca capturar la manera en que los humanos razonan naturalmente al construir demostraciones matemáticas.1 2 En vez de contar con unos pocos axiomas a los que se aplican unas pocas reglas de inferencia, la deducción natural propone vaciar la lista de axiomas y ampliar la de reglas deinferencia, introduciendo dos reglas para cada constante lógica: una para introducirla y otra para eliminarla.2 Una demostración se contruye partiendo de supuestos y aplicando las reglas para llegar a la conclusión deseada. La deducción natural fue introducida por Gerhard Gentzen en su trabajo Investigaciones sobre la inferencia lógica (Untersuchungen über das logische Schliessen), publicado en1934-1935.2
Reglas de inferencia
Conectiva Nombre de la regla Abreviación Formalización Cálculo de secuentes

Introducción de la negación


Eliminación de la negación




Introducción de la conjunción




Eliminación de la conjunción





Introducción de la disyunción




Eliminación de la disyunción





Introducción del condicional material...