Аксиоматика Тарского (геометрия)

Аксиоматика Тарского — система аксиом элементарной евклидовой геометрии, предложенная Альфредом Тарским. Замечательна тем, что формулируется в логике первого порядка с равенством и не требует теории множеств.

История

Альфред Тарский работал над своей аксиоматизацией с перерывами с 1926 до его смерти в 1983 году; первая публикация вышла в 1959 году. В частности, Тарский доказал, что его аксиоматика полна и непротиворечива; более того, существует алгоритм позволяющий выяснить, верно или неверно любое утверждение. (Эта теорема не противоречит теореме Гёделя о неполноте, поскольку в аксиоматике Тарского для геометрии нет средств выразить арифметику.)

Основные труды Тарского и его учеников в этом направлении изложены в монографии 1983 года. Аксиоматика, представленная в этой книге, состоит из 10 аксиом и одной схемы аксиом.

Аксиомы

Неопределяемые понятия

• Лежать между — тернарное отношение Bxyz, означающее, что у «лежит между» х и z. Другими словами, что y является точкой на отрезке хz. (При этом концы включаются, то есть, как будет следовать из аксиом, Bxxz — истинно).

• Конгруэнтность — тетрадное отношение wx ≡ yz, означающее, что отрезок wx конгруэнтен отрезку yz; другими словами, что длина wx равна длине yz.

Аксиомы

Аксиома Паша

Схема аксиом непрерывности

Верхняя оценка размерности.

Аксиома о пятом отрезке

• Рефлексивность конгруэнтности:

  $xy\equiv yx\,.$

• Тождественность конгруэнтности:

  $xy\equiv zz\rightarrow x=y.$

• Транзитивность конгруэнтности:

  $(xy\equiv zu\land xy\equiv vw)\rightarrow zu\equiv vw.$

• Тождественность отношения лежать между:

  $Bxyx\rightarrow x=y.$

То есть единственная точка на отрезке линии $xx$ — это сама точка $x$.

• Аксиома Паша:

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

Две диагонали выпуклого четырехугольника $xuvy$ должны пересекаться в некоторой точке.

• Схема аксиом непрерывности. Пусть $\phi (x)$ и $\psi (y)$ суть формулы первого порядка без свободных переменных a или b. Пусть также нет свободных переменных $x$ в $\psi (y)$ или $y$ в $\phi (x)$. Тогда все выражения следующего типа являются аксиомами:

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

То есть, если $\phi (x)$ и $\psi (y)$ описывают два множества точек луча с вершиной a, первое из которых левее второго, то найдётся точка b между этими множествами.

• Нижняя оценка размерности:

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

То есть существуют три неколлинеарные точки. Без этой аксиомы теории могут быть смоделированы с помощью одномерной вещественной прямой, одной точки или даже пустого множества.

• Верхняя оценка размерности:

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

То есть любые три точки, равноудаленные от двух различных точек, лежат на прямой. Без этой аксиомы теория может быть смоделирована в многомерном (в том числе трёхмерном) пространстве.

• Аксиома о пятом отрезке:

  ${(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'.$

То есть, если отрезки 4 отмеченных пар на двух чертежах справа равны, то и отрезки в пятой паре равны между собой.

• Построение отрезка:

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

То есть от любой точки в любом направлении можно отложить отрезок данной длины.

Ссылки

• Беклемишев Л. Д. Элементарная геометрия с точки зрения логики. лекции Летней школы «Современная математика», 20—23 июля 2014.