Godel's incompleteness theorem states there will be unprovable statements in some language. Can it be proven that the unprovable statements in some language $F$ are necessarily not just "trivially unprovable" statements such as:

  • The axioms themselves (statements taken to be true in the absence of proof) Note: Servaes has kindly advised advised these are considered "trivially provable" and therefore not applicable - fine.

  • Theorems of the metatheory (e.g. True is True; True is not False) Note: Noah Schweber has advised these are trivial theorems and therefore not applicable - fine.

  • Illogical statements (statements whose negation requires the statement be true e.g. the liar paradox) Note: Please see longer footnote below.

  • "Ungrounded statements" as described by Saul Kripke here (Note: I've this category added at a later date)

  • Any other cases of "trivially unprovable" statements which I haven't identified.

    Clearly we have the category "Proof that something, which is not a theorem of the axioms, does not exist." into which falls the example of the continuum hypothesis in ZFC which is thought unlikely to fit into any of the above categories - so it would seem likely that there must be non-trivial statements in some languages which are unprovable, but is it proven, or provable, that there necessarily exist unprovable statements not fitting into any of these "trivial" categories, in every language? (Note bolding added later as the meaning was missed by some readers before)

    What I'm trying to do here, is to categorise in some sense the types of unprovable statements and circumstances in which they arise.

    Note with respect to Illogical Statements: In response to advice I'm defining more explicitly what I consider an illogical statement and why I think the Liar Paradox is one. Please correct any misconception!

    Definition: An illogical statement is a statement whose truth value is the inverse of its own truth value.

    1: (Sentence $s_1$ is illogical if $s_1\implies\neg s_1$ or $\neg s_1\implies s_1$)

    2: Let $s_1$ be the Liar Paradox "This sentence is false.".

    3: Rewriting 2: $s_1\implies \neg s_1$

    4: From 3,1: $\implies s_1$ is illogical.

    And for the modified Liar: Modified Liar: This sentence is unprovable:

    5: Let $s_2$ be "This sentence is unprovable."

    6: $(s_2\implies s_2)\implies\neg s_2$

    7: $s_2\implies\neg s_2$

    8: From 7,1: $\implies s_2$ is illogical.

    Please don't shower the question with downvotes... I'm still learning! Give me a chance to improve the question.

  • $\endgroup$
    • 5
      $\begingroup$ Aren't the axioms of a language trivially provable? That is, simply their statement constitutes a proof within the language. $\endgroup$ – Servaes Jun 12 '16 at 16:43
    • $\begingroup$ Goodstein's theorem is known to be undecidable in PA, and it doesn't appear to me to be in any of the categories you mentioned. $\endgroup$ – MJD Jun 12 '16 at 16:46
    • 2
      $\begingroup$ G's incompleteness theorem "manufacture" unprovable sentences (relative to the theory considered) that belong to no one of your cases. $\endgroup$ – Mauro ALLEGRANZA Jun 12 '16 at 16:47
    • 2
      $\begingroup$ First of all, the axioms are provable in the axiom system - they are just one-line proofs. Godel is about what is provable in an axiom system, and in an axiom system, the axioms are proven. (2) Godel finds a statement in the theory which can't be proven. The statement has a meta-meaning - we want it to be true to match our intuition about the natural numbers - but it is neither true nor false in the axiom system. The axiom system just doesn't specify our intuition about the natural numbers enough. $\endgroup$ – Thomas Andrews Jun 12 '16 at 16:50
    • 1
      $\begingroup$ @RobertFrost As my answer states, given any reasonable theory $T$ there will be a Diophantine equation $E$ such that the sentence "$E$ has no solutions" is neither provable nor disprovable by $T$. This is about as concrete as it gets. Another response: for any reasonable $T$, we can find a $\varphi$ which is not decidable from $T$, but such that neither $T+\varphi$ nor $T+\neg\varphi$ proves $Con(T)$ (HINT: otherwise $T+\neg Con(T)$ would be complete . . .). And, by the way, you still haven't defended your claim of illogicality in any real way! $\endgroup$ – Noah Schweber Jun 14 '16 at 20:25

    It seems you are confused about the statement of Godel's theorem:

    If $T$ is a "reasonable" first-order theory, then there is a first-order sentence $\varphi$ in the language of $T$ such that neither $\varphi$ nor $\neg\varphi$ is provable in $T$.

    None of the examples you give are examples of such a sentence!

    • The axioms of a theory $T$ are provable in $T$.

    • Statements like "This statement is false" cannot be expressed in first-order logic.

    • I'm not sure what "True is true" means, but if you're going to express it in first-order logic, it would presumably be "$\top\iff \top$," which is indeed a theorem, as is "$\neg(\top\iff\bot)$."

    I think the following might help explain why Godel isn't trivial:

    Let's work with the theory $PA$ (Peano arithmetic) for simplicity. It's language is $\{+, \times, <, 0, 1\}$, which means that a first-order sentence in this language is built out of

    • Those symbols,

    • variables - which are interpreted as ranging over numbers,

    • quantifiers $\exists$ and $\forall$ - again, ranging over numbers,

    • Booleans $\wedge, \vee, \implies$, and $\neg$,

    • and okay fine we also want parentheses "$($" and "$)$".

    At this point it's a good exercise to sit down and try to express "This statement is false" in this way. You'll quickly find that it seems to be impossible: the language simply isn't expressive enough to talk about sentences and truth. Now, the genius of Godel's proof is the realization that actually the language of arithmetic can talk about sentences and provability (if not truth) in an indirect-but-still-powerful way, via Godel numbering. And then a modified version of the Liar paradox - specifically, the sentence $$\mbox{"This sentence is not provable in $PA$"}$$ (or better yet, Rosser's variation - "For every $PA$-proof of this sentence, there is a shorter $T$-disproof of this sentence") - lets us show that $PA$ is incomplete.

    But this is extremely non-trivial, since at the outset it's not clear at all how to form sentences which talk about sentences, let alone sentences which talk about themselves, in the very narrow first-order language of $PA$!

    EDIT, in reply to your comments below: Let's start with your last comment. The notion of "proof" in Godel's theorem is "proof from the axioms of $T$"; there is simply no relevant notion of ex nihilo proof. So yes, the axioms of $T$ are trivially provable from $T$.

    This is a good point, though - in my above formulation of the Godel sentence, I used "prove" as shorthand for "prove in $PA$," which I should not have done. I've fixed it now.

    As to expressing the Liar Paradox in the language of arithmetic - no, those don't work, for a number of reasons:

    • First, a very minor point: "$x\not=x$" and "$x=y\iff x\not=y$" aren't sentences, they're formulas - they have free variables. So you'd need to quantify them out first - e.g. "$\forall x(x\not=x)$," or similarly.

    • Second, those sentences (even when made into genuine sentences) aren't paradoxical, they're just wrong. Think about it: "$0\not=0$" isn't a paradox, it's just a false statement.

    • Third, more fundamentally, you seem to be treating the variables as ranging over sentences (motivating e.g. "$x\not=x$" as "a sentence is not equal to itself"). But they don't do this: the variables range only over numbers.

    • Fourth, even if they did range over sentences (and they can be treated as doing so in certain contexts, via Godel number, if we're careful), there's nothing forcing the variable "$x$" in "$x\not=x$" to refer to the formula "$x\not=x$" itself - and self-reference is critical to the Liar Paradox. "This statement is false" is a paradox; "some other statement is false" isn't, really.

    Finally, there's your objection that the Godel sentence is "illogical." I'm not really sure what that means, but I think you're still assuming that the language of arithmetic is broader than it actually is. The Godel sentence (and its many variations) is just a statement about natural numbers; the fact that it has any self-referential character at all is surprising. And we can do even more concretely: as a corollary of the MRDP theorem, as long as $T$ is a true, computably axiomatizable theory, there is a Diophantine equation $E_T$ such that

    • $E_T$ has no solutions, but

    • $T$ cannot prove "$E_T$ has no solutions."

    This is about as concrete as it gets; I don't know any way that Diophantine equations are "illogical." Recall: a Diophantine equation is an equation of the form $p(x_1, . . . , x_n)=q(x_1, . . . , x_n)$ where $p$ and $q$ are polynomials with natural number coefficients; and a solution to a Diophantine equation is a set of natural numbers which solves it.

    In fact, the construction of $E_T$ from $T$ is effective: there is a computable function $f$ such that, if $e$ is a code (i.e. Turing machine index) for a true computably axiomatizable theory $T$ in the language of arithmetic, then $f(e)$ is a code for a Diophantine equation which has no solutions but which $T$ can't prove has no solutions.

    Tl;dr: I think you should go back and read the proof of Godel's theorem, and the surrounding definitions in mathematical logic, carefully. It is not trivial, nor is the Godel sentence illogical. Peter Smith's book does a very good job explicating it.

    • $\begingroup$ An aside: in the first part of my answer I implied that "$\top$" and "$\bot$" are symbols in first-order logic, yet they're missing from my description of first-order logic in the second part of my answer. This is fine, though: we can treat "$\top$" as an abbreviation for "$\forall x(x=x)$," and similarly for "$\bot$". $\endgroup$ – Noah Schweber Jun 12 '16 at 17:31
    • 1
      $\begingroup$ @RobertFrost No, this is incorrect. While it is true that "This statement is false" implies "$\exists x(x\not=x)$" (or at least, it would be true if "This statement is false" could be expressed as a first-order sentence), it is not true that "$\exists x(x\not=x)$" is equivalent (in any nice sense) to "This statement is false." The sentence "$\exists x(x\not=x)$" is straightforwardly false; the sentence "This statement is false" is paradoxical. Finally, for the third time, variables in first-order logic range over numbers, not sentences. (Cont'd) $\endgroup$ – Noah Schweber Jun 13 '16 at 18:00
    • 1
      $\begingroup$ Also, I have no idea what "illogical" means in this context. All the sentences involved here are sentences about natural numbers! And the Godel sentence does not declare itself to be an axiom; "axiom" is a precise term, and refers only to the specific elements of the theory $T$. There is a relation to the Liar paradox, but they're quite different things. $\endgroup$ – Noah Schweber Jun 13 '16 at 18:01
    • 1
      $\begingroup$ "I'm concerned that these examples have illogicality in them." This sentence, insofar as it means anything, is false. You should actually read Godel's proof (or better yet, one of the modern explanations thereof) before dismissing it as "trivial" or the sentences involved as "illogical." I think we've temporarily reached the point of diminishing returns, so I'm going to bow out for now, but let me end with one exercise: if you really think "$\exists x(x\not=x)$" is a formulation of the Liar, then you should be able to deduce a contradiction in $PA$ from it or its negation. (cont'd) $\endgroup$ – Noah Schweber Jun 13 '16 at 18:06
    • 1
      $\begingroup$ @RobertFrost Those two statements certainly aren't the same - "$\exists x(x=5)$" is certainly a true statement about the natural numbers, but whether "$x=5$" is true or not depends on what variable assignment you use (google "free variable"). Finally, I'm not sure what you mean by "every statement inherently declares its own existence." I would strongly suggest that you try to make all the notions you're using here - "illogical," "inherently declares," etc. - precise. Mathematical logic is, like the rest of mathematics, an exact subject. $\endgroup$ – Noah Schweber Jun 13 '16 at 18:43

    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.