Logica

Demostración en Lógica de predicados
Teoría de la demostración en logica de predicados
En este capítulo estudiaremos la extensión del sistema de deducción natural
a la lógica de primer orden.Recordamos que la teoría de la demostración nos proporciona métodos
alternativos a los métodos semánticos para averiguar
² la validez de una fórmula: si ' es una fórmula válida se dice que
esdemostrable 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© ` ':
Las deniciones generales de sistema formal axiomático, teorema, deducci
ón, métodos directos y por refutación son las mismas estudiadas en
la sección 5.1 del capítulo 5. Las iremosempleando a lo largo de todo el
capítulo.
También valen el teorema de la deducción 5.1.9 y su corolario 5.1.10,
que permiten establecer la relación entre deducciones correctas y fórmulas
válidas:Teorema 8.0.1 (Teorema de la deducción) Sean f'1; '2; : : : 'ng un
conjunto de fórmulas y ' una fórmula. Entonces
f'1; '2; : : : 'ng ` ' si y sólo si f'1; '2; : : : 'n¡1g ` ('n ! '):
Corolario 8.0.2Dada una demostración de una deducción, es siempre posible
encontrar una fórmula válida que la represente.
Ya comentamos que en la lógica de primer orden no existe ningún método
de demostración quesea decidible. Por tanto, la extensión de la teoría de los
tableaux sintácticos a la lógica de primer orden no puede proporcionar un
método ecaz y nito para establecer la satisfacibilidad de unafórmula.
8.1 Denición del sistema de deducción natural
de Gentzen
La extensión del sistema de deducción natural de la lógica proposicional a
la lógica de predicados mantiene su carácter intuitivo,ya que se basa en
deducciones. Las ocho reglas de inferencia de la denición de este sistema
del capítulo 5 siguen valiendo y tienen ahora que ser completadas por reglas
de inferencia para los...