Sistema Gentzen
Un poco de historia
El sistema Gentzen como su nombre lo indica fue creado por Gerhard Gentzen quien fue un Matemático y lógico alemán. Nacido el 24 de noviembre de 1909 en Greifswald (Alemania), murió el 4 de agosto de 1945 en Praga (República Checa) como prisionero poco después de terminar la guerra.
Sus principales trabajos fueron en las fundaciones de la matemática y la teoría de la demostración. En 1934, Gentzen introduce la noción de sistema de deducción natural para lógica clásica y lógica intuicionista. Demuestra que toda prueba puede escribirse de manera normalizada sin cortes. Para ello introduce el cálculo de consecuencias lógicas o secuentes. En 1936, Gentzen demuestra la consistencia de la teoría elemental de números.
Definiciones
El sistema de Gentzen es un sistema deductivo similar al método del tableaux tanto en su desarrollo como en su función, con la diferencia que el método del tableaux parte de la meta negando la formula original y el sistema Gentzen de las literales que contiene la formula.
Para desarrollar el sistema Gentzen de manera mas sencilla podemos basarnos del tableaux (El sistema de Gentzen es el tableaux al revés) empezando con tomar los átomos resultantes del tableaux cambiando el signo ya que en el tableaux negamos la formula original, para continuar con el proceso seguimos los pasos del tableaux de forma ascendente usando las tablas del sistema Gentzen mostradas en la siguiente sección.
Tautología: Es aquella proposición (compuesta) que es cierta para todos los valores de verdad de sus variables . Formula valida. Se representa con el símbolo ╞
Ejemplos
Para resolver los siguientes ejemplos se usaron las tablas de Gentzen las cuales se encuentran eleboradas para casos genericos.
| α1 | α2 | α |
| ¬¬A | A | |
| A1 | A2 | ¬(¬A1 Λ ¬A2) |
| A1 | A2 | A1 V A2 |
| A1 | A2 | ¬A1→ A2 |
| A1 | A2 | A1 ↑ A2 |
| A1 | A2 | A1 ↓ A2 |
| ¬(A1→A2) | ¬(A2→A1) | ¬(A1↔A2) |
| ¬(A1→A2) | ¬(A2→A1) | A1 Θ A2 |
| β1 | β2 | β |
| B1 | B2 | B1 Λ B2 |
| B1 | B2 | ¬(¬B1 V ¬B2) |
| B1 | B2 | ¬(B1→¬B2) |
| B1 | B2 | B1 ↑ B2 |
| B1 | B2 | B1 ↓ B2 |
| ¬(B1→B2) | ¬(B2→B1) | ¬(B1↔B2) |
| ¬(B1→B2) | ¬(B2→B1) | B1 Θ B2 |
Ejemplo 1.0 comprobación de (p v q)→(q v p)
∴Demostramos que (p v q)→(q v p) es una tautologia.
Ejemplo 2.0 comprobación de (¬b → ¬a)→(a → b)
∴ Demostramos que (¬b → ¬a)→(a → b) es una tautologia.
| <= | Ejercicios desarrollados paso a paso con el Sistema Gentzen, realizados por: Alma Cristina Martinez Lopez |
| <= | Tema Anterior: 2.4.1 Pruebas Deductivas |
| => | Siguiente Tema: 2.4.3 Sistemas de Hilbert |
| Regresar al TEMARIO: Matematicas para Maestria |
