Axiomes de Tarski

A1: Réflexivité de la congruence

${\displaystyle xy\equiv yx.}$

A2: Transitivité de la congruence

${\displaystyle (xy\equiv zu\land xy\equiv vw)\rightarrow zu\equiv vw.}$

A3: Segment nul

${\displaystyle xy\equiv zz\rightarrow x=y.}$

A4: Report de segment

${\displaystyle \exists z\,[Bxyz\land yz\equiv ab].}$

A5: Cinq segments

${\displaystyle {(x\neq y\land Bxyz\land Bx'y'z'\land xy\equiv x'y'\land yz\equiv y'z'\land xu\equiv x'u'\land yu\equiv y'u')}\rightarrow zu\equiv z'u'.}$

Axiome de Pasch.

A6: Identité

${\displaystyle Bxyx\rightarrow x=y.}$

A7: Axiome de Pasch

${\displaystyle (Bxuz\land Byvz)\rightarrow \exists a\,(Buay\land Bvax).}$

A8: Plus petite dimension

${\displaystyle \exists a\,\exists b\,\exists c\,[\neg Babc\land \neg Bbca\land \neg Bcab].}$

Il existe trois points non colinéaires, il n'existe donc pas de modèle de la théorie de dimension < 2.

Plus grande dimension : trois points équidistants à u et v forment une droite.

A9: Plus grande dimension

${\displaystyle (xu\equiv xv\land yu\equiv yv\land zu\equiv zv\land u\neq v)\rightarrow (Bxyz\lor Byzx\lor Bzxy).}$

Il n'existe pas de modèle de dimension > 2.

A10: Axiome d'Euclide

• ${\displaystyle (Bxuv\land Byuz\land x\neq u)\rightarrow \exists a\,\exists b\,(Bxya\land Bxzb\land Bavb).}$

Il existe d'autres formulations équivalentes au cinquième postulat d’Euclide. Par exemple[1] :

• ${\displaystyle ((Bxyw\land xy\equiv yw)\land (Bxuv\land xu\equiv uv)\land (Byuz\land yu\equiv zu))\rightarrow yz\equiv vw.}$
• ${\displaystyle Bxyz\lor Byzx\lor Bzxy\lor \exists a\,(xa\equiv ya\land xa\equiv za).}$

Continuité : si φ et ψ divisent la demi-droite en deux parties alors il existe un point b séparant ces deux parties.

A11: Schéma d'axiome de continuité

${\displaystyle \exists a\,\forall x\,\forall y\,[(\phi (x)\land \psi (y))\rightarrow Baxy]\rightarrow \exists b\,\forall x\,\forall y\,[(\phi (x)\land \psi (y))\rightarrow Bxby}$

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]:

${\displaystyle (Buvp\land u\neq v\land Bapb\land b\neq p)\rightarrow \exists y\,\exists z\,(ay\equiv ab\land az\equiv ab\land Bypz\land Bupz).}$

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

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].