Teorema de Seidenberg-Tarski

El teorema de Seidenberg-Tarski es un enunciado sobre la posibilidad de eliminar cuantificadores en la teoría elemental de los números reales con suma y multiplicación ( campos reales cerrados ), y, en consecuencia, la decidibilidad de esta teoría.

Redacción

Para cualquier fórmula en la firma que contenga predicados de dos lugares y , constantes y operaciones de dos lugares y , existe una fórmula equivalente sin cuantificador en el conjunto de números reales . $\varphi$ $=$ $<$ ${\ estilo de visualización 0}$ $una$ $+$ $\veces$ $\psi$ $\matemáticas {R}$

Notas

Enunciado equivalente: semialgebraicidad de proyecciones de un conjunto semialgebraico : dado que la proyección de un conjunto semialgebraico a lo largo de uno de los ejes agrega un cuantificador de existencia al sistema definidor , que puede eliminarse, su resultado será un semi- conjunto algebraico en ; por otro lado, la naturaleza semialgebraica de cualquier proyección de un conjunto semialgebraico asegura la eliminación del cuantificador de existencia en cualquier fórmula, y este es el único punto no trivial en la demostración del teorema de eliminación del cuantificador. $A\subconjunto \mathbb {R} ^{n+1}$ $\mathbb{R} ^{n}$

El teorema se puede considerar como una generalización de gran alcance del teorema de Sturm [1] y, por lo tanto, también aparece como un teorema de Sturm generalizado . Con tal visión, el teorema de Sturm se formula [2] como la presencia para cualquier polinomio de una fórmula libre de cuantificadores tal que la equivalencia se sigue de los axiomas de un campo real cerrado: $p(x,x_{1},\dots,x_{n})$ ${\ estilo de visualización \ psi (x_{1}, \ puntos, 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}, \puntos,x_{n})=0)

; la formulación del teorema de Seidenberg-Tarski en este caso es la transición de una fórmula arbitraria sin cuantificador , limitada por el cuantificador existencial, a una fórmula sin cuantificador :

{\ estilo de visualización \ varphi (x, x_{1}, \ puntos, x_ {n})}

{\ estilo de visualización \ psi (x_{1}, \ puntos, 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} ,\puntos,x_{n}))

. Además, si la prueba clásica del teorema de Sturm utiliza esencialmente técnicas de análisis (en particular, el teorema de la desaparición de una función continua que cambia de signo), entonces la lógica matemática proporciona una prueba puramente algebraica del hecho [2] .

Historia

Demostrado por Tarski en 1948 en un artículo sobre la decidibilidad de las teorías del álgebra elemental y la geometría elemental. [3] En 1954, Abraham Seidenberg encontró un método de prueba más simple y natural [4] [5] .

Notas

↑ EA Gorin . Sobre propiedades asintóticas de polinomios y funciones algebraicas de varias variables // Uspekhi Mat . - 1961. - T. 16 , N° 1 (97) . - S. 91-118 . Archivado desde el original el 13 de mayo de 2013.
↑ 1 2 E. Engeler. Metamatemáticas de las matemáticas elementales. - M. : Mir, 1987. - S. 23-24. — 128 págs.
↑ A. Tarski. Un método de decisión para álgebra y geometría elementales . R-109 . Corporación RAND (1 de agosto de 1948). Consultado el 27 de diciembre de 2018. Archivado desde el original el 11 de agosto de 2017. (indefinido)
↑ A. Seidenberg. Nuevo método de decisión para álgebra elemental (inglés) // Ann. de Matemáticas. , Ser. 2.- 1954.- vol. 60 . - pág. 365-374 .
↑ A. Robinson . Reseña: A. Seidenberg. Un nuevo método de decisión para álgebra elemental. Anales de matemáticas, ser. 2 vol. 60 (1954), págs. 365-374. // J. Símbolo. Iniciar sesión . - 1957. - T. 22 , N º 3 . …Este artículo elegantemente escrito contiene una alternativa al método de decisión de Tarski para “álgebra elemental”, es decir, para oraciones formuladas en el cálculo de predicados inferiores con referencia a un campo cerrado real (XIV 188). Al igual que el de Tarski, el método descrito aquí depende de la eliminación de cuantificadores. En el presente caso, esto equivale a una generalización del teorema de Sturm de la siguiente manera...

Literatura

N. K. Vereshchagin , A. Kh. Shen . 2. Lenguajes y Cálculo // Clases de Lógica Matemática y Teoría de Algoritmos. - M. : MTSNMO, 2012. - S. 101-111.