Soy un estudiante de lógica que recientemente se encontró con dos pruebas de geometría de columna que parecen ser la perdición de muchos estudiantes de secundaria. Mi pregunta principal, sin embargo, es que ¿hay alguna manera de hacer estas pruebas completamente en el lenguaje de la lógica de primer orden y, por lo tanto, utilizando los métodos de la deducción natural? Decir "Si dos ángulos son complementarios, entonces suman 90 grados" como justificación es demasiado, demasiado extenso para mí y parece que podría descomponerse en las deducciones frías, precisas y sin ambigüedades de la lógica formal (debería ser una premisa traducible a la lógica formal, que luego se puede utilizar para derivar otros enunciados utilizando las más de 19 reglas de inferencia). Gracias, chicos.
Respuestas
¿Demasiados anuncios?
Si le he entendido bien, ¿está buscando sistemas formales de lógica de primer orden en los que formalizar los enunciados de la geometría euclidiana?
Parece que hay varias formas de hacerlo.
-
En primer lugar, se podrían formalizar enunciados de geometría euclidiana dentro de una teoría de conjuntos FOL como ZFC, tomando ${\mathbb R}^2$ como el dominio del discurso, y demostrarlos allí (en última instancia, basándose sólo en sus axiomas de la teoría de conjuntos).
-
Como alternativa, se puede intentar factorizar este enfoque teórico de conjuntos en dos pasos:
-
En primer lugar, estableciendo un sistema de lógica de primer orden especialmente hecho para la formalización de la geometría euclidiana, y traduciendo su afirmación en una fórmula de esa teoría, y ...
-
... en segundo lugar modelar la teoría que eligió por el plano ${\mathbb R}^2$ dentro de su teoría de conjuntos ambientales.
De esta manera, una prueba formal de su traducción en el sistema FOL elegido para la geometría euclidiana producirá en particular una prueba de la traducción a la teoría de conjuntos por la solidez de la interpretación.
-
Conozco dos sistemas formales de FOL para la geometría euclidiana:
Aquí hay un artículo en el blog de las letras perdidas de Goedel que trata de las identidades elementales, que no se pueden demostrar utilizando las "matemáticas de la escuela secundaria", para saber cómo se definen las "matemáticas de alta escuela"
ver, http://rjlipton.wordpress.com/2014/07/10/high-school-theorems/
Especialmente vea la sección HSI.
Se puede hacer una formalización de la geometría basada en algunos axiomas de primer orden. Un ejemplo de tal sistema de axiomas es el sistema de Tarski. De hecho, lo hemos hecho. Puedes encontrar las pruebas comprobadas por ordenador aquí: http://geocoq.github.io/GeoCoq/ Si asumes sólo cortes Dedekind de primer orden, entonces los modelos de los axiomas de Tarski son campos reales cerrados.
