Is the negation of a non-theorem a theorem?

I don't know if that is something obvious or if it is a dumb question. But it seems to be true.

Consider the non-theorem $\forall x. x < 1$. Its negation is $\exists x. x \geq 1$ and is a theorem. Is this always true?

I couldn't find a counterexample.

If this is true I would like to know a good explanation why.

Solution 1:

It's neither obvious nor a dumb question. But it is, perhaps surprisingly, sensitive to what theory, or at least what language, you're proving things in. I assume you intend the example you gave, $(\exists x)\,x\ge1$, as a sentence about the real numbers. The reals are a real closed field, and the theory of real closed fields is complete: every sentence or its negation is a theorem. So this really is a special case: as fate would have it, for this theory, the negation of every non-theorem actually is a theorem, so you'll search in vain for a counterexample.

However, the same cannot be said for arithmetic, as formalized by Peano arithmetic (PA): there are sentences $S$ in the language of arithmetic such that neither $S$ nor $\neg S$ is a theorem of PA (assuming, of course, that PA is consistent). Examples include Gödel sentences (true sentences asserting their own unprovability within the system), as well as more natural sentences: Goodstein's theorem, which Kirby and Paris showed is unprovable in PA, and a true sentence about finite Ramsey theory which Paris and Harrington showed is independent of PA.

Set theory offers further examples. For our purposes, it's safe to say that ZFC is the system in which contemporary mathematical practice takes place. ZFC has its own Gödel sentences (assuming it's consistent), but it turns out that many natural mathematical questions — sentences $S$ — are simply independent of the ZFC axioms: ZFC proves neither $S$ nor $\neg S$. One famous example is the Continuum Hypothesis, but the list of interesting statements independent of ZFC is substantial.

The Axiom of Choice, AC, provides the "C" in ZFC. AC says: for every set $X$ of nonempty sets, there is a function $f$ with domain $X$ such that $f(x)\in x$ for all $x\in X$ ($f$ is a choice function for $X$). ZFC without AC is the system known as ZF. It turns out AC is not provable in ZF, and the negation of AC is not provable in ZF. In some models of ZF, every set has a choice function (these models are, of course, models of ZFC); in other models, many infinite sets lack choice functions.

Finally, note that, assuming it's consistent, ZFC cannot prove its own consistency. Via Gödel numbering and arithmetization of syntax, a sentence meaning "ZFC is consistent" can be formulated within ZFC. This sentence is just a statement about the integers, which isn't provable even in ZFC. However, if we add a large cardinal axiom, even a "small large cardinal" axiom such as "There exists an inaccessible cardinal", then the resulting stronger theory can prove that ZFC is consistent, and in particular new statements of arithmetic become provable.

Solution 2:

Suppose we are talking about the theory of groups. The statement $$ \forall x \forall y \big(xy=yx\big) $$ is not a theorem (it is false for some groups). It negation $$ \exists x \exists y \big(xy \ne yx\big) $$ is also not a theorem (it, too, is false for some groups).