¿Por qué tu computadora no entiende ZFC?
Introducción Casi toda la matemática moderna se escribe en el lenguaje de la Teoría de Conjuntos, pero casi toda la matemática verificada por computadora se hace en Teoría de Tipos. ¿Por qué existe esta discrepancia? La respuesta está en como las asignaciones de verdad y las demostraciones dependen mucho de un marco. Dentro del estudio de la lógica matemática, cuyo punto de partida busca responder a la pregunta: ¿Cómo se razona y deduce correctamente?, se debe enfatizar dos enfoques: la sintaxis y la semántica. ...