Axiomes de Tarski
Les axiomes de Tarski, dus à Alfred Tarski, sont un système d'axiomes pour la géométrie euclidienne exprimé en logique du premier ordre. Les prédicats utilisés dans le langage sont : le point y est entre les points x et z : (entre deux ou en anglais betweenness) ; la distance de x à y est égale à la distance de z à u : (congruence). A1: Réflexivité de la congruence A2: Transitivité de la congruence A3: Segment nul A4: Report de segment A5: Cinq segments A6: Identité A7: Axiome de Pasch A8: Plus petite dimension Il existe trois points non colinéaires, il n'existe donc pas de modèle de la théorie de dimension < 2. A9: Plus grande dimension Il n'existe pas de modèle de dimension > 2. A10: Axiome d'Euclide Il existe d'autres formulations équivalentes au cinquième postulat d’Euclide. Par exemple : A11: Schéma d'axiome de continuité où φ et ψ sont des formules du premier ordre ne contenant ni a ni b, φ ne contenant pas y et ψ ne contenant pas x. Au lieu de cet axiome A11, il peut être introduit un axiome de double intersection droite-cercle :
- Axiomes de congruence. Seul l’axiome A5 traite de la congruence des figures planes. L’absence d’un axiome équivalent à l’axiome de report d’angle de Hilbert rend la construction du milieu d’un segment plus délicate. Elle emprunte les étapes suivantes : L’orthogonalité est ainsi définie : trois points a, b, et c forment un angle droit de sommet a, si, c’ étant le symétrique de c par rapport à a, bc et bc’ sont congruents. La construction du milieu d’un segment est d’abord effectuée pour un segment disposant d’un point équidistant de ses extrémités. L'axiome de double intersection droite-cercle permet la construction aisée de la perpendiculaire abaissée d’un point sur une droite. La construction de Gupta permet toutefois de se dispenser de cet axiome, au prix d'un développement beaucoup plus laborieux. La définition de la symétrie par rapport à une droite, isométrie conservant la relation d'interposition. La construction de la perpendiculaire à une droite élevée d’un point de cette droite.