INVESTIGADORES
SANCHEZ TERRAF Pedro Octavio
congresos y reuniones científicas
Título:
La independencia de CH formalizada en Isabelle/ZF
Autor/es:
PEDRO SÁNCHEZ TERRAF; GUNTHER, EMMANUEL; PAGANO, MIGUEL; MATÍAS STEINBERG
Lugar:
Neuquén
Reunión:
Congreso; Reunión de la Unión Matemática Argentina; 2022
Institución organizadora:
Unión Matemática Argentina
Resumen:
Como es bien sabido, Cohen demostró mediante la técnica de forzamiento o forcing que la Hipótesis del Continuo ($mathit{CH}$) no se sigue de los axiomas $mathit{ZFC}$ de la teoría de conjuntos, ganando así una medalla Fields.$mathit{ZFC}$ no es finitamente axiomatizable, y posee dos esquemas de axiomas: Reemplazo y Separación (que en realidad es reducible al primero). En esta charla contaré algunos detalles sobre nuestra formalización en computadora, usando el asistente de pruebas Isabelle, de dicho resultado de Cohen. Uno de los puntos destacados es que identificamos un conjunto de 34 instancias del Axioma de Reemplazo que son suficientes para construir modelos contables transitivos de $mathit{CH}$ y su negación.
