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

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

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

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

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

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

Аксиомы

Аксиома Паша

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

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

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

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

  ${\displaystyle xy\equiv yx\,.}$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1. Tarski, Alfred (1959), What is elementary geometry?, in Leon Henkin, Patrick Suppes and Alfred Tarski, The axiomatic method. With special reference to geometry and physics. Proceedings of an International Symposium held at the Univ. of Calif., Berkeley, Dec. 26, 1957-Jan. 4, 1958, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, с. 16–29.
2. Schwabhäuser, W., Szmielew, W., Alfred Tarski, 1983. Metamathematische Methoden in der Geometrie. Springer-Verlag.

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