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

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

История

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

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

Аксиомы

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

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

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

Аксиомы

Аксиома Паша

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

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

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

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

  $xy\equiv yx.$

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

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

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

  $(xy\equiv zu\wedge xy\equiv vw)\to zu\equiv vw.$

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

  $Bxyx\to x=y.$

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

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

  $(Bxuz\wedge Byvz)\to \mathrm{\exists }a(Buay\wedge Bvax).$

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

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

  $\mathrm{\exists }a\mathrm{\forall }x\mathrm{\forall }y[(\varphi (x)\wedge \psi (y))\to Baxy]\to \mathrm{\exists }b\mathrm{\forall }x\mathrm{\forall }y[(\varphi (x)\wedge \psi (y))\to Bxby].$

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

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

  $\mathrm{\exists }a\mathrm{\exists }b\mathrm{\exists }c[\mathrm{\neg }Babc\wedge \mathrm{\neg }Bbca\wedge \mathrm{\neg }Bcab].$

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

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

  $(xu\equiv xv\wedge yu\equiv yv\wedge zu\equiv zv\wedge u\ne v)\to (Bxyz\vee Byzx\vee Bzxy).$

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

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

  $(x\ne y\wedge Bxyz\wedge B{x}^{\prime }{y}^{\prime }{z}^{\prime }\wedge xy\equiv x^{\prime }{y}^{\prime }\wedge yz\equiv y^{\prime }{z}^{\prime }\wedge xu\equiv x^{\prime }{u}^{\prime }\wedge yu\equiv y^{\prime }{u}^{\prime })\to zu\equiv z^{\prime }{u}^{\prime }.$

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

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

  $\mathrm{\exists }z[Bxyz\wedge yz\equiv ab].$

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

Ссылки

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