¿Qué le falta a la axiomatización de Tarski de la geometría euclidiana?

El lenguaje de la “geometría euclidiana elemental”, en el sentido tarskiano, consiste precisamente en aquellas declaraciones que pueden formularse usando cuantificadores de primer orden sobre puntos (“para todos los puntos …” y “existe un punto tal que …”), booleano operadores, y los conceptos “p = q”, “p está en el segmento de línea de q a r”, y “p está tan lejos de q como r está de s”. La teoría de la “geometría elemental euclidiana (plano)” será precisamente aquellas declaraciones de la forma anterior que son verdaderas en la geometría 2d familiar.

Lo que “falta” es lo que no es / no puede ser discutido en ese idioma [por ejemplo, no habla en absoluto sobre brachistochrones … Menos oscuramente, tenga en cuenta que si bien ciertos tipos de discusiones de líneas, círculos, longitudes, etc. son posibles, uno no puede decir cosas como “La longitud del círculo centrado en p que pasa por q es igual a la distancia de r a s” en este lenguaje].

Como estamos considerando con precisión las declaraciones verdaderas en este lenguaje en particular, la teoría del interés es obviamente consistente y completa; La única pregunta es si es decidible.

Tarski descubrió una lista finita de axiomas y esquemas de axiomas cuyas consecuencias fueron precisamente las afirmaciones verdaderas de la geometría euclidiana elemental, estableciendo así su capacidad de decisión.

Esa es la forma directa de pensarlo. Habiendo dicho eso, la forma más simple de ver que la geometría euclidiana elemental es decidible es, creo, usando la idea de Descartes de que las preguntas geométricas pueden convertirse en preguntas aritméticas, pensando en términos de coordenadas.

Cada declaración en el lenguaje mencionado anteriormente se puede traducir a una declaración usando cuantificadores de primer orden sobre números reales (“para todos los números reales …” y “existe un número real tal que …”), operadores booleanos, suma, multiplicación, = y <.

Dado que la teoría de las declaraciones verdaderas de esta última forma (“aritmética real elemental”) es decididamente famosa (un resultado también debido a Tarski *), también debe ser la geometría elemental del plano euclidiano (así como sus análogos en cualquier otro número finito fijo de dimensiones).

[*: Para decidir la verdad o la falsedad de una declaración en aritmética real primaria, básicamente, primero se utilizan manipulaciones lógicas estándar para colocar todos los cuantificadores al frente de la declaración, luego uno por uno elimina los cuantificadores de adentro hacia afuera usando una variante del teorema de Sturm, hasta terminar con una de las dos oraciones libres de cuantificadores en este idioma: “Verdadero” o “Falso”]

Lo que falta es la cuantificación de números. La geometría elemental está toda ahí. Puntos, líneas, círculos, ángulos, triángulos, etc. son parte del lenguaje. Todo en los primeros 4 libros de la geometría de Euclides está cubierto.

El quinto libro trata sobre la teoría de las proporciones y proporciones de Eudoxus, y el sexto incluye triángulos similares. La definición de proporción de Eudoxus implica cuantificadores para los números. Esas cosas están fuera del lenguaje descrito por Tarski para la geometría.

Hay una manera de obtener proporciones para segmentos de línea que no se basa en la definición de Eudoxus. A saber, puede decir segmentos de línea dados a, b, c y d, que a : b = c : d cuando el rectángulo a por d es igual al rectángulo b por c. Pero eso no ayudará en algo como las proporciones de ángulos.

Más tarde, en el Libro XII, Euclides usa la teoría de Eudoxus para mostrar que los círculos son proporcionales a los cuadrados en sus radios. Eso también está más allá del lenguaje de Tarski.

No soy un experto en teoría de modelos o geometría elemental, pero el propio Tarski da una explicación muy legible: ver

Tarski, Alfred. “¿Qué es la geometría elemental?” El método axiomático, con especial referencia a la geometría y la física (1959): 16-29.

http://www.corelab.ntua.gr/study

Es cierto que me gustaría ver una descripción más explícita de lo que la teoría de primer orden no puede probar, pero deja en claro que es principalmente exitoso en el manejo de declaraciones sobre muchos puntos, por lo que las declaraciones que dicen algo significativo sobre más que muchos los puntos probablemente están fuera de la imagen.