UNIVERSIDAD NACIONAL DEL SUR
BAHIA BLANCA ARGENTINA
1 3
DEPARTAMENTO DE MATEMÁTICA PROGRAMA DE: Teoría de la Demostración Curso
Posgrado
HORAS PROFESOR RESPONSABLE
100 hs. Dr. Martín Figallo
REQUISITOS PREVIOS
Se requiere Fundamentos de la Matemática cursada y/o aprobada.
DESCRIPCI ÓN
La teoría de la demostración o (teoría de la prueba) es una rama de la lógica matemática que trata a
las demostraciones como objetos formales, facilitando su análisis mediante diferentes técnicas. Las
demostraciones suelen presentarse como estructuras definidas inductivamente que se construyen de
acuerdo con ciertas reglas (axiomas, reglas de inferencia) de los sistemas lógicos. Del estudio de las
demostraciones formales se infieren importantes propiedades de la lógica. El curso se dictará en dos
clases semanales (teórico-prácticas) de tres horas de duración.
OBJETIVOS
El objetivo del curso es introducir al alumno en los tópicos básicos de la Teoría de la Demostración. Se
presentarán diferentes formalismos para presentar un sistema lógico sintáctico (cálculos de Hilbert,
cálculos de secuentes y deducción natural). Se presentarán y demostrarán los resultados más relevantes
del área como, por ejemplo, el Teorema de Eliminación de Corte, Propiedad de la Subfórmula, etc., y
sus consecuencias (decidibilidad, consistencia, interpolación, etc.).
MOTIVACIÓN O FUNDAMENTACIÓN DEL CURSO
La Teoría de la Demostración es una de las disciplinas más importantes de la Lógica Matemática y es
Uunto a la teoría de modelos, teoría de conjuntos y teoría de la recursión) uno de los cuatro pilares
fundamentales de los fundamentos de la matemática. Por lo que resulta un tópico de fundamental
importancia para cualquier alumno que pretenda desempeñarse en la Lógica Matemática.
MECANISMO DE EVALUACIÓN
La evaluación constará de un examen final.
lAÑO 2017
UNIVERSIDAD NACIONAL DEL SUR 2 3
BAHIA BLANCA ARGENTINA DEPARTAMENTO DE MATEMÁTICA
PROGRAMA DE: Teoría de la Demostración Curso Posgrado
PROGRAMA
Unidad 1: La lógica proposicional clásica (CPL) y la lógica proposicional intuicionista (IPL).
Definición, contrapartidas algebraicas (Álgebras de Boole y Álgebras de Heyting). Cálculos de
Hilbert para CPL e IPL. Teoremas de Correctitud y Completitud.
Unidad 11: Cálculos de secuentes (de Gentzen) . Los cálculos LK y LJ. Reglas estructurales y reglas
lógicas. La regla de corte. Demostraciones formales. Reglas admisibles y derivables. Teoremas de
Correctitud y Completitud, Principio de Inversión.
Unidad lB: Propiedad de la Subfórmula y Teorema de Eliminación de Corte (Hauptsatz).
Consecuencias del Teorema de Eliminación de Corte: Consistencia, Teorema de interpolación de
Craig, Decidibilidad, etc.
Unidad IV: Deducción Natural. Reglas de introducción y de eliminación de conectivos.
Deducciones estilo árbol. Pasos de reducción. Principio de inversión. Teoremas de Correctitud y
Completitud. Deducciones normales y deducciones de longitud mínima. Teorema de las
demostraciones normales y consecuencias.
Unidad V: Eliminación de corte algebraica. Completaciones de álgebras. Matrices de Gentzen.
Cuasi-completaciones y eliminación de corte
Unidad VI: Extensiones a la lógica clásica e intuicionista de primer orden.
lAÑO 2017
3 3UNIVERSIDAD NACIONAL DEL SUR
BAHIA BLANCA ARGENTINA DEPARTAMENTO DE MATEMÁTICA
Curso Posgrado
PROGRAMA DE: Teoría de la Demostración
BIBLIOGRAFIA
1. G. Gentzen. Untersuchungen uber das logische Schliessen, Mathematische Zeitschrift, 39, pp 176-210,405-431 (1935).
2. G. Gentzen. Recherches sur la d'eduction Logique traduit de L' Allemand par R. Feys et 1. Ladri'ere, Presses Universitaires de France, 108, Boulevard Saint-Germain, Paris, 1955.
3. J. Y. Girard, Y. Lafont and P. Taylor. Proofs and Types, Cambridge University Press, Cambridge, 1989.
4. 1. Y. Girard. Prooftheory and Logical Complexity, Bibliopolis, 1987.
5. G. Takeuti. ProofTheory. Second edition, North-Holland, 1987.
6. D. Prawitz. Natural deduction: A proof-theoretical stucly. Mineola, New York: Dover Publications (2006) [1965]. ISBN 978-0-486-44654.
7. F. Belardinelli, P. Jipsen and H. Ono, AIgebraic aspects of cut elimination. Studia Logica, 77, 209-240 (2004).
8. N. Galatos, P. Jipsen, T. Kowalski and H. Ono. Residuated Lattices : An AIgebraic Glimpse at Substructural Logics, Elsevier Science, 2007.
9. H. Ono, Completions of Algebras and Completeness ofModal and Substructural Logics, Advances in Modal Logic, Volume 4,335-353 (2003).
/PROFESOR RESPONSABLE AÑO DIRECTOR D~ARTAl\1ENTO
2017 Oro SHELDY JAVIER o SROSI DIRECTOR OECA o~it
• . , ,. oO. ••Dr. Martín Figallo _-. .... .:.h . r... .• _-' __ .j j •• ~,_:r:.jt:C:1
AÑO I 2017 I I I I I I I I !
Top Related