Teoria existencial dels número real

En llògica matemàtica, teoria de la complexitat computacional i ciències de la computació, la teoria existencial dels número real és el conjunt de totes les oracions verdaderes de la forma

$$\mathrm{\exists }{X}_1\cdots \mathrm{\exists }{X}_{n}F(X_1,\dots ,X_n),$$

a on les variables $X_i$ s'interpreten com a valors reals, i a on $F(X_1,\dots X_n)$ és una fòrmula ben formada que implica igualtats i desigualtats de polinomis reals. Una oració d'esta forma és verdadera si és possible trobar valors per a totes les variables que, en substituir-les en la fòrmula $F$, la fan verdadera.

El problema de decisió de la teoria existencial dels número real és el problema de trobar un algoritme que determine, per a cada oració, si és verdadera o falsa. De manera equivalent, és el problema de comprovar si un conjunt semialgebraico donat no és buit. Este problema de decisió és NP-difícil i residix en el PSPACE, lo que li conferix una complexitat significativament menor que el procediment ideat per Alfred Tarski de l'eliminació de quantificadors per a decidir enunciats en la teoria de primer orde dels número real sense la restricció de quantificadors existencial. No obstant, en la pràctica, els métodos generals de la teoria de primer orde seguixen sent l'opció preferida per a resoldre estos problemes.

La classe de complexitat $\mathrm{\exists }ℝ$ s'ha definit per a descriure la classe de problemes computacionals que poden traduir-se a oracions equivalents d'esta forma. En teoria de la complexitat estructural, es troba entre NP i PSPACE. Molts problemes naturals en teoria de grafos geomètrics, especialment els problemes de reconeiximent de grafos d'intersecció geomètrics i el enderezamiento de les arestes de representacions de grafos en punts de creuament, pertanyen a $\mathrm{\exists }ℝ$ i són complets per a esta classe. En este cas, la completitud significa que existix una traducció en la direcció inversa, d'una oració arbitrària sobre els número real a una instància equivalent del problema donat.

Antecedents

En llògica matemàtica, una teoria és un llenguage formal que consistix en un conjunt de sentències escrites utilisant un conjunt fix de símbols. La teoria de primer orde de cossos reals tancats té els següents símbols:

• Les constants 0 i 1
• Un conjunt numerable de variables $X_i$
• Les operacions de suma, resta, multiplicació i (opcionalmente) divisió
• Els símbols <, ≤,=, ≥, >, i ≠ per a la comparació de valors reals
• Els conectors llògics ∧, ∨, ¬, i ⇔
• Paréntesis
• El quantificador universal ∀ (para tot) i el quantificador existencial ∃ (existix).

Una seqüència d'estos símbols forma una oració que pertany a la teoria de primer orde dels reals si està gramaticalmente ben formada, totes les seues variables estan quantificades apropiadament, i (quan s'interpreta com una afirmació matemàtica sobre els número real) és una afirmació verdadera. Com va mostrar Tarski, esta teoria pot ser descrita per un esquema de axioma i un procediment de decisió que és complet i efectiu: per a cada oració completament quantificada i gramatical, l'oració o la seua negació (pero no abdós) poden derivar-se dels axioma. La mateixa teoria descriu cada cos real tancat, no solament els número real. No obstant, hi ha atres sistemes numèrics que no són descrits en precisió per estos axioma. En particular, la teoria definida de la mateixa manera per als número entero en lloc dels número real és indecidible, inclús per a oracions existencials (equacions diofánticas) segons el teorema de Matiyasevich.

La teoria existencial dels reals és un fragment de la teoria de primer orde, que consistix en oracions en les que tots els quantificadors són existencials i apareixen abans de qualsevol atre símbol. És dir, és el conjunt de totes les oracions verdaderes de la forma

$$\mathrm{\exists }{X}_1\cdots \mathrm{\exists }{X}_{n}F(X_1,\dots ,X_n),$$

a on $F(X_1,\dots X_n)$ és una fòrmula ben formada que implica igualtats i desigualtats de polinomis reals. El problema de decisió per a la teoria existencial dels reals és el problema algorítmic de comprovar si una oració donada pertany a esta teoria. De forma equivalent, per a cadenes que superen les comprovacions sintàctiques bàsiques (utilisar els símbols correctes en la sintaxis correcta i no tindre variables no quantificades), el problema consistix en comprovar si l'oració és una afirmació verdadera sobre els número real. El conjunt de $n$-tuplas d'número real $(X_1,\dots X_n)$ per a les que $F(X_1,\dots X_n)$ és verdader es denomina conjunt semialgebraico, per lo que el problema de decisió per a la teoria existencial dels reals pot reformular-se, equivalentemente, com comprovar si un conjunt semialgebraico dau és no buit.

Per a determinar la complexitat temporal del algoritme necessari per a abordar el problema de decisió de la teoria existencial dels reals, és important contar en una mida del tamany de l'entrada. La mida més simple d'este tipo és la llongitut d'una oració: és dir, el número de símbols que conté. No obstant, per a conseguir un anàlisis més precís del comportament dels algoritmes per a este problema, és convenient descompondre el tamany d'entrada en vàries variables, separant el número de variables a quantificar, el número de polinomis dins de l'oració i el grau d'estos polinomis.

Eixemples

El número áureo $\phi$ pot definir-se com la raïl del polinomi $x^2-x-1$. Este polinomi té dos raïls, de les quals solament una (la proporció áurea) és major que un. Per lo tant, l'existència de la proporció áurea pot expressar-se per mig de l'oració:

$$\mathrm{\exists }{X}_1(X_1>1\wedge X_1\times X_1-X_1-1=0).$$.

Ya que la proporció áurea no és un número trascendente, esta és una oració verdadera i pertany a la teoria existencial dels número real. La resposta al problema de decisió per a la teoria existencial dels número real, donada esta oració com a entrada, és el valor booleano verdader.

La desigualtat de les miges aritmètica i geomètrica establix que, per a cada dos números no negatius $x$ i $y$, es complix la següent desigualtat:

$$\frac{x+y}{2}\ge \sqrt{xy}.$$

Com es va mencionar anteriorment, es tracta d'una oració de primer orde sobre els número real, pero en quantificadors universals en lloc d'existencials, i que utilisa símbols adicionals per a la divisió, raïls quadrades i el número 2, símbols que no estan permesos en la teoria de primer orde dels reals. No obstant, en elevar al quadrat abdós costats, es pot transformar en la següent oració existencial, que pot interpretar-se com la pregunta de si la desigualtat té contraeixemples:

$\mathrm{\exists }{X}_1\mathrm{\exists }{X}_2(X_1\ge 0\wedge X_2\ge 0\wedge (X_1+X_2)\times (X_1+X_2)<(X_1+X_1)\times (X_2+X_2)).$

La resposta al problema de decisió per a la teoria existencial dels reals, donada esta oració com a entrada, és el valor booleano fals: no hi ha contraeixemples. Per lo tant, esta oració no pertany a la teoria existencial dels reals, a pesar de tindre la forma gramatical correcta.

Vore també

• Dècim problema de Hilbert, sobre la teoria existencial (indecidible) dels sancers.