Seidenberg-Tarskis sats

Seidenberg-Tarski-satsen är ett uttalande om möjligheten att eliminera kvantifierare i den elementära teorin för reella tal med addition och multiplikation ( stängda reella fält ), och som en konsekvens av denna teoris avgörbarhet.

Formulering

För varje formel i signaturen som innehåller tvåställspredikat och , konstanter och och tvåställsoperationer och , finns det en kvantifieringsfri formel som motsvarar den i uppsättningen av reella tal . $\varphi$ $=$ $<$ $0$ $ett$ $+$ $\ gånger$ $\psi$ $\mathbb {R}$

Anteckningar

Motsvarande uttalande: semi-algebraicitet av projektioner av en semi-algebraisk mängd : eftersom projektionen av en semi-algebraisk mängd längs en av axlarna lägger till en existenskvantifierare till det definierande systemet , som kan elimineras, kommer dess resultat att bli en semi- algebraisk inställd ; å andra sidan säkerställer den semi-algebraiska karaktären av varje projektion av en semi-algebraisk mängd eliminering av existenskvantifieraren i vilken formel som helst, och detta är den enda icke-triviala punkten i beviset för kvantifierarelimineringssatsen. $A\subset \mathbb {R} ^{n+1}$ $\mathbb {R} ^{n}$

Satsen kan betraktas som en långtgående generalisering av Sturms sats [1] , och framstår därför också som en generaliserad Sturms sats . Med ett sådant synsätt formuleras Sturms sats [2] som närvaron för vilket polynom som helst av en kvantifieringsfri formel så att ekvivalensen följer av axiomen för ett slutet reellt fält: $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 av Seidenberg-Tarski-satsen i detta fall är övergången från en godtycklig kvantifierarfri formel , begränsad av den existentiella kvantifieraren, till en kvantifierarfri 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}))

. Dessutom, om det klassiska beviset för Sturms sats huvudsakligen använder analystekniker (i synnerhet satsen om försvinnandet av en kontinuerlig funktion som ändrar tecken), så ger matematisk logik ett rent algebraiskt bevis på faktumet [2] .

Historik

Bevisades av Tarski 1948 i en artikel om avgörbarheten av teorier om elementär algebra och elementär geometri. [3] År 1954 hittade Abraham Seidenberg en enklare och mer naturlig bevismetod [4] [5] .

Anteckningar

↑ E. A. Gorin . Om asymptotiska egenskaper hos polynom och algebraiska funktioner hos flera variabler // Uspekhi Mat . - 1961. - T. 16 , nr 1 (97) . - S. 91-118 . Arkiverad från originalet den 13 maj 2013.
↑ 1 2 E. Engeler. Elementär matematiks metamatematik. - M .: Mir, 1987. - S. 23-24. — 128 sid.
↑ A. Tarski. En beslutsmetod för elementär algebra och geometri . R-109 . RAND Corporation (1 augusti 1948). Hämtad 27 december 2018. Arkiverad från originalet 11 augusti 2017. (obestämd)
↑ A. Seidenberg. Ny beslutsmetod för elementär algebra (engelska) // Ann. av matte. , Ser. 2. - 1954. - Vol. 60 . - s. 365-374 .
↑ A. Robinson . Recension: A. Seidenberg. En ny beslutsmetod för elementär algebra. Annaler av matematik, ser. 2 vol. 60 (1954), sid. 365-374. // J. Symb. Logga . - 1957. - T. 22 , nr 3 . …Denna elegant skrivna uppsats innehåller ett alternativ till Tarskis beslutsmetod för "elementär algebra", dvs för meningar formulerade i den nedre predikatkalkylen med hänvisning till ett reellt slutet fält (XIV 188). Liksom Tarskis är metoden som beskrivs här beroende av eliminering av kvantifierare. I det aktuella fallet motsvarar detta en generalisering av Sturms teorem enligt följande...

Litteratur

N. K. Vereshchagin , A. Kh. Shen . 2. Språk och analys // Föreläsningar om matematisk logik och teori om algoritmer. - M. : MTSNMO, 2012. - S. 101-111.