Axiomes de Tarski

Modèle:Voir homonyme

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 : $B x y z$ (entre deux ou en anglais betweenness) ;
la distance de x à y est égale à la distance de z à u : $x y \equiv z u$ (congruence).

Axiomes

A1: Réflexivité de la congruence

$x y \equiv y x .$

A2: Transitivité de la congruence

$(x y \equiv z u \land x y \equiv v w) \to z u \equiv v w .$

A3: Segment nul

$x y \equiv z z \to x = y .$

A4: Report de segment

$\exists z [B x y z \land y z \equiv a b] .$

A5: Cinq segments

$(x \neq y \land B x y z \land B x^{'} y^{'} z^{'} \land x y \equiv x^{'} y^{'} \land y z \equiv y^{'} z^{'} \land x u \equiv x^{'} u^{'} \land y u \equiv y^{'} u^{'}) \to z u \equiv z^{'} u^{'} .$

A6: Identité

$B x y x \to x = y .$

A7: Axiome de Pasch

$(B x u z \land B y v z) \to \exists a (B u a y \land B v a x) .$

A8: Plus petite dimension

$\exists a \exists b \exists c [\neg B a b c \land \neg B b c a \land \neg B c a b] .$

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

$(x u \equiv x v \land y u \equiv y v \land z u \equiv z v \land u \neq v) \to (B x y z \lor B y z x \lor B z x y) .$

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

A10: Axiome d'Euclide

$(B x u v \land B y u z \land x \neq u) \to \exists a \exists b (B x y a \land B x z b \land B a v b) .$

Il existe d'autres formulations équivalentes au cinquième postulat d’Euclide. Par exempleModèle:Sfn :

$((B x y w \land x y \equiv y w) \land (B x u v \land x u \equiv u v) \land (B y u z \land y u \equiv z u)) \to y z \equiv v w .$
$B x y z \lor B y z x \lor B z x y \lor \exists a (x a \equiv y a \land x a \equiv z a) .$

A11: Schéma d'axiome de continuité

$\exists a \forall x \forall y [(ϕ (x) \land ψ (y)) \to B a x y] \to \exists b \forall x \forall y [(ϕ (x) \land ψ (y)) \to B x b y$

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 Modèle:Sfn:

$(B u v p \land u \neq v \land B a p b \land b \neq p) \to \exists y \exists z (a y \equiv a b \land a z \equiv a b \land B y p z \land B u p z) .$

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 suivantesModèle:Sfn :

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 laborieuxModèle:Sfn.
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 suivantesModèle:Sfn :

- 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 suivantesModèle:Sfn :

- 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 « Modèle:Lien »)^[1]. Cette axiomatique a été utilisée conjointement aux assistants de preuve Rocq et HOL Light pour démontrer la validité des propositions du livre I des Éléments d'Euclide^[1].

Notes et références

Modèle:Références

Voir aussi

Bibliographie

Articles connexes

Modèle:Palette Modèle:Portail

↑ ^1,0 et ^1,1 Modèle:Ouvrage

[coudene-1] 1,0 et ^1,1 Modèle:Ouvrage

[1]

Axiomes de Tarski

Sommaire

Axiomes

Commentaires

Résultats métamathématiques

Notes et références

Voir aussi

Bibliographie

Articles connexes

Menu de navigation

Axiomes de Tarski

Axiomes

Commentaires

Résultats métamathématiques

Notes et références

Voir aussi

Bibliographie

Articles connexes

Menu de navigation

Rechercher