Seidenberg-Tarski tétel

A Seidenberg-Tarski-tétel a valós számok elemi elméletében való kvantorok összeadás és szorzás ( zárt valós mezők ) kiküszöbölésének lehetőségére , és ennek következtében ennek az elméletnek a eldönthetőségére vonatkozó kijelentés.

Megfogalmazás

Az aláírásban szereplő bármely képlethez , amely kéthelyű predikátumokat és , konstansokat és kéthelyes műveleteket és és , létezik vele egyenértékű kvantormentes formula a valós számok halmazán . $\varphi$ $=$ $<$ $0$ $egy$ $+$ $\szor$ $\psi$ $\mathbb {R}$

Jegyzetek

Ekvivalens állítás: félalgebrai halmaz vetületeinek félalgebraisága : mivel egy félalgebrai halmaz valamelyik tengely mentén történő vetülete egy létezési kvantort ad a definiáló rendszerhez , ami kiküszöbölhető, ennek eredménye egy félig algebrai halmaz ; másrészt egy félalgebrai halmaz bármely vetületének félalgebrai jellege biztosítja a létező kvantor megszüntetését bármely képletben, és ez az egyetlen nem triviális pont a kvantor eliminációs tétel bizonyításában. $A\subset \mathbb {R} ^{n+1}$ $\mathbb {R} ^{n}$

A tétel a Sturm-tétel [1] messzemenő általánosításának tekinthető , ezért általánosított Sturm-tételként is megjelenik . Ilyen nézetben a Sturm-tétel [2] úgy van megfogalmazva, hogy bármely polinomra létezik egy kvantormentes formula úgy, hogy az ekvivalencia egy zárt valós mező axiómáiból következik: $p(x,x_{1},\dots ,x_{n})$ $\psi (x_{1},\dots ,x_{n},a,b)$

a<b\Rightarrow \psi (x_{1},\pontok ,x_{n},a,b)\equiv \exists x(a<x<b\land p(x,x_{1}, \pontok ,x_{n})=0)

; A Seidenberg-Tarski-tétel megfogalmazása ebben az esetben az átmenet egy tetszőleges kvantormentes formuláról , amelyet az egzisztenciális kvantor korlátoz, egy kvantormentes formulára :

\varphi (x,x_{1},\dots ,x_{n})

\psi (x_{1},\dots ,x_{n},a,b)

a<b\Rightarrow \psi (x_{1},\pontok ,x_{n},a,b)\equiv \exists x(a<x<b\land \varphi (x,x_{1}) ,\pontok ,x_{n}))

. Sőt, ha a Sturm-tétel klasszikus bizonyítása alapvetően elemzési technikákat alkalmaz (különösen az előjelet változtató folytonos függvény eltűnéséről szóló tételt), akkor a matematikai logika tisztán algebrai bizonyítékot ad a tényre [2] .

Történelem

Tarski bizonyította 1948 - ban az elemi algebra és az elemi geometria elméleteinek eldönthetőségéről szóló cikkében . [3] 1954-ben Abraham Seidenberg talált egy egyszerűbb és természetesebb bizonyítási módszert [4] [5] .

Jegyzetek

↑ E. A. Gorin . A polinomok aszimptotikus tulajdonságairól és több változó algebrai függvényeiről // Uspekhi Mat . - 1961. - T. 16 , 1. szám (97) . - S. 91-118 . Archiválva az eredetiből 2013. május 13-án.
↑ 1 2 E. Engeler. Az elemi matematika metamatematikája. - M . : Mir, 1987. - S. 23-24. — 128 p.
↑ A. Tarski. Döntési módszer elemi algebra és geometria számára . R-109 . RAND Corporation (1948. augusztus 1.). Letöltve: 2018. december 27. Az eredetiből archiválva : 2017. augusztus 11.. (határozatlan)
↑ A. Seidenberg. Új döntési módszer elemi algebrához (angol) // Ann. a Math. , Ser. 2. - 1954. - évf. 60 . - P. 365-374 .
↑ A. Robinson . Recenzió: A. Seidenberg. Új döntési módszer elemi algebra számára. A matematika évkönyvei, ser. 2 köt. 60 (1954), pp. 365-374. // J. Symb. Bejelentkezés . - 1957. - T. 22 , 3. sz . …Ez az elegánsan megírt dolgozat Tarski döntési módszerének alternatíváját tartalmazza az „elemi algebra”, azaz az alsó predikátumkalkulusban megfogalmazott mondatok esetében egy valós zárt mezőre hivatkozva (XIV 188). Tarskihoz hasonlóan az itt leírt módszer is a kvantorok kiiktatásától függ. Jelen esetben ez Sturm tételének a következő általánosítását jelenti…

Irodalom

N. K. Verescsagin , A. Kh. Shen . 2. Nyelvek és kalkulus // Előadások a matematikai logikáról és az algoritmusok elméletéről. - M. : MTSNMO, 2012. - S. 101-111.