Axiomes de Tarski
![Page d’aide sur l’homonymie](http://upload.wikimedia.org/wikipedia/commons/thumb/a/a9/Logo_disambig.svg/20px-Logo_disambig.svg.png)
Pour l’article homonyme, voir l'axiome de Tarski en théorie des ensembles, dans Théorie des ensembles de Tarski-Grothendieck (en)..
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).
Axiomes
A1: Réflexivité de la congruence
A2: Transitivité de la congruence
A3: Segment nul
A4: Report de segment
A5: Cinq segments
![](http://upload.wikimedia.org/wikipedia/commons/thumb/e/ea/Tarski%27s_formulation_of_Pasch%27s_axiom.svg/220px-Tarski%27s_formulation_of_Pasch%27s_axiom.svg.png)
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.
![](http://upload.wikimedia.org/wikipedia/commons/thumb/e/e4/Points_in_a_plane_equidistant_to_two_given_points_lie_on_a_line.svg/220px-Points_in_a_plane_equidistant_to_two_given_points_lie_on_a_line.svg.png)
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[1] :
![](http://upload.wikimedia.org/wikipedia/commons/thumb/1/17/Tarski%27s_continuity_axiom.svg/220px-Tarski%27s_continuity_axiom.svg.png)
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 [2]:
Commentaires
1. 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[2] :
- 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[3].
- 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.
- Cette dernière permet enfin la construction du milieu d’un segment quelconque, sans l’axiome d’Euclide.
2. Axiome de Pasch.
L’axiome A7 est à la fois plus restrictif et moins restrictif que l’axiome de Pasch dans le système de Hilbert, qui affirme : Soient trois points xyz non colinéaires et u un point du segment zx distinct de z et x. Si une droite d coupe le segment xz en u, elle coupe aussi soit le segment xy soit le segment yz
L’axiome A7 est moins restrictif dans le fait qu’il n’exclut pas la colinéarité des points x, y, et z, ni n’exige que les points u et v soient distincts des points précédents. C’est d’ailleurs dans ces cas particuliers que peuvent être démontrées les autres axiomes d’ordre de Hilbert.
L’axiome A7 (axiome de Pasch intérieur) est plus restrictif dans la mesure où il ne couvre que le cas où la droite d coupe la droite xy en un point w tel que y est entre x et w. Dans le cas où x est entre w et y (axiome de Pasch extérieur), la démonstration emprunte les étapes suivantes[3] :
- Une droite D est dite entre deux points x et z n’appartenant pas à cette droite d s’il existe un point u qui soit sur la droite D et qui soit entre x et z.
- Lemme : si une droite D est entre deux points x et z, et r est un point de D, alors la droite D est entre x et tout point y distinct de r et appartenant à la demi-droite d’origine r et passant par z.
- L’axiome de Pasch « intérieur » et le lemme permettent de démontrer l’axiome de Pasch « extérieur ».
Dans le cas où la droite d ne coupe pas la droite xy, la démonstration nécessite l’axiome d’Euclide selon Hilbert, qui ne fait pas partie des axiomes de Tarski.
3. Axiome d’Euclide.
L’axiome A10 est différent de l’axiome d’Euclide selon Hilbert, qui affirme: Si xy est parallèle à la droite d passant par z, et si u est un point entre x et z, la droite yu coupe la droite d. (autrement dit il n’existe qu’une parallèle à d passant par y) La démonstration de l’axiome d’Euclide selon Hilbert emprunte les étapes suivantes[3] :
- Définition de deux points situés d’un même côté d’une droite : deux points a et b sont du même côté de la droite D s’il existe un point c tel que D soit entre a et c, et entre b et c.
- Si la droite D est entre les points a et b, alors a et b ne sont pas du même côté de la droite D.
- La relation binaire « être du même côté d’une droite » est réflexive, symétrique et transitive.
- Si la droite B est parallèle à la droite A, deux points quelconque de B sont d’un même côté de A.
- Si deux droites distinctes A et B passant par un point commun a étaient toutes les deux parallèles à une droite C, un point quelconque de A et un point quelconque de B seraient d’un même côté de C. Or l’axiome A10 permettrait d’associer à tout point de C un point x de A et un point y de B, tels que la droite C soit entre x et y, d’où contradiction
Résultats métamathématiques
L'axiomatisation est cohérente, complète et décidable (voir « Théorème de Tarski-Seidenberg (en) »)[4]. Cette axiomatique a été utilisée conjointement aux assistants de preuve Coq et HOL Light pour démontrer la validité des propositions du livre I des Éléments d'Euclide[4].
Notes et références
- ↑ Beeson 2016.
- ↑ a et b Beeson 2015.
- ↑ a b et c Schwabhäuser.
- ↑ a et b Yves Coudène, La géométrie élémentaire d'Euclide à aujourd'hui, Calvage & Mounet, coll. « Mathématiques en devenir », , 451 p. (ISBN 978-2-49-323001-0), IV. Axiomatiques, chap. 5 (« Axiomatique d'Alfred Tarski »)
Voir aussi
Bibliographie
- (en) Michael Beeson, A constructive version of Tarski's geometry, Annals of pure and applied logic, vol. 166, , chap. Issue 11, p. 1199-1273
- (en) Michael Beeson, A Constructive geometry and the parallel postulante, Bulletin of Symbolic logic, vol. 22, , chap. Issue 1
- (de) W. Schwabhäuser, Wanda Zwielew et Alfred Tarski, Metamathematishe Methoden in der Geometrie, Springer-Verlag 1983, Reprinted 2012 by ISHI Press.
Articles connexes
- Espace euclidien
- Eva Kallin
v · m | |
---|---|
Portail de la géométrie