Teorema Seidenberg-Tarski

Teorema Seidenberg-Tarski este o afirmație despre posibilitatea eliminării cuantificatorilor în teoria elementară a numerelor reale cu adunare și înmulțire ( câmpuri reale închise ), și, în consecință, asupra decidabilității acestei teorii.

Formulare

Pentru orice formulă din semnătură care conține predicate cu două locuri și , constante și și operații cu două locuri și , există o formulă fără cuantificatori echivalentă cu aceasta pe mulțimea numerelor reale . $\varphi$ $=$ $<$ $0$ $unu$ $+$ $\times$ $\psi$ $\mathbb {R}$

Note

Enunț echivalent: semialgebricitatea proiecțiilor unei mulțimi semialgebrice : deoarece proiecția unei mulțimi semialgebrice de-a lungul uneia dintre axe adaugă un cuantificator de existență la sistemul definitoriu , care poate fi eliminat, rezultatul său va fi un semi- mulţime algebrică în ; pe de altă parte, natura semialgebrică a oricărei proiecții a unei mulțimi semialgebrice asigură eliminarea cuantificatorului existenței în orice formulă, iar acesta este singurul punct netrivial din demonstrația teoremei eliminării cuantificatorului. $A\subset \mathbb {R} ^{n+1}$ $\mathbb {R} ^{n}$

Teorema poate fi considerată ca o generalizare de anvergură a teoremei lui Sturm [1] , și de aceea apare și ca o teoremă generalizată a lui Sturm . Cu o astfel de vedere, teorema lui Sturm este formulată [2] ca prezența pentru orice polinom a unei formule fără cuantificatori, astfel încât echivalența să rezulte din axiomele unui câmp real închis: $p(x,x_{1},\dots,x_{n})$ $\psi (x_{1},\dots,x_{n},a,b)$

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

; formularea teoremei Seidenberg-Tarski în acest caz este trecerea de la o formulă arbitrară fără cuantificatori , limitată de cuantificatorul existențial, la o formulă fără cuantificatori :

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

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

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

. Mai mult, dacă demonstrația clasică a teoremei lui Sturm folosește în esență tehnici de analiză (în special, teorema privind dispariția unei funcții continue care își schimbă semnul), atunci logica matematică oferă o demonstrație pur algebrică a faptului [2] .

Istorie

Demonstrat de Tarski în 1948 într-un articol despre determinabilitatea teoriilor algebrei elementare și geometriei elementare. [3] În 1954, Abraham Seidenberg a găsit o metodă de demonstrare mai simplă și mai naturală [4] [5] .

Note

↑ E. A. Gorin . Despre proprietățile asimptotice ale polinoamelor și funcțiilor algebrice ale mai multor variabile // Uspekhi Mat . - 1961. - T. 16 , nr. 1 (97) . - S. 91-118 . Arhivat din original pe 13 mai 2013.
↑ 1 2 E. Engeler. Metamatematica matematicii elementare. - M . : Mir, 1987. - S. 23-24. — 128 p.
↑ A. Tarski. O metodă de decizie pentru algebră și geometrie elementară . R-109 . RAND Corporation (1 august 1948). Consultat la 27 decembrie 2018. Arhivat din original la 11 august 2017. (nedefinit)
↑ A. Seidenberg. Nouă metodă de decizie pentru algebra elementară (engleză) // Ann. de Matematică. , Ser. 2. - 1954. - Vol. 60 . - P. 365-374 .
↑ A. Robinson . Recenzie: A. Seidenberg. O nouă metodă de decizie pentru algebra elementară. Analele matematicii, ser. 2 vol. 60 (1954), pp. 365-374. // J. Symb. Log . - 1957. - T. 22 , nr 3 . …Această lucrare scrisă elegant conține o alternativă la metoda de decizie a lui Tarski pentru „algebra elementară”, adică pentru propoziții formulate în calculul predicatului inferior cu referire la un câmp real închis (XIV 188). Ca și cea a lui Tarski, metoda descrisă aici depinde de eliminarea cuantificatorilor. În cazul de față, aceasta echivalează cu o generalizare a teoremei lui Sturm după cum urmează...

Literatură

N. K. Vereshchagin , A. Kh. Shen . 2. Limbi și calcul // Prelegeri despre logica matematică și teoria algoritmilor. - M. : MTSNMO, 2012. - S. 101-111.