Введение
Набор аксиом, используемый в логике первого порядка. Аксиомы Тарского — это система аксиом для евклидовой геометрии, в частности для той части евклидовой геометрии, которая может быть сформулирована в логике первого порядка с тождеством (то есть формулируется как элементарная теория). Следовательно, она не требует лежащей в основе теории множеств. Единственными примитивными объектами системы являются «точки», а единственными примитивными предикатами — «между» (выражающее тот факт, что точка лежит на отрезке прямой между двумя другими точками) и «конгруэнтность» (выражающее тот факт, что расстояние между двумя точками равно расстоянию между двумя другими точками). Система содержит бесконечно много аксиом. Эта система аксиом принадлежит Альфреду Тарскому, который впервые представил её в 1926 году. Другими современными аксиоматизациями евклидовой геометрии являются аксиомы Гильберта (1899) и аксиомы Бирхоффа (1932). Используя свою систему аксиом, Тарски показал, что теория первого порядка евклидовой геометрии является непротиворечивой, полной и разрешимой: каждое утверждение в её языке либо доказуемо, либо опровержимо на основе аксиом, и существует алгоритм, определяющий для любого заданного утверждения, является ли оно доказуемым или нет.
Tarski's axioms are an axiom system for Euclidean geometry, specifically for that portion of Euclidean geometry that is formulable in first order logic with identity (i. e. is formulable as an elementary theory). As such, it does not require an underlying set theory. The only primitive objects of the system are "points" and the only primitive predicates are "betweenness" (expressing the fact that a point lies on a line segment between two other points) and "congruence" (expressing the fact that the distance between two points equals the distance between two other points). The system contains infinitely many axioms. The axiom system is due to Alfred Tarski who first presented it in 1926. Other modern axiomizations of Euclidean geometry are Hilbert's axioms (1899) and Birkhoff's axioms (1932). Using his axiom system, Tarski was able to show that the first order theory of Euclidean geometry is consistent, complete and decidable: every sentence in its language is either provable or disprovable from the axioms, and we have an algorithm which decides for any given sentence whether it is provable or not.
Аксиомы
Альфред Тарски с перерывами работал над аксиоматизацией и метаматематикой евклидовой геометрии с 1926 года до своей смерти в 1983 году, а работа Тарски (1959) ознаменовала его углубленный интерес к этой области. Исследования Тарски и его учеников в области евклидовой геометрии завершились монографией Швабхаузера, Смилева и Тарски (1983), в которой представлены 10 аксиом и одна схема аксиом, приведенные ниже, соответствующая метаматематика и значительная часть материала по этой теме. Гупта (1965) внес важный вклад, а Тарски и Гивант (1999) рассматривают историю вопроса.
Основные отношения
Эти аксиомы представляют собой более элегантную версию набора, разработанного Тарским в 1920-х годах в рамках его исследования метаматематических свойств евклидовой планиметрии. Для достижения этой цели требовалось переформулировать эту геометрию как теорию первого порядка. Тарски сделал это, постулировав вселенную точек, где строчные буквы обозначают переменные, изменяющиеся в пределах этой вселенной. Равенство обеспечивается базовой логикой (см. Логика первого порядка#Равенство и его аксиомы). Затем Тарски постулировал два примитивных отношения: отношение между, триадическое отношение. Атомное высказывание Bxyz означает, что точка y находится "между" точками x и z, иными словами, что y лежит на отрезке xz. (Это отношение интерпретируется включительно, так что Bxyz тривиально истинно, когда x=y или y=z). Совместимость (или "равноудаленность"), тетрадическое отношение. Атомное высказывание Cwxyz или, чаще, wx ≡ yz может быть интерпретировано как то, что отрезок wx совместим с отрезком yz, другими словами, длина отрезка wx равна длине отрезка yz. Отношение между отражает аффинные свойства (например, параллельность прямых) евклидовой геометрии, а совместимость – ее метрические свойства (например, углы и расстояния). Базовая логика включает тождество, бинарное отношение, обозначаемое знаком =. Приведенные ниже аксиомы сгруппированы по типам отношений, которые они используют, а затем отсортированы сначала по количеству экзистенциальных кванторов, а затем по количеству атомарных высказываний. Аксиомы следует понимать как универсальные квантификации; следовательно, любые свободные переменные следует считать неявно универсально квантифицированными.
Betweenness, a triadic relation. The atomic sentence Bxyz denotes that the point y is "between" the points x and z, in other words, that y is a point on the line segment xz. (This relation is interpreted inclusively, so that Bxyz is trivially true whenever x=y or y=z). Congruence (or "equidistance"), a tetradic relation. The atomic sentence Cwxyz or commonly wx ≡ yz can be interpreted as wx is congruent to yz, in other words, that the length of the line segment wx is equal to the length of the line segment yz. Betweenness captures the affine aspect (such as the parallelism of lines) of Euclidean geometry; congruence, its metric aspect (such as angles and distances). The background logic includes identity, a binary relation denoted by =. The axioms below are grouped by the types of relation they invoke, then sorted, first by the number of existential quantifiers, then by the number of atomic sentences. The axioms should be read as universal closures; hence any free variables should be taken as tacitly universally quantified.