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.

  • 8
    $\begingroup$ The answer depends on what you define as "not-theorem". $\endgroup$ – 5xum Nov 7 '15 at 0:19
  • $\begingroup$ Some valid proposition. $\endgroup$ – Rafael Castro Nov 7 '15 at 0:20
  • $\begingroup$ Some valid (and provable) proposition. $\endgroup$ – Rafael Castro Nov 7 '15 at 0:26
  • $\begingroup$ You need to tell us what first-order theory you are working in. The answer to your "is this always true?" for the theory of the real numbers is yes, but for the theory of natural number it is no. $\endgroup$ – Rob Arthan Nov 7 '15 at 0:31
  • 1
    $\begingroup$ My comment wasn't quite right: if you fix a particular structure like $\Bbb{N}$ or $\Bbb{R}$, then the theory of that structure is complete: any sentence is either true or false. If you are looking at a theory defined by axioms and inference rules, then we need to know what those axioms and inference rules are, $\endgroup$ – Rob Arthan Nov 7 '15 at 0:51

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.

  • 3
    $\begingroup$ Note that the "assuming it's consistent" that appears a couple of times, is just because an inconsistent theory (equipped with the kinds of logic we're talking about) proves every sentence and in particular it has no undecidable sentences. From the POV of this question, there are no non-theorems anyway in that case and the question is moot :-) $\endgroup$ – Steve Jessop Nov 7 '15 at 15:02
  • $\begingroup$ @SteveJessop Thanks for adding that. It may not be obvious to all readers, or to the OP, that in an inconsistent theory there are no non-theorems (every sentence is a theorem). That's because $(p\land \neg p)\to q$ is a tautology, anyway it is in classical logic, so if a theory proves one contradiction, it proves every sentence. $\endgroup$ – BrianO Nov 8 '15 at 4:51

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).

  • $\begingroup$ You need a $\forall \text{ groups } G$ in front of your first formula, and so one of the two is true. In any case, if you specify which sets the $x$ and $y$ are being drawn from, you see that one of the two is true. $\endgroup$ – Eric Thoma Jan 31 '16 at 4:08
  • $\begingroup$ A "theorem" is a statement in a certain "theory". The theory of groups has no quantifier "$\forall$ Groups", nor does it allow talking about "sets". $\endgroup$ – GEdgar Jan 31 '16 at 14:36
  • $\begingroup$ I see. Thank you for clarifying. $\endgroup$ – Eric Thoma Jan 31 '16 at 20:43

It is not always true. There are undecidable propositions as well, propositions that are both unprovable and whose negations are unprovable. This is the essence of Gödel's first incompleteness theorem.

There are many examples in the answers to this other question.

  • 1
    $\begingroup$ The answer depends on the theory the OP is interested in. $\endgroup$ – Rob Arthan Nov 7 '15 at 0:32
  • 1
    $\begingroup$ @RobArthan I interpreted the question to be about propositions in "all of mathematics" (so including incomplete theories) but now I'm not sure I even understood the basic gist of the question. $\endgroup$ – Aaron Golden Nov 7 '15 at 0:41
  • 1
    $\begingroup$ @AaronGolden: you and I are on the same wavelength now $\ddot{\smile}$. $\endgroup$ – Rob Arthan Nov 7 '15 at 0:42
  • 1
    $\begingroup$ Whether a particular theory or a particular interpretation of "not theorem" was in intended, this post directly addresses the question as asked. Don't discount such answers. you can learn from them. +1 $\endgroup$ – Paul Sinclair Nov 7 '15 at 0:44
  • 1
    $\begingroup$ I would like to point out that this answer does not apply if the first-order theory of interest is the theory of the reals (which is what the OP said was the theory of interest in a comment under the question). The first-order theory of the reals is complete. $\endgroup$ – Rob Arthan Nov 7 '15 at 0:55

Consider an invalid (non-theorem) statement.

  • For all $z∈C$ where Re($z$)≠$0$; we must have $z_i≤z_j$.

Its negation is:

For some $z∈C$ where Re($z$)≠$0$; we must have $z_i>z_j$, which is also invalid (a non-theorem).


Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.