Аксиоматика Тарского

Аксиоматика Тарского — это один из вариантов аксиоматического построения евклидовой геометрии, предложенный польско-американским математиком и логиком Альфредом Тарским в середине XX века. В отличие от классической системы аксиом Евклида или более строгой системы Гильберта, аксиоматика Тарского является элементарной (то есть использует логику первого порядка, без кванторов по множествам) и полной (для неё существует алгоритм, позволяющий доказать или опровергнуть любое утверждение, сформулированное в её языке). Она основана на минимальном наборе исходных понятий и аксиом, что делает её удобной для метаматематических исследований и компьютерного доказательства теорем.

История создания

Альфред Тарский (1901—1983) внёс фундаментальный вклад в теорию моделей, алгебраическую логику и основания математики. В 1920-х — 1930-х годах он активно занимался проблемой разрешимости теорий. В 1930 году он опубликовал работу «О полноте элементарной геометрии», в которой показал, что элементарная геометрия (то есть геометрия, допускающая формулировки в логике первого порядка) является полной и разрешимой. Однако первая полная система аксиом, реализующая эту идею, была опубликована Тарским лишь в 1959 году в совместной работе с американским математиком Леонардом Гиллисом (Leonard Gillies) и в более развёрнутом виде в 1967 году в книге «What is Elementary Geometry?» (в соавторстве с Стивеном Гивентом). Система была разработана как инструмент для изучения метаматематических свойств геометрии, в частности, для доказательства её разрешимости.

Основные понятия

Аксиоматика Тарского использует минимальное количество исходных (неопределяемых) понятий. В классическом варианте это:

1. Точки — единственный тип объектов (в отличие от геометрии Гильберта, где есть точки, прямые и плоскости). Все геометрические объекты (прямые, отрезки, углы) определяются как множества точек.
2. Трёхместное отношение «между» (B(x, y, z)): точка y лежит между точками x и z на прямой (то есть x, y, z коллинеарны, и y находится на отрезке xz).
3. Четырёхместное отношение конгруэнтности (Cong(x, y, z, w) или xy ≡ zw): отрезок xy конгруэнтен (равен по длине) отрезку zw.

В некоторых вариантах аксиоматики также используется предикат «точка x является концом отрезка» или «точки x и y различны», но это часто выводится из других аксиом.

Система аксиом

Аксиоматика Тарского состоит из нескольких групп аксиом, формализованных в логике первого порядка. Всего их обычно 11 (в наиболее распространённой версии 1967 года). Ниже приведён их содержательный перечень.

Аксиомы конгруэнтности

1. Рефлексивность конгруэнтности: Отрезок xy конгруэнтен сам себе: xy ≡ yx.
2. Симметричность конгруэнтности: Если xy ≡ zw, то zw ≡ xy.
3. Транзитивность конгруэнтности: Если xy ≡ zw и zw ≡ uv, то xy ≡ uv.
4. Аксиома откладывания отрезка: Для любых точек a, b, c, d существует точка e такая, что между a и b лежит c? (уточнение: на луче от a через b можно отложить отрезок, равный данному). Формально: ∀a∀b∀c∀d∃e (B(a, b, e) ∧ be ≡ cd).

Аксиомы отношения «между»

1. Симметричность «между»: Если B(x, y, z), то B(z, y, x). (Порядок точек на прямой не важен.)
2. Аксиома Паша (внутренняя версия): Если B(a, b, c) и B(a, d, e), то существует точка f такая, что B(b, f, d) и B(c, f, e). (Эта аксиома гарантирует, что прямая, пересекающая одну сторону треугольника, пересечёт и другую.)
3. Аксиома единственности отрезка: Если B(x, y, z), то x ≠ y. (Точка не может лежать между собой и другой точкой.)
4. Аксиома непрерывности (схема аксиом): Для любых двух формул φ(x) и ψ(y) с одной свободной переменной, если существует точка a, для которой φ(a) истинно, и точка b, для которой ψ(b) истинно, и для всех x, y, если φ(x) и ψ(y) истинны, то B(x, y, z) (где z — некоторая точка), то существует точка c такая, что для всех x, y, если φ(x) и ψ(y) истинны, то B(x, c, y). (Это аналог аксиомы непрерывности Дедекинда, но выраженный в логике первого порядка.)

Аксиомы конгруэнтности и «между»

1. Аксиома пяти отрезков (аксиома подобия): Если два отрезка конгруэнтны, и их продолжения также конгруэнтны, то треугольники равны. Формально: если B(a, b, c), B(a', b', c'), ab ≡ a'b', bc ≡ b'c', ad ≡ a'd', bd ≡ b'd', то cd ≡ c'd'.
2. Аксиома построения треугольника: Для любых точек a, b, c, d, e, если ab ≡ a'b' и ac ≡ a'c' и bc ≡ b'c', то точки a, b, c определяют треугольник, конгруэнтный треугольнику a', b', c'.

Аксиома размерности

1. Аксиома размерности: Существует не более n+1 точек, попарно равноудалённых друг от друга. Для плоскости (n=2) это означает, что не существует четырёх точек, попарно равноудалённых (то есть нет правильного тетраэдра в плоскости). Для прямой (n=1) — не существует трёх попарно равноудалённых точек.

Свойства аксиоматики

• Элементарность: Все аксиомы сформулированы на языке логики первого порядка (кванторы только по точкам, не по множествам). Это позволяет применять к теории методы теории моделей.
• Полнота: Теория, заданная аксиоматикой Тарского, является полной. Это означает, что для любого утверждения, сформулированного в её языке, либо оно само, либо его отрицание может быть выведено из аксиом. Это свойство было доказано самим Тарским.
• Разрешимость: Существует алгоритм (процедура), который для любого утверждения элементарной геометрии за конечное число шагов определяет, истинно оно или ложно. Это следует из полноты и эффективной аксиоматизируемости теории. Алгоритм основан на методе элиминации кванторов (исключения кванторов) над полем вещественных чисел.
• Категоричность: В отличие от аксиоматики Гильберта, аксиоматика Тарского не является категоричной (то есть не задаёт модель единственным образом с точностью до изоморфизма). Она допускает существование нестандартных моделей (например, с бесконечно малыми или бесконечно большими отрезками), которые удовлетворяют всем аксиомам, но не изоморфны стандартной евклидовой плоскости.

Связь с другими теориями

• Геометрия Гильберта: Система Гильберта (1899) содержит 20 аксиом, включая аксиомы порядка, конгруэнтности, непрерывности и параллельности. Она использует три типа объектов (точки, прямые, плоскости) и является более привычной для преподавания, но не является элементарной (содержит аксиому непрерывности в виде аксиомы полноты, которая не выражается в логике первого порядка). Аксиоматика Тарского является более экономной и метаматематически удобной.
• Аналитическая геометрия: Аксиоматика Тарского эквивалентна теории вещественных замкнутых полей. Евклидова плоскость в ней моделируется как декартово произведение R × R, где R — вещественное замкнутое поле. Отношение «между» и конгруэнтность определяются через координаты.
• Теория моделей: Аксиоматика Тарского — классический пример полной и разрешимой теории, который используется для иллюстрации методов элиминации кванторов и теории моделей.

Критика и ограничения

• Сложность для преподавания: Из-за минимализма и абстрактности (например, использование только точек) аксиоматика Тарского крайне неудобна для начального обучения геометрии. Она не интуитивна и требует значительной математической подготовки.
• Отсутствие наглядности: В ней нет прямых линий как самостоятельных объектов, все построения ведутся через отношение «между». Это затрудняет визуализацию.
• Ограниченность элементарной геометрии: Аксиоматика Тарского описывает только элементарную геометрию, то есть утверждения, которые можно сформулировать без кванторов по множествам. Многие важные геометрические понятия (например, длина окружности, площадь круга, непрерывные функции) не входят в её язык, так как требуют анализа бесконечных множеств.

Значение

Аксиоматика Тарского сыграла ключевую роль в развитии метаматематики и теории алгоритмов. Она показала, что даже такая содержательная теория, как евклидова геометрия, может быть полностью формализована и алгоритмически разрешима. Это стало важным шагом на пути к созданию систем автоматического доказательства теорем и компьютерной алгебры. В частности, метод элиминации кванторов, разработанный для этой теории, лёг в основу алгоритмов, используемых в современных системах компьютерной математики (например, в Mathematica и Maple).

Источники

• Tarski, A. (1959). What is elementary geometry? In The Axiomatic Method (pp. 16–29). North-Holland.
• Tarski, A., & Givant, S. (1999). Tarski's System of Geometry. Bulletin of Symbolic Logic, 5(2), 175–214.
• Гильберт, Д. (1998). Основания геометрии. М.: Наука. (Приложение с аксиоматикой Тарского в современных изданиях).
• Schwabhäuser, W., Szmielew, W., & Tarski, A. (1983). Metamathematische Methoden in der Geometrie. Springer-Verlag.