UMA 2022
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.
Trabajo en conjunto con: Emmanuel Gunther (Universidad Nacional de Córdoba, Argentina), Miguel Pagano (Universidad Nacional de Córdoba, Argentina) y Matías Steinberg (Universidad Nacional de Córdoba, Argentina).