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

Эта статья об аксиомах евклидовой геометрии. Чтобы узнать об аксиомах Тарского для действительных чисел , см. Аксиоматизацию действительных чисел Тарского . Аксиомы Тарского для теории множеств см. в теории множеств Тарского – Гротендика .

Аксиомы Тарского представляют собой систему аксиом для евклидовой геометрии , особенно для той части евклидовой геометрии, которая формулируется в логике первого порядка с тождеством (т.е. формулируется как элементарная теория ). Как таковая, она не требует базовой теории множеств . Единственными примитивными объектами системы являются «точки», а единственными примитивными предикатами являются «между» (выражающий тот факт, что точка лежит на отрезке между двумя другими точками) и «конгруэнтность» (выражающий тот факт, что расстояние между двумя точек равно расстоянию между двумя другими точками). Система содержит бесконечное множество аксиом.

Система аксиом принадлежит Альфреду Тарскому , который впервые представил ее в 1926 году. Другими современными аксиомами евклидовой геометрии являются аксиомы Гильберта (1899 г.) и аксиомы Биркгофа (1932 г.).

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

Обзор

В начале своей карьеры Тарский преподавал геометрию и исследовал теорию множеств. Его коллега Стивен Гивант (1999) объяснил точку отсчета Тарского:

От Энрикеса Тарский узнал о работах Марио Пьери , итальянского геометра, находившегося под сильным влиянием Пеано. Тарский предпочитал систему Пьери [из его мемуаров «Точка и сфера» ], где логическая структура и сложность аксиом были более прозрачными.

Затем Живант говорит, что Тарский разработал свою систему «с типичной тщательностью»:

Чем отличался подход Тарского к геометрии? Прежде всего, система аксиом была гораздо проще любой из существовавших до того времени систем аксиом. Фактически длина всех аксиом Тарского вместе взятых не намного больше, чем длина одной из 24 аксиом Пьери. Это была первая система евклидовой геометрии, которая была достаточно простой, чтобы все аксиомы могли быть выражены только в терминах примитивных понятий , без помощи определенных понятий. Еще более важно то, что впервые было проведено четкое различие между полной геометрией и ее элементарной, то есть ее первого порядка, частью.

Как и другие современные аксиоматизации евклидовой геометрии, Тарский использует формальную систему, состоящую из строк символов, называемых предложениями , конструкция которых учитывает формальные синтаксические правила и правила доказательства, которые определяют разрешенные манипуляции с предложениями. В отличие от некоторых других современных аксиоматизаций, таких как аксиоматизация Биркгофа и Гильберта , аксиоматизация Тарского не имеет примитивных объектов, кроме точек , поэтому переменная или константа не может относиться к линии или углу. Поскольку точки — единственные примитивные объекты, а система Тарского — это теория первого порядка , невозможно даже определить линии как наборы точек. Единственными примитивными отношениями ( предикатами ) являются «между» и «конгруэнтность» между точками.

Аксиоматизация Тарского короче, чем у ее конкурентов, в этом смысле Тарский и Гивант (1999) ясно это подчеркивают. Оно более краткое, чем у Пьери, потому что Пьери имел только два примитивных понятия, а Тарский ввел три: точка, промежуточность и конгруэнтность. Такая экономия примитивных и определенных понятий означает, что система Тарского не очень удобна для занятий евклидовой геометрией. Скорее, Тарский разработал свою систему для облегчения ее анализа с помощью инструментов математической логики , то есть для облегчения вывода ее метаматематических свойств. Система Тарского обладает тем необычным свойством, что все предложения могут быть записаны в универсально-экзистенциальной форме, что является частным случаем пренексной нормальной формы . В этой форме все кванторы универсальности предшествуют любым кванторам существования , так что все предложения можно преобразовать в форму $\forall u\forall v\ldots \exists a\exists b\dots .$ Этот факт позволил Тарскому доказать, что евклидова геометрия разрешима : существует алгоритм , который может определить истинность или ложность любого предложения. Аксиоматизация Тарского также завершена . Это не противоречит первой теореме Гёделя о неполноте , поскольку теории Тарского не хватает выразительной силы, необходимой для интерпретации арифметики Робинсона ( Францен 2005 , стр. 25–26).

Аксиомы

Альфред Тарский работал над аксиоматизацией и метаматематикой евклидовой геометрии с перерывами с 1926 года до своей смерти в 1983 году, причем Тарский (1959) возвестил о его зрелом интересе к этому предмету. Кульминацией работы Тарского и его учеников по евклидовой геометрии стала монография Швабхойзер, Шмелев и Тарский (1983), в которой изложены 10 аксиом и одна схема аксиом, показанная ниже, связанная с ними метаматематика и значительная часть предмета. Гупта (1965) внес важный вклад, а Тарский и Гивант (1999) обсуждают историю.

Фундаментальные отношения

Эти аксиомы представляют собой более элегантную версию набора, который Тарский разработал в 1920-х годах в рамках своего исследования метаматематических свойств евклидовой геометрии плоскости . Эта цель потребовала переформулировать эту геометрию как теорию первого порядка . постулировав вселенную точек Тарский сделал это , , где строчные буквы обозначали переменные, расположенные в этой вселенной. Равенство обеспечивается базовой логикой (см. Логика первого порядка#Равенство и ее аксиомы ). Затем Тарский сформулировал два примитивных соотношения:

• Посредничество , тройственное отношение . Атомарное предложение Bxyz означает, что точка y находится «между» точками x и z , другими словами, что y является точкой на отрезке xz . (Это соотношение интерпретируется включительно, так что Bxyz тривиально истинно всякий раз, когда x=y или y=z ).
• Конгруэнтность (или «эквидистантность») — тетрадное отношение . Атоматическое предложение Cwxyz или обычно wx ≡ yz можно интерпретировать как , yz конгруэнтное , yz другими словами, что длина отрезка wx равна длине отрезка wx .

Посредственность отражает аффинный аспект (такой как параллельность линий) евклидовой геометрии; конгруэнтность, ее метрический аспект (например, углы и расстояния). Фоновая логика включает в себя тождество , бинарное отношение , обозначаемое =.

Приведенные ниже аксиомы сгруппированы по типам отношений, которые они вызывают, а затем отсортированы сначала по количеству кванторов существования, а затем по количеству атомарных предложений. Аксиомы следует понимать как универсальные замыкания ; следовательно, любые свободные переменные должны рассматриваться как неявно универсальные количественные значения .

Аксиомы сравнения

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

$xy\equiv yx\,.$

Тождество соответствия

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

Транзитивность сравнения

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

Комментарий

В то время как отношение конгруэнтности $xy\equiv zw$ формально является четырехсторонним отношением между точками, неформально его также можно рассматривать как бинарное отношение между двумя отрезками прямой. $xy$ и $zw$. Приведенные выше аксиомы «Рефлексивности» и «Транзитивности» в совокупности доказывают оба:

• что это бинарное отношение на самом деле является отношением эквивалентности
  • это рефлексивно: $xy\equiv xy$.
  • это симметрично $xy\equiv zw\rightarrow zw\equiv xy$.
  • это транзитивно $(xy\equiv zu\land zu\equiv vw)\rightarrow xy\equiv vw$.
• и что порядок указания точек отрезка прямой не имеет значения.
  • $xy\equiv zw\rightarrow xy\equiv wz$.
  • $xy\equiv zw\rightarrow yx\equiv zw$.
  • $xy\equiv zw\rightarrow yx\equiv wz$.

Аксиома «транзитивности» утверждает, что конгруэнтность является евклидовой , поскольку она соответствует первому из » Евклида « общих понятий .

Аксиома «идентичности конгруэнтности» интуитивно утверждает, что если xy конгруэнтен отрезку, который начинается и заканчивается в одной и той же точке, x и y являются одной и той же точкой. Это тесно связано с понятием рефлексивности бинарных отношений .

Аксиомы посредничества

аксиома Паша

Тождество Промежутка

$Bxyx\rightarrow x=y.$

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

Аксиома Паша

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

Непрерывность: φ и ψ делят луч на две половины, и аксиома утверждает существование точки b, разделяющей эти две половины.

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

Пусть φ( x ) и ψ( y ) — формулы первого порядка, содержащие свободных экземпляров a b или не . Пусть также не существует свободных экземпляров x в ψ( y ) или y в φ( 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].$

Пусть r — луч с конечной точкой a . Пусть формулы первого порядка φ и ψ определяют подмножества X и Y из r такие, что каждая точка в Y находится справа от каждой точки X (относительно a ). Тогда существует точка b в r, между X и Y. лежащая По сути, это конструкция разреза Дедекинда , выполненная таким образом, чтобы избежать количественной оценки множеств.

Обратите внимание, что формулы φ( x ) и ψ( y ) могут содержать параметры, т.е. свободные переменные, отличные от a , b , x, y . И действительно, каждый экземпляр схемы аксиом, не содержащий параметров, может быть доказан на основе других аксиом.

Нижнее измерение

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

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

Аксиома Евклида

Можно дать три варианта этой аксиомы, обозначенные ниже A, B и C. Они эквивалентны друг другу с учетом остальных аксиом Тарского и действительно эквивалентны постулату параллельности Евклида .

А : $((Bxyw\land xy\equiv yw)\land (Bxuv\land xu\equiv uv)\land (Byuz\land yu\equiv uz))\rightarrow yz\equiv vw.$

Пусть отрезок соединяет середины двух сторон данного треугольника . Этот отрезок будет вдвое короче третьей стороны. Это эквивалентно сумме внутренних углов любого треугольника в два прямых угла .

Б : $Bxyz\lor Byzx\lor Bzxy\lor \exists a\,(xa\equiv ya\land xa\equiv za).$

Для любого треугольника существует круг , включающий все его вершины.

Аксиома Евклида: C

С : $(Bxuv\land Byuz\land x\neq u)\rightarrow \exists a\,\exists b\,(Bxya\land Bxzb\land Bavb).$

Для любого угла и любой точки v внутри него существует отрезок прямой, включающий v , с конечной точкой на каждой стороне угла.

Каждый вариант имеет преимущество перед остальными:

• А обходится без экзистенциальных кванторов ;
• B имеет наименьшее количество переменных и атомарных предложений ;
• C требует лишь одного примитивного понятия — посредственности. Этот вариант является обычным в литературе.

Пять сегментов

Пять сегментов

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

Начните с двух треугольников : xuz и x'u'z'. Нарисуйте отрезки yu и y'u', соединяя вершину каждого треугольника с точкой на стороне, противоположной вершине. В результате получаются два разделенных треугольника, каждый из которых состоит из пяти сегментов. Если каждая из четырёх отрезков одного треугольника конгруэнтна отрезку другого треугольника, то пятые отрезки в обоих треугольниках должны быть равны.

Это эквивалентно правилу стороны-угла-стороны для определения равенства двух треугольников; если углы uxz и u'x'z' равны (существуют равные треугольники xuz и x'u'z' ), а две пары инцидентных сторон конгруэнтны ( xu ≡ x'u' и xz ≡ x'z ' ), то оставшаяся пара сторон также конгруэнтна ( uz ≡ u'z' ).

Сегмент Строительство

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

Для любой точки y можно провести в любом направлении (определяемом x ) линию, соответствующую любому отрезку ab .

Обсуждение

По мнению Тарского и Гиванта (1999: 192–93), ни одна из вышеперечисленных аксиом не является принципиально новой. Первые четыре аксиомы устанавливают некоторые элементарные свойства двух примитивных отношений. Например, рефлексивность и транзитивность конгруэнции устанавливают, что конгруэнтность является отношением эквивалентности над отрезками прямой. Тождество конгруэнтности и взаимосвязи регулирует тривиальный случай, когда эти отношения применяются к неразличимым точкам. Теорема xy ≡ zz ↔ x = y ↔ Bxyx расширяет эти аксиомы тождества.

Ряд других свойств посредственности можно вывести в виде теорем. включая:

• Рефлексивность : Bxxy ;
• Симметрия : Bxyz → Bzyx ;
• Транзитивность : ( Bxyw ∧ Byzw ) → Bxyz ;
• Связность : ( Bxyw ∧ Bxzw ) → ( Bxyz ∨ Bxzy ).

Последние два свойства полностью упорядочивают точки, составляющие отрезок прямой.

Аксиомы верхнего и нижнего измерения вместе требуют, чтобы любая модель этих аксиом имела размерность 2, т. е. чтобы мы аксиоматизировали евклидову плоскость. Соответствующие изменения в этих аксиомах дают наборы аксиом для евклидовой геометрии для размерностей 0, 1 и больше 2 (Тарский и Гивант 1999: Аксиомы 8 ⁽¹⁾ , 8 ^(н) , 9 ⁽⁰⁾ , 9 ⁽¹⁾ , 9 ^(н) ). Обратите внимание, что твердотельная геометрия не требует новых аксиом, в отличие от случая с аксиомами Гильберта . Более того, Нижнее Измерение для n измерений — это просто отрицание Верхнего Измерения для n — 1 измерений.

Когда количество измерений больше 1, посредственность можно определить с точки зрения конгруэнтности (Тарски и Гивант, 1999). Сначала определим отношение «≤» (где $ab\leq cd$ интерпретируется как «длина отрезка $ab$ меньше или равно длине отрезка $cd$"):

$xy\leq zu\leftrightarrow \forall v(zv\equiv uv\rightarrow \exists w(xw\equiv yw\land yw\equiv uv)).$

В случае двух измерений интуиция такова: для любого отрезка xy рассмотрим возможный диапазон длин xv , где v — любая точка на серединном перпендикуляре xy . Очевидно, что хотя верхней границы длины xv не существует , существует нижняя граница, которая возникает, когда v является средней точкой xy . Таким образом, если xy короче или равен zu , то диапазон возможных длин xv будет расширенным набором диапазона возможных длин zw , где w — любая точка на серединном перпендикуляре zu .

Затем взаимосвязь можно определить, интуитивно понимая, что кратчайшее расстояние между любыми двумя точками — это прямая линия:

$Bxyz\leftrightarrow \forall u((ux\leq xy\land uz\leq zy)\rightarrow u=y).$

Схема аксиом непрерывности гарантирует, что порядок точек на линии является полным (относительно определяемых свойств первого порядка). Как было указано Тарским, эта схема аксиом первого порядка может быть заменена более мощной аксиомой непрерывности второго порядка , если позволить переменным ссылаться на произвольные наборы точек. Полученная система второго порядка эквивалентна набору аксиом Гильберта. (Тарский и Гивант, 1999 г.)

Аксиомы Паша и Евклида хорошо известны. делает Аксиома построения сегмента возможным измерение и декартову систему координат — просто присвойте длину 1 некоторому произвольному непустому отрезку прямой. Действительно, в (Schwabhäuser 1983) показано, что, указав две выделенные точки на линии, называемые 0 и 1, мы можем определить сложение, умножение и упорядочение, превращая набор точек на этой линии в действительно замкнутое упорядоченное поле. . Затем мы можем ввести координаты из этого поля, показав, что каждая модель аксиом Тарского изоморфна двумерной плоскости над некоторым вещественно-замкнутым упорядоченным полем.

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

Пусть wff обозначает корректную формулу (или синтаксически правильную формулу первого порядка) в системе Тарского. Тарский и Гивант (1999: 175) доказали, что система Тарского:

• Последовательный : не существует такого wff, чтобы и его, и его отрицание можно было доказать с помощью аксиом;
• Полное : каждое wff или его отрицание является теоремой, доказуемой на основе аксиом;
• Разрешимость : существует алгоритм , который решает для каждого случая, является ли он доказуемым или опровергнутым с точки зрения аксиом. Это следует из Тарского:
  • Процедура решения реального замкнутого поля , которое он нашел методом исключения кванторов ( теорема Тарского–Зейденберга );
  • Аксиомы, допускающие упомянутое выше представление в виде двумерной плоскости над вещественным замкнутым полем .

Это приводит к тому, что каждое утверждение евклидовой геометрии (второго, общего порядка), которое может быть сформулировано как предложение первого порядка в системе Тарского, истинно тогда и только тогда, когда оно доказуемо в системе Тарского, и эта доказуемость может быть автоматически проверена. с алгоритмом Тарского. , например, применимо ко всем теоремам из книги I «Начал» Евклида. Примером теоремы евклидовой геометрии, которую нельзя сформулировать таким образом, является архимедово свойство отрезков S1 _{: для любых двух} и S2 _Это положительной длины существует натуральное число n такое, что nS ₁ длиннее S ₂ . (Это следствие того, что существуют вещественно-замкнутые поля, содержащие бесконечно малые числа. ) Другими понятиями, которые не могут быть выражены в системе Тарского, являются возможность построения с помощью линейки и циркуля , а также утверждения, в которых говорится о «всех многоугольниках» и т. д.

Гупта (1965) доказал независимость аксиом Тарского, за исключением Паша и рефлексивности сравнения .

Отрицание аксиомы Евклида дает гиперболическую геометрию , а полное ее устранение дает абсолютную геометрию . Полная (в отличие от элементарной) евклидова геометрия требует отказа от аксиоматизации первого порядка: замените φ( x ) и ψ( y ) в схеме аксиом Непрерывности на x ∈ A и y ∈ B , где A и B — универсально кванторные переменные. ранжирование по наборам точек.

Сравнение с системой Гильберта

Аксиомы Гильберта для геометрии плоскости номер 16, включая транзитивность конгруэнтности и вариант аксиомы Паша. Единственное понятие интуитивной геометрии, упоминаемое в примечаниях к аксиомам Тарского, — это треугольник . (Версии B и C аксиомы Евклида относятся к «кругу» и «углу» соответственно.) Аксиомы Гильберта также требуют «луча», «угла» и понятия треугольника, «включающего» угол. В дополнение к посредничеству и конгруэнтности аксиомы Гильберта требуют примитивного бинарного отношения «on», связывающего точку и линию.

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

Таким образом, система Гильберта значительно сильнее: каждая модель изоморфна реальной плоскости. $\mathbb {R} ^{2}$ (используя стандартные понятия точек и линий). Напротив, система Тарского имеет много неизоморфных моделей: для каждого вещественно-замкнутого поля F плоскость F ² предоставляет одну из таких моделей (где взаимосвязь и конгруэнтность определяются очевидным образом).

Первые четыре группы аксиом аксиом Гильберта для плоской геометрии биинтерпретируемы с аксиомами Тарского минус непрерывность.

См. также

• Евклидова геометрия
• Евклидово пространство

Ссылки

• Франзен, Торкель (2005), Теорема Гёделя: неполное руководство по ее использованию и злоупотреблениям , AK Peters, ISBN  1-56881-238-8
• Живант, Стивен (1 декабря 1999 г.). «Объединение нитей в творчестве Альфреда Тарского» . Математический интеллект . 21 (1): 47–58. дои : 10.1007/BF03024832 . ISSN   1866-7414 . S2CID   119716413 .
• Гринберг, Марвин Джей (2010). «Старые и новые результаты в основах элементарных плоских евклидовых и неевклидовых геометрий» (PDF) . Американский математический ежемесячник . 117 (3): 198. дои : 10.4169/000298910x480063 .
• Гупта, Х.Н. (1965). Вклад в аксиоматические основы геометрии (докторская диссертация). Калифорнийский университет в Беркли.
• Тарский, Альфред (1959), «Что такое элементарная геометрия?», В книге Леона Хенкина, Патрика Суппеса и Альфреда Тарского (ред.), Аксиоматический метод. Особое внимание уделяется геометрии и физике. Материалы международного симпозиума, состоявшегося в Университете. Калифорнии, Беркли, 26 декабря 1957 г. — январь. 4, 1958 , Исследования по логике и основам математики, Амстердам: Северная Голландия, стр. 16–29, MR   0106185 .
  • Доступно в виде переиздания 2007 года , Brouwer Press, ISBN   1-4437-2812-8
• Тарский, Альфред ; Гивант, Стивен (1999), «Система геометрии Тарского» , Бюллетень символической логики , 5 (2): 175–214, CiteSeerX   10.1.1.27.9012 , doi : 10.2307/421089 , ISSN   1079-8986 , JSTOR   421089 , МР   1791303 , S2CID   18551419
• Швабхойзер, В.; Шмелев, В. ; Тарский, Альфред (1983). Метаматематические методы в геометрии . Спрингер-Верлаг.
• Щерба, Л.В. (1986). «Тарский и геометрия» (PDF) . Журнал символической логики . 51 (4): 907–12. дои : 10.2307/2273904 . JSTOR   2273904 . S2CID   35275962 .