Кіріспе
Бірінші реттік логикада қолданылатын аксиомалар жиынтығы. Тарски аксиомалары – Евклид геометриясы үшін аксиомалар жүйесі, атап айтқанда, бірінші реттік логикада (яғни элементар теория ретінде) тұжырымдалатын Евклид геометриясының бөлігі. Сондықтан, оған негізгі жинақтар теориясы қажет емес. Жүйенің бастапқы объектілері – тек "нүктелер", ал бастапқы предикаттары – "аралықта жату" (бір нүкте екі басқа нүктенің арасындағы түзу сызығында орналасқандығын көрсетеді) және "сәйкестік" (екі нүктенің арақашықтығы басқа екі нүктенің арақашықтығына тең екендігін көрсетеді). Жүйеде шексіз көп аксиома бар. Аксиомалар жүйесін алғаш 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.