Seidenbergova-Tarského věta

Seidenbergova-Tarského věta je tvrzením o možnosti eliminace kvantifikátorů v elementární teorii reálných čísel se sčítáním a násobením ( uzavřená reálná pole ), a v důsledku toho o rozhodnutelnosti této teorie.

Formulace

Pro jakýkoli vzorec v podpisu obsahující dvoumístné predikáty a , konstanty a a dvoumístné operace a existuje vzorec bez kvantifikátoru, který je ekvivalentní tomuto vzorci na množině reálných čísel . $\varphi$ $=$ $<$ $0$ $jeden$ $+$ $\krát$ $\psi$ $\mathbb {R}$

Poznámky

Ekvivalentní tvrzení: semialgebraicita projekcí semialgebraické množiny : jelikož promítání semialgebraické množiny podél jedné z os přidává do definiční soustavy kvantifikátor existence , který lze eliminovat, bude jeho výsledkem semi- algebraické zasazení ; na druhé straně semialgebraická povaha jakékoli projekce semialgebraické množiny zajišťuje eliminaci kvantifikátoru existence v jakémkoli vzorci, a to je jediný netriviální bod v důkazu teorému o eliminaci kvantifikátoru. $A\subset \mathbb {R} ^{n+1}$ $\mathbb {R} ^{n}$

Větu lze považovat za dalekosáhlé zobecnění Sturmovy věty [1] , a proto se také objevuje jako zobecněná Sturmova věta . S tímto pohledem je Sturmův teorém formulován [2] jako přítomnost pro jakýkoli polynom bezkvantifikátorového vzorce tak, že ekvivalence vyplývá z axiomů uzavřeného reálného pole: $p(x,x_{1},\tečky ,x_{n})$ $\psi (x_{1},\tečky ,x_{n},a,b)$

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

; formulace Seidenbergovy-Tarského věty je v tomto případě přechodem od libovolného vzorce bez kvantifikátoru , omezeného existenčním kvantifikátorem, k formuli bez kvantifikátoru :

\varphi (x,x_{1},\tečky ,x_{n})

\psi (x_{1},\tečky ,x_{n},a,b)

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

. Navíc, pokud klasický důkaz Sturmovy věty v podstatě používá analytické techniky (zejména věta o mizení spojité funkce, která mění znaménko), pak matematická logika dává čistě algebraický důkaz skutečnosti [2] .

Historie

Prokázal Tarski v roce 1948 v článku o rozhodnutelnosti teorií elementární algebry a elementární geometrie. [3] V roce 1954 Abraham Seidenberg našel jednodušší a přirozenější metodu důkazu [4] [5] .

Poznámky

↑ E. A. Gorin . O asymptotických vlastnostech polynomů a algebraických funkcí více proměnných // Uspekhi Mat . - 1961. - T. 16 , č. 1 (97) . - S. 91-118 . Archivováno z originálu 13. května 2013.
↑ 1 2 E. Engeler. Metamatematika elementární matematiky. - M .: Mir, 1987. - S. 23-24. — 128 str.
↑ A. Tarski. Rozhodovací metoda pro elementární algebru a geometrii . R-109 . RAND Corporation (1. srpna 1948). Získáno 27. prosince 2018. Archivováno z originálu 11. srpna 2017. (neurčitý)
↑ A. Seidenberg. Nová rozhodovací metoda pro elementární algebru (anglicky) // Ann. matematiky. , Ser. 2. - 1954. - Sv. 60 . - str. 365-374 .
↑ A. Robinson . Recenze: A. Seidenberg. Nová rozhodovací metoda pro elementární algebru. Letopisy matematiky, seř. 2 sv. 60 (1954), str. 365-374. // J. Symb. Log . - 1957. - T. 22 , č. 3 . …Tento elegantně napsaný článek obsahuje alternativu k Tarskiho rozhodovací metodě pro „elementární algebru“, tj. pro věty formulované v nižším predikátovém počtu s odkazem na reálně uzavřené pole (XIV 188). Stejně jako Tarskiho i zde popsaná metoda závisí na eliminaci kvantifikátorů. V tomto případě to znamená zobecnění Sturmovy věty takto…

Literatura

N. K. Vereščagin , A. Kh. Šen . 2. Jazyky a počet // Přednášky o matematické logice a teorii algoritmů. - M. : MTSNMO, 2012. - S. 101-111.