This page is keyboard accessible:
• Use Tab, Shift + Tab keys to traverse the main menu. To enter a sub-menu use the Right Arrow key. To leave a sub-menu use the Left Arrow or the Escape key.
• The Enter or the Space key opens the active menu item.
• To skip the menu and move to the main content, press Tab after the page loads to reveal a skip button.
• To get back to the top of the page anytime, press the Home key.
• For more information, click here: Accessibility   Close this tip.

Note: Full functionality of this web page requires JavaScript to be enabled in your browser.

True but unprovable?

Gödel’s ‘true’ but unprovable sentence

There are people who reject any notion that the ‘unprovable’ formula (unprovable by the formal system) given by Gödel’s incompleteness proof can in any way be considered to be ‘true’.


But in fact:

  • many professional mathematicians who believe that Gödel’s proof is correct also believe that Gödel’s ‘unprovable’ statement is shown to be true by Gödel’s proof – for example, Roger Penrose, Douglas Hofstadter, Gregory Chaitin, George Boolos, Elliott Mendelson.
  • Gödel himself believed that his proof showed the ‘unprovable’ statement to be true. In the preface of his proof he states (Meltzer’s translation):

    “From the remark that [the unprovable statement] asserts its own unprovability, it follows at once that [the unprovable statement] is correct, since [the unprovable statement] is certainly unprovable (because undecidable). So the proposition which is undecidable in the system PM yet turns out to be decided by meta-mathematical considerations.”


The rejection of the interpretation that the ‘unprovable’ formula given by Gödel’s proof can in any way be considered to be ‘true’ is a rather fashionable notion in some circles. The roots of this interpretation can be traced to an inordinate desire to avoid any implication that Gödel’s proof gives rise to a contradiction. It only arose more than 30 years after the publication of Gödel’s proof and was conceived as a response to the publication of a paper Minds, Machines and Gödel by J. R. Lucas, which claimed that Gödel’s proof showed that there must be an inherent difference between minds and machines (see the page Gödel, Minds, and Machines for links to the continuing debate that has arisen over this issue).


That idea is rather disturbing to those who think that the physical evidence shows that minds are in principle no different to machines. And so, in order to avoid the conclusion that there must be a contradiction somewhere, a way had to be devised to get round this difficulty.


The argument thus devised has been presented in several ways, but the essence of the claim is twofold:

  • that Gödel’s proof only asserts a conditional statement:

    “If the formal system is consistent, then there is a formula of the formal system, which is not provable by the formal system, but it is true.”

  • that it cannot be assumed that there is any consistent formal system, so we cannot assert that Gödel’s unprovable statement for any formal system is ‘true’ – because that would mean we were assuming that the formal system is consistent.


Cherry picking of mathematical assumptions

The fallacy in the above argument should be obvious:


While these persons insist that Gödel’s proof cannot show the unprovable statement to be ‘true’, they are nevertheless at the same time insisting that Gödel’s proof is correct. And by doing so they are assuming the language that Gödel used to state his proof in is itself consistent. For convenience we will call this language GPL.


Now, guess what fundamental core of number theory is used in Gödel’s proof language GPL? Basically, the answer is:


Sufficient recursive number theory to be able to create a formula of number theory that Gödel interprets as meaning:

There is a proof of a certain formula of the formal system.


And guess what fundamental core of number theory a formal system must have in order that Gödel’s proof is applicable to it?

Yes, you’re right. Unsurprisingly, it is:


Sufficient recursive number theory to be able to create a formula of number theory that Gödel interprets as meaning:

There is a proof of a certain formula of the formal system.


Now, if you assume that the language GPL of Gödel’s proof is consistent, that means that you must be assuming that that fundamental core of number theory that Gödel’s proof uses is also consistent (since it includes that core of number theory). So if there is a formal system with that same fundamental core of number theory, you must also be assuming that this same core of number theory is consistent within the formal system (regardless of the consistency of the formal system as a whole).


So the nub of the argument that the ‘unprovable’ statement cannot be ‘true’ is this:

  1. We have a informal mathematical language GPL, which is the language in which Gödel’s proof is written.
  2. It is acceptable to assume that the part of Gödel’s informal language GPL that does not consist of that fundamental core of number theory is consistent (as well as assuming that the fundamental core of number theory is consistent).
  3. We have, in principle, any number of formal mathematical systems to which Gödel’s proof can be applied.
  4. It is forbidden to assume, for even one of these formal systems, that the part of the formal system that does not consist of that fundamental core of number theory is consistent.

Now, bear in mind that the language GPL of Gödel’s proof is natural language. It is not a fully defined language, and the axioms and rules of inference of that language are not fully defined. On the other hand, a formal language is fully defined, with no room for ambiguity or interpretation of the axioms and rules of that language.


And there is no reason why one cannot have formal systems that have the minimum of axioms that will provide that necessary fundamental core of number theory. Such a system may indeed be incomplete, but no-one has managed to explain why one should not be able to assume that it is consistent when that fundamental core of number theory that is the basis of the system can be assumed to be consistent.


So where is the logical basis for assuming that Gödel’s proof is more likely to be consistent than any formal system?


Answer – there isn’t any. This is simply a case of cherry picking the assumptions to give the desired outcome, and has no logical basis whatsoever. There is no logical basis for the assertion that there cannot be a valid interpretation that the ‘unprovable’ formula given by Gödel’s proof is also ‘true’ for at least one formal mathematical system.


Determining if a mathematical system is Inconsistent

It can be difficult to know if a mathematical system is consistent. There have been several instances where mathematical systems have been devised, and have been assumed to be consistent but which later have been shown to be inconsistent because contradictory self-referential statements could be created in that system.


The classic examples are:

  • Frege’s Set Theory
  • Church’s Foundations of Logic
  • Curry’s Combinatory Logic


Frege’s theory was shown to be inconsistent by Bertrand Russell (Footnote: See, for example Russell’s paradox entry in Stanford Encyclopedia.), and both Church’s and Curry’s systems were shown to be inconsistent by Kleene and Rosser. (Footnote: See, for example Kleene-Rosser paradox entry in Stanford Encyclopedia.) In all of these systems, an inconsistency was found because a contradictory self-referential statement could be created in the system.


Of course, those systems were devised many years ago, and you might suppose that mathematicians now know how to develop mathematical systems that are consistent. But no, contradictions have also been found in recently devised logical systems, including, perhaps surprisingly, systems developed for computer science. (Footnote: See, for example Contradictions in recent systems of logic entry in Stanford Encyclopedia.)


And then, of course, we have Gödel’s proof language GPL. This is assumed by supporters of Gödel’s proof to be entirely consistent, even though it is an informal language that is not clearly defined, and which creates a self-referential statement by a proof in which many detailed steps are simply skipped over and assumed to be of no importance, and assumed to be consistent.


‘True but unprovable’ and formal versions of Gödel’s proof

It’s rather interesting to look at the claim that the ‘unprovable’ formula cannot be considered to be ‘true’ along with claims that there can be formal versions of Gödel’s proof.


First of all, we note that the claim that the ‘unprovable’ formula cannot be considered to be ‘true’ necessarily involves the contention that there can be no assumption of consistency of the formal systems to which Gödel’s proof applies.


Secondly, we know that if Gödel’s proof language GPL is inconsistent, then it proves nothing. Therefore, if it is accepted that Gödel’s proof actually proves anything, that necessarily includes the assumption that Gödel’s proof language GPL is consistent.


But if Gödel’s proof language GPL could be stated in a formal language, and if the claim is that it does prove something, then that necessarily assumes that that formal proof language is consistent.


But, according to the above argument, we are not allowed to assume that any formal system that is the subject of Gödel’s proof is consistent.


And that would be saying that it is valid to assume the consistency of one particular formal language (the formal language that Gödel’s proof would be written in) and yet at the same time it is not permissible to assume that even one formal language is consistent.


And that is contradictory, isn’t it?


See Gödel’s contradiction for more on this.


What is ‘Truth’ anyway?

For more on what the notion of what ‘true’ might mean if it doesn’t mean ‘provable’ by some means, see The notion of ‘truth’.

section divider


section divider



Diverse opinions and criticisms are welcome, but messages that are frivolous, irrelevant or devoid of logical basis will be blocked. Difficulties in understanding the site content are usually best addressed by contacting me by e-mail. Note: you will be asked to provide an e-mail address - any address will do, it does not require verification. Your e-mail will only be used to notify you of replies to your comments - it will never be used for any other purpose and will not be displayed. If you cannot see any comments below, see Why isn’t the comment box loading?.

section divider

The Lighter Side


Paper on the diagonal proof

There is now a paper that deals with the matter of language and the diagonal proof, see On Considerations of Language in the Diagonal Proof.

section divider

Other recently added pages

The Myths of Platonism


Goodman’s Paradox


The Platonist Rod paradox


The Balls in the Urn Paradox


section divider

Lebesgue Measure

There is now a new page on a contradiction in Lebesgue measure theory.

section divider

Easy Footnotes

I found that making, adding or deleting footnotes in the traditional manner proved to be a major pain. So I developed a different system for footnotes which makes inserting or changing footnotes a doddle. You can check it out at Easy Footnotes for Web Pages (Accessibility friendly).

section divider

O’Connor’s “computer checked” proof

I have now added a new section to my paper on Russell O’Connor’s claim of a computer verified incompleteness proof. This shows that the flaw in the proof arises from a reliance on definitions that include unacceptable assumptions - assumptions that are not actually checked by the computer code. See also the new page Representability.

Previous Blog Posts

Moderate Platonism

Descartes’ Platonism

The duplicity of Mark Chu-Carroll

A John Searle Inanity

Man versus Machine

Fake News and Fake Mathematics

Ned Block’s Blockhead

Are we alone in the Universe?

Good Math, Bad Math?

Bishops Dancing with Pixies?

Artificial Intelligence

Cranks and Crackpots

The Chinese Room


For convenience, there are now two pages on this site with links to various material relating to Gödel and the Incompleteness Theorem


– a page with general links:

Gödel Links


– and a page relating specifically to the Gödel mind-machine debate:

Gödel, Minds, and Machines

Printer Friendly

All pages on this website are printer friendly, and will print the main content in a convenient format. Note that the margins are set by your browser print settings.

Note: for some browsers JavaScript must be enabled for this to operate correctly.


Comments on this site are welcome, please see the comment section.


Please note that this web site, like any other is a collection of various statements. Not all of this web site is intended to be factual. Some of it is personal opinion or interpretation.


If you prefer to ask me directly about the material on this site, please send me an e-mail with your query, and I will attempt to reply promptly.


Feedback about site design would also be appreciated so that I can improve the site.

Copyright © James R Meyer 2012 - 2018