Seidenberg-Tarski teorem

Seidenberg-Tarski-sætningen er et udsagn om muligheden for at eliminere kvantifikatorer i den elementære teori for reelle tal med addition og multiplikation ( lukkede reelle felter ), og som en konsekvens denne teoris afgørelighed .

Ordlyd

For enhver formel i signaturen , der indeholder to-steds prædikater og , konstanter og og to-steds operationer og , findes der en kvantifier-fri formel svarende til den på sættet af reelle tal . $\varphi$ $=$ $<$ $0$ $en$ $+$ $\ gange$ $\psi$ $\mathbb {R}$

Noter

Tilsvarende udsagn: semi-algebraicitet af projektioner af et semi-algebraisk sæt : da projektionen af et semi-algebraisk sæt langs en af akserne tilføjer en eksistenskvantator til det definerende system , som kan elimineres, vil dets resultat være en semi- algebraisk sat i ; på den anden side sikrer den semi-algebraiske karakter af enhver projektion af en semi-algebraisk mængde eliminering af eksistenskvantifieren i enhver formel, og dette er det eneste ikke-trivielle punkt i beviset for kvantifier-elimineringssætningen. $A\subset \mathbb {R} ^{n+1}$ $\mathbb {R} ^{n}$

Sætningen kan betragtes som en vidtgående generalisering af Sturms sætning [1] , og fremstår derfor også som en generaliseret Sturms sætning . Med en sådan opfattelse er Sturms sætning formuleret [2] som tilstedeværelsen for et hvilket som helst polynomium af en kvantifier-fri formel , således at ækvivalensen følger af aksiomer af et lukket reelt felt: $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)

; Formuleringen af Seidenberg-Tarski-sætningen i dette tilfælde er overgangen fra en vilkårlig kvantifier-fri formel , begrænset af den eksistentielle kvantifier, til en kvantifier-fri formel :

\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} ,\dots ,x_{n}))

. Desuden, hvis det klassiske bevis for Sturms sætning i det væsentlige bruger analyseteknikker (især sætningen om forsvinden af en kontinuert funktion, der skifter fortegn), så giver matematisk logik et rent algebraisk bevis for faktum [2] .

Historie

Bevist af Tarski i 1948 i en artikel om afgøreligheden af teorier om elementær algebra og elementær geometri. [3] I 1954 fandt Abraham Seidenberg en enklere og mere naturlig bevismetode [4] [5] .

Noter

↑ E. A. Gorin . Om asymptotiske egenskaber af polynomier og algebraiske funktioner af flere variable // Uspekhi Mat . - 1961. - T. 16 , nr. 1 (97) . - S. 91-118 . Arkiveret fra originalen den 13. maj 2013.
↑ 1 2 E. Engeler. Metamatematik af elementær matematik. - M . : Mir, 1987. - S. 23-24. — 128 s.
↑ A. Tarski. En beslutningsmetode for elementær algebra og geometri . R-109 . RAND Corporation (1. august 1948). Hentet 27. december 2018. Arkiveret fra originalen 11. august 2017. (ubestemt)
↑ A. Seidenberg. Ny beslutningsmetode for elementær algebra (engelsk) // Ann. af matematik. , Ser. 2. - 1954. - Bd. 60 . - S. 365-374 .
↑ A. Robinson . Anmeldelse: A. Seidenberg. En ny beslutningsmetode for elementær algebra. Annals of Mathematics, ser. 2 bind. 60 (1954), s. 365-374. // J. Symb. Log . - 1957. - T. 22 , nr. 3 . …Dette elegant skrevne papir indeholder et alternativ til Tarskis beslutningsmetode for "elementær algebra", dvs. for sætninger formuleret i den nedre prædikatregning med henvisning til et reelt lukket felt (XIV 188). Ligesom Tarskis afhænger den her beskrevne metode af eliminering af kvantifikatorer. I det foreliggende tilfælde svarer dette til en generalisering af Sturms sætning som følger...

Litteratur

N. K. Vereshchagin , A. Kh. Shen . 2. Sprog og regning // Forelæsninger om matematisk logik og teori om algoritmer. - M. : MTSNMO, 2012. - S. 101-111.