Русская Википедия:Аксиоматика Тарского (геометрия)
Аксиоматика Тарского — система аксиом элементарной евклидовой геометрии, предложенная Альфредом Тарским. Замечательна тем, что формулируется в логике первого порядка с равенством и не требует теории множеств.
История
Альфред Тарский работал над своей аксиоматизацией с перерывами с 1926 до его смерти в 1983 году; первая публикация вышла в 1959 году[1]. В частности, Тарский доказал, что его аксиоматика полна и непротиворечива; более того, существует алгоритм позволяющий выяснить, верно или неверно любое утверждение. (Эта теорема не противоречит теореме Гёделя о неполноте, поскольку в аксиоматике Тарского для геометрии нет средств выразить арифметику.)
Основные труды Тарского и его учеников в этом направлении изложены в монографии 1983 года[2]. Аксиоматика, представленная в этой книге, состоит из 10 аксиом и одной схемы аксиом.
Аксиомы
- Неопределяемые понятия
- Лежать между — тернарное отношение Bxyz, означающее, что у «лежит между» х и z. Другими словами, что y является точкой на отрезке хz. (При этом концы включаются, то есть, как будет следовать из аксиом, Bxxz — истинно).
- Конгруэнтность — тетрадное отношение wx ≡ yz, означающее, что отрезок wx конгруэнтен отрезку yz; другими словами, что длина wx равна длине yz.
- Аксиомы
- Рефлексивность конгруэнтности:
- <math>xy \equiv yx\,.</math>
- Тождественность конгруэнтности:
- <math>xy \equiv zz \rightarrow x=y.</math>
- Транзитивность конгруэнтности:
- <math>(xy \equiv zu \land xy \equiv vw) \rightarrow zu \equiv vw.</math>
- Тождественность отношения лежать между:
- <math>Bxyx \rightarrow x=y.</math>
- То есть единственная точка на отрезке линии <math>xx</math> — это сама точка <math>x</math>.
- Аксиома Паша:
- <math>(Bxuz \land Byvz) \rightarrow \exists a\, (Buay \land Bvax).</math>
- Две диагонали выпуклого четырехугольника <math>xuvy</math> должны пересекаться в некоторой точке.
- Схема аксиом непрерывности. Пусть <math>\phi(x)</math> и <math>\psi(y)</math> суть формулы первого порядка без свободных переменных a или b. Пусть также нет свободных переменных <math>x</math> в <math>\psi(y)</math> или <math>y</math> в <math>\phi(x)</math>. Тогда все выражения следующего типа являются аксиомами:
- <math>\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].</math>
- То есть, если <math>\phi(x)</math> и <math>\psi(y)</math> описывают два множества точек луча с вершиной a, первое из которых левее второго, то найдётся точка b между этими множествами.
- Нижняя оценка размерности:
- <math>\exists a \, \exists b\, \exists c\, [\neg Babc \land \neg Bbca \land \neg Bcab].</math>
- То есть существуют три неколлинеарные точки. Без этой аксиомы теории могут быть смоделированы с помощью одномерной вещественной прямой, одной точки или даже пустого множества.
- Верхняя оценка размерности:
- <math>(xu \equiv xv \land yu \equiv yv \land zu \equiv zv \land u \ne v) \rightarrow (Bxyz \lor Byzx \lor Bzxy).</math>
- То есть любые три точки, равноудаленные от двух различных точек, лежат на прямой. Без этой аксиомы теория может быть смоделирована в многомерном (в том числе трёхмерном) пространстве.
- Аксиома о пятом отрезке:
- <math>{(x \ne 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'.</math>
- То есть, если отрезки 4 отмеченных пар на двух чертежах справа равны, то и отрезки в пятой паре равны между собой.
- Построение отрезка:
- <math> \exists z\, [Bxyz \land yz \equiv ab].</math>
- То есть от любой точки в любом направлении можно отложить отрезок данной длины.
Примечания
- ↑ Шаблон:Citation.
- ↑ Schwabhäuser, W., Szmielew, W., Alfred Tarski, 1983. Metamathematische Methoden in der Geometrie. Springer-Verlag.
Ссылки
- Беклемишев Л. Д. Элементарная геометрия с точки зрения логики. лекции Летней школы «Современная математика», 20—23 июля 2014.
