No es ni evidente ni una pregunta tonta. Pero es, quizás sorprendentemente, sensibles a lo que la teoría, o al menos lo que el lenguaje, estamos probando cosas. Supongo que la intención de que el ejemplo que usted dio, $(\exists x)\,x\ge1$, como una frase acerca de los números reales. Los reales son un verdadero campo cerrado, y la teoría de la real campos cerrados es completa: cada frase o su negación es un teorema. Así que esto es realmente un caso especial: como la suerte lo tendría, para esta teoría, la negación de todos los no-teorema de la realidad es un teorema, por lo que vas a buscar en vano un contraejemplo.
Sin embargo, el mismo no puede decirse de la aritmética, formalizadas por la aritmética de Peano (PA): hay frases $S$ en el lenguaje de la aritmética de tal manera que ninguno de $S$ ni $\neg S$ es un teorema de la PA (suponiendo, claro, que la PA es consistente). Los ejemplos incluyen Gödel frases (true sentencias que afirman su propio unprovability dentro del sistema), así como la más natural de las sentencias: el teorema de Goodstein, que Kirby y París se mostró no demostrable en PA, y una verdadera sentencia sobre finito Ramsey teoría de que París y Harrington mostró es independiente de la PA.
La teoría de conjuntos ofrece más ejemplos. Para nuestros propósitos, es seguro decir que ZFC es el sistema en el que los contemporáneos de la práctica de matemáticas se lleva a cabo. ZFC tiene su propio Gödel frases (suponiendo que es constante), pero resulta que muchos de los naturales de preguntas de matemáticas - sentencias de $S$ - son, sencillamente, independiente de los axiomas de ZFC: ZFC demuestra ni $S$ ni $\neg S$. Un ejemplo famoso es la Hipótesis continua, pero la lista de declaraciones interesantes independiente de ZFC es sustancial.
El Axioma de Elección, CA, ofrece la "C" en ZFC. AC dice:
para cada conjunto $X$ de conjuntos no vacíos, hay una función de $f$ dominio $X$ tal que $f(x)\in x$ para todos los $x\in X$ ($f$ es una función de elección para $X$). ZFC sin AC es el sistema conocido como de ZF. Resulta que AC no es comprobable en ZF, y la negación de la AC no es comprobable en ZF. En algunos modelos de ZF, cada conjunto tiene una función de elección (estos modelos son, por supuesto, los modelos de ZFC); en otros modelos, muchos de los conjuntos infinitos falta de elección de las funciones.
Por último, tenga en cuenta que, asumiendo que es consistente, ZFC no puede probar su propia consistencia. A través de la numeración de Gödel y arithmetization de sintaxis, una frase que significa "ZFC es consistente" puede ser formulado dentro de ZFC. Esta frase es sólo una declaración acerca de los números enteros, que no es comprobable, incluso en ZFC. Sin embargo, si añadimos un gran cardenal axioma, incluso un "pequeño gran cardenal" axioma como "existe un cardinal inaccesible", y el resultado es más fuerte la teoría puede demostrar que ZFC es consistente, y, en particular, las nuevas declaraciones de la aritmética convertido en demostrable.