Axiomática geométrica

Los sistemas de axiomas.

Formas de definir los fundamentos de la geometría:
•    un enfoque sintético
•    Axiomas de Hilbert: puntos, líneas, planos + axiomas geométricos
•    Axiomas de Tarski: puntos + axiomas geométricos
•    Axiomas de Euclides
•    un enfoque analítico (partiendo de un cuerpo dado ? (generalmente ℝ) y definiendo el plano como ? n ),
•    enfoques mixtos analíticos / sintéticos asumiendo tanto un cuerpo como algunos axiomas geométricos:
•    método de área: cuerpo de inicio un cuerpo para medir distancias y áreas con signo + axiomas geométricos
•    Sistema de axiomas de estilo de Birkhoff : comience con un cuerpo para medir la distancia y los ángulos + axiomas geométricos
•    enfoques basados en grupo de transformaciones (programa de Erlangen )

Enfoque sintético.

Con Descartes y Tarski se puede demostrar que podemos definir coordenadas.
Sistema de axiomas es el de Tarski
Sistema de axiomas de Hilbert
Los axiomas de Euclides
Axiomas de Tarski (excepto la continuidad) son equivalentes a los axiomas de Hilbert (excepto la continuidad).

La formalización basada en los axiomas de Tarski

Wanda Szmielew y Alfred Tarski iniciaron el proyecto de un tratado sobre los fundamentos de la geometría.
Wolfram Schwabhäuser continuó el proyecto de Wanda Szmielew y Alfred Tarski. Publicó el tratado en 1983 en alemán: Metamathematische Methoden in der Geometrie .

•    propiedades de congruencia
•    congruencia entre propiedades
•    colinealidad
•    transitividad
•    punto medio
•    ortogonalidad
•    Reflexividad
•    ángulos
•    paralelismo
•    paralelismo usando decidibilidad de intersección
•    Demostraciones sintéticas de los teoremas de Pappus y Desargues.

longitud Longitud definida como una clase de equivalencia utilizando el predicado de congruencia.
ángulos Medida de ángulo definida como una clase de equivalencia utilizando el predicado de congruencia de ángulos.
Pappus-Pascal
Desargues Prueba de Hessenberg de que Pappus implica Desargues.

Aritmetización de la geometría

•    Suma Definición geométrica de la suma.
•    Producto Definición geométrica del producto.
•    Pedido. cuerpo Todas las pruebas necesarias para obtener un cuerpo ordenado.
•    Longitudes Definición de la longitud de un segmento usando coordenadas, definición de comparación de longitudes usando coordenadas, prueba de que estas definiciones corresponden a sus contrapartes geométricas,
•    teorema de Pitágoras,
•    teorema de Thales.
•    Coordenadas Prueba de las fórmulas para caracterizar los predicados de congruencia, intermediación, colinealidad y punto medio mediante coordenadas.
•    extensión Instanciación de estructuras de cuerpo ordenadas y conexión a la nsatztáctica para obtener prueba automáticamente utilizando la base de Gröbner.

Formalización de los elementos de Euclides

•    El primer enfoque consiste en formalizar la afirmación de Euclides sin intentar formalizar las pruebas originales.
•    formalizado la prueba de Gupta de que el punto medio puede construirse sin axiomas de continuidad círculo / círculo, mientras que la prueba original de Euclides necesita esta suposición.
•    Michael Beeson completó la formalización del primer libro de los Elementos

Conexión con los axiomas de Hilbert

Los axiomas de Tarski se siguen de los axiomas de Hilbert.

•    Tarski a Hilbert Una prueba de que los axiomas de Hilbert (sin continuidad) se siguen de los axiomas de Tarski.
•    Hilbert a Tarski Una prueba de que los axiomas de Tarski (sin continuidad) se siguen de los axiomas de Hilbert.

Variantes del sistema de axiomas de Tarski

•    Tarski a Makarios La formalización de un breve artículo de Makarios que muestra que cambiando ligeramente un axioma podemos borrar otro axioma.
•    Tarski a Beeson La prueba de que el sistema de axiomas constructivos propuesto por Beeson es clásicamente equivalente al sistema de axiomas de Tarski.
Postulados paralelos
Demostramos la equivalencia entre varias versiones del postulado paralelo, incluido el conocido postulado de Playfair y el quinto postulado de Euclides.