Como un modelo teórico, aquí está cómo iba a pensar acerca de este problema. Estoy seguro de que hay maneras más directas de resolver, pero voy a describir una "lógica".
En primer lugar, recordemos que la teoría de la real campos cerrados es decidable. Esto significa que para cualquier frase, $\varphi$ en el primer orden lenguaje de ordenada campos, existe un algoritmo (aunque increíblemente ineficiente algoritmo) para determinar si $\varphi$ es verdadera o falsa en $\mathbb{R}$. Usted puede ver esto como un caso especial de la efectiva eliminación de cuantificadores para la teoría de la RCF de bienes de campos cerrados: Existe un algoritmo que encuentra, para cualquiera de primer orden de la fórmula $\varphi(x_1,\dots,x_n)$, lo que equivale a cuantificador fórmula libre de $\psi(x_1,\dots,x_n)$. Una oración es sólo una fórmula, sin variables libres, y cuantificador libre de penas son fácilmente decidable.
OK, pero la declaración "existen infinidad de $(x,y)$ tal que $p(x,y) = 0$" no es expresable como una de primer orden de la frase - la lógica de primer orden no tiene el cuantificador "existe un número infinito". Así que vamos a romper lo que esto significa.
Tenga en cuenta que si $p$ tiene una infinidad de raíces, entonces (1) hay algunos $a$ tal que existen infinitos $b$$p(a,b) = 0$, o (2) hay una infinidad de $a$ que hay algunos $b$$p(a,b) = 0$. Así que nuestra condición es equivalente a $$(\exists x\,\exists^\infty y\,p(x,y) = 0)\lor (\exists^\infty x\,\exists y\,p(x,y)),$$
donde $\exists^\infty$ es sinónimo de "no existen infinidad".
Mirando en el caso (1) en primer lugar, tenga en cuenta que para cualquier fijo $x = a$, $p(a,y)$ es un polinomio en a $y$, e $\exists^\infty y\,p(a,y) = 0$ si y sólo si $p(a,y)$ es el polinomio cero. Escrito $p(x,y) = \sum_{i=0}^d q_i(x)y^d$, podemos ver que $p(a,y) = 0$ si y sólo si $a$ es una raíz común de los polinomios $\{q_0(x),\dots,q_d(x)\}$. Por lo tanto, $\exists x\, \exists^\infty y\,p(x,y)$ es equivalente a $\exists x\, \bigwedge_{i=0}^d q_i(x) = 0$, y ahora podemos aplicar el procedimiento de decisión para la RCF para responder a esta pregunta.
De inflexión para el caso (2), vamos a $\varphi(x)$ ser la fórmula $\exists y\, p(x,y)$. Es una consecuencia de la eliminación de cuantificadores que cualquier fórmula en una variable libre se define una unión finita de puntos e intervalos (es lo que significa decir que la RCF es o-mínimo), y una unión finita de puntos e intervalos es infinito si y sólo si contiene un intervalo abierto no vacío. Por lo tanto, $\exists^\infty x\, \varphi(x)$ es equivalente a $$\exists z_1\, \exists z_2\, ((z_1<z_2)\land (\forall w\, (z_1<w<z_2)\rightarrow \varphi(w))),$$
y ahora podemos aplicar el procedimiento de decisión para la RCF para responder a esta pregunta.
Después de haber dado un algoritmo para decidir si cada uno de los casos es cierto, hemos terminado.
Usted podría desea profundizar más y ver si usted puede reemplazar las dos aplicaciones del algoritmo de decisión caja de color negro con más concretos (y eficiente!) los algoritmos. En la parte (1) sólo pedimos que si un sistema de polinomios en una variable tiene una raíz común, que se puede hacer uso de las bases de Gröbner. La aplicación en la parte (2) era un poco más complicado, pero puede ser desglosado de la siguiente manera. En primer lugar, se podría aplicar a la eliminación de cuantificador a $\varphi(x)$ ( $\exists y\, p(x,y) = 0$ ). Esto equivale a venir para arriba con un cuantificador de condición libre en $a$ que es equivalente a la polinomio $p(a,y)$ tener una raíz, que se puede hacer trabajando cuidadosamente a través de una aplicación de Sturm del teorema de a $p(a,y)$, y mantener un seguimiento de cómo las propiedades de $a$ afectan la respuesta. Ahora dejando $\psi(x)$ ser el cuantificador libre equivalente a $\varphi(x)$, podemos poner $\psi(x)$ en forma normal disyuntiva como $\bigvee_{k=1}^m \psi_k(x)$ y preguntar si alguno de los $\psi_k(x)$ contienen un intervalo abierto. Cada una de las $\psi_k$ es una conjunción de atómica y negada atómica condiciones, que es equivalente a un sistema de polinomio desigualdades, cada uno de la forma $q_i(x) \leq 0$ o $q_i(x) \geq 0$. Puede comprobar si el conjunto solución de este sistema contiene un intervalo abierto no vacío mediante la comprobación para ver si alguno de los polinomios involucrados comparten raíces y, a continuación, la aproximación de las raíces lo suficientemente precisa.
Bonificación nota: a Pesar del hecho de que la lógica de primer orden no tiene el cuantificador $\exists^\infty$ ("existen infinidad de"), aún se puede hablar de "eliminación del cuantificador $\exists^\infty$". Una teoría de la $T$ elimina $\exists^\infty$ si para cada fórmula $\varphi(x_1,\dots,x_n,y)$, no es una fórmula $\psi(x_1,\dots,x_n)$ tal que para cualquier tupla $\overline{a}$ a partir de un modelo de $M$ de $T$, $M\models \psi(a_1,\dots,a_n)$ si y sólo si existen infinitos $b$ tal que $M\models \varphi(a_1,\dots,a_n,b)$. Esta eliminación es efectiva si existe un algoritmo que produce $\psi$$\varphi$.
Ahora RCF elimina $\exists^\infty$ (de hecho, todos los o-teoría mínima no, ver la Finitud Lema 3.1.7 en Domar a la topología y de la o-un mínimo de estructuras por van den Dries). Y estoy seguro de que lo hace de manera efectiva, lo que podría responder a la pregunta directamente. Pero no sé de referencia de la parte superior de mi cabeza, y escribir el algoritmo implicaría un razonamiento similar a lo que escribí anteriormente, pero en mucho mayor generalidad.
