Lógica Matemática - Demostración en Lógica de Proposiciones

En el capítulo anterior estudiamos el método indirecto de refutación (y los tableaux
semánticos) y el método directo de la tablas de verdad como métodos
semánticos para vericar la validez de fórmulas y deducciones. Sin embargo,
si el número de proposiciones atómicas es elevado las tablas de verdad no son
un método eciente (para un signatura con n fórmulas atómicas, tenemos
que construir una tablas de 2n las).
La teoría de la demostración o teoría de pruebas nos proporciona
métodos alternativos a las tablas de verdad para averiguar
² la validez de una fórmula proposicional: si ' es una fórmula
válida se dice que es demostrable y se escribe ` ':
² si una fórmula ' es consecuencia lógica de un conjunto de
premisas ©: si ' es consecuencia lógica de © se dice que ' es
deducible en el sistema a partir de © y se escribe © ` ':
El objetivo principal de cualquier teoría de pruebas es demostrar la validez
de fórmulas, independientemente del contexto particular que se estén
considerando: la demostración de la validez de una fórmula o de una deducci
ón en un sistema de demostración no se desarrolla teniendo en cuenta todas
las posibles valoraciones, se obtiene utilizando una secuencia nita de pasos
y, en cada uno de ellos, se aplican las reglas de inferencia del sistema.
Ya comentamos que los sistemas de demostración se suelen dividir endos clases: sistemas directos y sistemas indirectos (o por refutación).
Los primeros aplican una cadena nita de reglas de inferencia hasta llegar
77
78
a la fórmula que se quiere demostrar. Los segundos aplican la técnica de
reducción al absurdo.
Siendo sistemas clásicos, los sistemas de demostración directos tienen
interés histórico y además son los más naturales ya que son los más cercanos
a la forma de razonamiento habitual.
Los sistemas directos son adaptables a lógicas no clásicas, pero son de
difícil automatización.
Lo sistemas de demostración indirectos son más modernos y adecuados
para su automatización, pero no son aplicables a lógicas distintas de las
lógicas clásicas.
En este capítulo estudiaremos un particular sistema de demostración axiom
ático, el sistema de deducción natural de Gentzen.
El método de los tableaux semánticos que estudiamos en la teoría interpretativa
tiene, en realidad, una estructura completamente sintáctica y, por
tanto, se puede considerar un ejemplo de sistemas de demostración axiomá-
tico indirecto.
Como veremos, es posible demostrar que estos sistemas axiomáticos son
equivalentes a la teoría interpretativa. Es decir, se puede vericar que una
fórmula proposicional es una tautología en la teoría interpretativa si y sólo si
es una fórmula válida en la teoría de la demostración que vamos a estudiar.