| الوصف: |
“La lógica, a lo largo de los últimos doscientos años, se ha diversificado en su alcance. En la actualidad, para llevar a cabo su investigación, un lógico puede requerir conocimientos de teoría de conjuntos, teoría de prueba, teoría de modelos, computabilidad, aritmética, teoría de categorías, topología, lenguajes de programación, teorías de tipos y/o álgebra. Esta diversidad se dio principalmente por las contribuciones de las matemáticas en la lógica y viceversa. En el presente trabajo el interés recae en la interrelación entre la lógica y los fundamentos de las matemáticas. Particularmente, en la formalización de los teoremas matemáticos dentro de un sistema lógico. Es sabido que esto se puede hacer de diversas maneras, siendo la predilecta en los cursos de licenciatura, la formalización de las matemáticas en la teoría de conjuntos ZFC (Zermelo-Fraenkel-Choice). No obstante, otras aproximaciones al problema menos conocidas tienen ventajas y desventajas en comparación con ésta. Con el motivo de mostrar la variedad de sistemas en los cuales se pueden axiomatizar las matemáticas, el presente trabajo exhibe la formalización estándar de las matemáticas en el sistema ZFC así como una implementación moderna en la denominada teoría de tipos homotopía, HoTT. A la par se efectúa una comparación conceptual entre ambos enfoques.” |