Could Gödel’s incompleteness theorem be circumvented with a quine?

As you all probably know, Gödel’s incompleteness theorem states, that it will never be possible for mathematics to prove its own correctness.
Mainly because that proof would be part of mathematics too, and hence need proving itself. And that leads to an infinite loop in logic.

But I realized that a quine, as in, a program that can output itself, seems to circumvent that problem: It really CAN output ALL of itself.

So I’m wondering, if the general tricks used in quines might be usable to “solve” that problem in mathematics too. At least to arrive at a different problem that might be solvable in a different way.
And if not, then I’m curious why exactly not, so I can lay this to rest in my head.

• Quines are used to prove Gödel's incompleteness theorem. Mar 13, 2022 at 13:52
• "Mainly because that proof would be part of mathematics too, and hence need proving itself. And that leads to an infinite loop in logic." That's not an accurate summary of the incompleteness theorem. You should read the proof itself, rather than informal summaries of the proof/result. Mar 13, 2022 at 18:50
• Ironically, the fundamental principle of quines --- diagonalization --- is exactly the same idea used to prove Gödel's theorem. Mar 15, 2022 at 8:08
• A better intuitive summary of Gödel's incompleteness theorem would be: "A theory is either so small that it cannot express enough theorems, or it is so powerful that it can express too many theorems, including theorems that it cannot prove."
– Stef
Mar 15, 2022 at 10:23
• @NoahSchweber: Sure… If you translate it from mathematics to human for me… ;) … I have found that I can understand even the hardest things in mathematics easily, if they are properly visualized (e.g. by 3blue1brown). The problem is that I can’t translate them unless I already know them. … Seriously, I don’t even expect visualization. I would be happy if mathematicians would learn a core principle in programming: Use Descriptive Identifiers! ^^ … As long as you guys keep insisting on using symbols that are impossible to even look up, I’m forced to rely on “informal” summaries.
– anon
Jul 9, 2022 at 19:49

Here is the proof of Gödel's incompleteness theorem, in a nutshell, for a theory $$T$$. We construct a sentence $$\Pi$$ which states that "$$T$$ proves that $$\Pi$$ is false". The sentence mentions itself, just like a quine.

If $$T$$ proves $$\Pi$$ then $$T$$ also proves that $$\Pi$$ is false, and so $$T$$ cannot be sound. If $$T$$ proves that $$\Pi$$ is false then $$\Pi$$ is true, and so again $$T$$ is not sound.

• And the theory T just needs to be strong enough to express the sentence P. The fact that you can write it down is enough for Gödel’s theorem to hit you. (Although writing it down is not quite as trivial, but not particularly difficult either). Mar 14, 2022 at 8:45
• Yuval, the way you express the Godel sentence is not intrinsically wrong, but it is the reverse of the usual convention: your sentence $\Pi$ is false, but such that $\lnot\Pi$ is not provable, but it's usual to express the result in terms of a sentence that is true-but-not-provable. Rather than edit your answer to negate everything, I wrote another answer based on yours, and added a remark or two of my own. Mar 15, 2022 at 12:40
• What is a "theory" in this context? Mar 16, 2022 at 0:17
• @DifferentialCovariance A system of mathematical reasoning. Mar 16, 2022 at 4:21
• Mike, completeness means there is either a proof that P is false, or a proof that P is true. If not P is not provable, then the theory is incomplete, or P is provable. Mar 16, 2022 at 7:21

Mainly because that proof would be part of mathematics too, and hence need proving itself. And that leads to an infinite loop in logic.

No, that's not the flaw identified by Gödel’s incompleteness theorem. As you note, that can be addressed with a quine. Quines are, loosely speaking, the cause of the theorem, not the solution: if you can create a statement that outputs itself, then you can also create a statement that outputs a negation of its provability. That is, you have a statement that declares that it can't be proven. If the statement can be proven, then it's false, so you've proven a false statement, which means that your system is inconsistent. If it can't be proven, then the statement is true (since what the statement consists of is the declaration that it can't be proven), thus it is a statement that is true, but can't be proven to be true. Therefore, every sufficiently sophisticated mathematical system is either inconsistent or contains statements that are true, but can't be proven.

[This is just my attempt to make Yuval Filmus's answer more mathematically accurate. Feel free to combine the answers, delete this one, or whatever seems best.]

Here is the proof of Gödel's incompleteness theorem, in a nutshell, for a theory $$T$$. We construct a sentence $$\Pi$$ which states that "There is no proof of $$\Pi$$ in $$T$$". The sentence mentions itself, just like a quine, and exploits the fact that formulas and proofs can be encoded as numbers in such a way that the property of being a proof of a formula is expressible in arithmetic terms.

If $$T$$ is sound and proves $$\Pi$$ then $$\Pi$$ is true, so $$T$$ does not prove $$\Pi$$, a contradiction. We conclude that $$T$$ does not prove $$\Pi$$; but then $$\Pi$$ is indeed true, and $$T$$ provides no proof of it.

Mainly because that proof would be part of mathematics too, and hence need proving itself. And that leads to an infinite loop in logic.

This is not the reason why Gödel’s incompleteness theorem proves that no set of rules (Mathematics, C++, Philosophy, Law, Religion etc.) can prove its own correctness. The actual reason is kind of a generalization of The Halting Problem in computing.

Gödel proved that for any set of rules you can formulate a statement (eg. program) that breaks the rules. Therefore it is impossible to fix rules (programming language, Mathematics etc.) to make them unbreakable (always true/applicable for all statements/programs). The Halting Problem can actually be interpreted as a reformulation of Gödel's Incompleteness Theorem in the context of Turing Machines/Computers (indeed there are papers written on the topic).

Whereas the Halting Problem proves that it is not always possible to write an algorithm that always generate a solution (proving that some problems are undecidable), the Incompleteness Theorem proves that it is not always possible to prove that all the rules in your system (Mathematics, C++, etc) can be proven to be always true.

But in practice this is not a problem. Just as we can write useful software even when some problems cannot be solved by software we can do useful problem solving even if we don't use all statements mathematics can produce.

One candidate for the incompleteness theorem may or may not be the twin prime conjecture, which states that there are infinitely many twin prime numbers (couples of prime numbers differing by 2). To this day, it could not be proved, which means that it is either false and we were not able to disprove it yet, or it may be true and we have not found a valid proof for it yet, or it may be one of those statements that Gödel talked about - that is, a statement that is true but unprovable.

• "no set of rules [...] can prove its own correctness" This is not right. You mean: no set of rules strong enough to express arithmetic can prove its own correctness. There are many weak sets of rules that can prove their own consistency (the empty set of rules, for example!). Mar 15, 2022 at 17:35
• One "twin" missing. The twin prime number conjecture states there are infinitely many twin prime numbers. That there are infinitely many prime numbers is proven in Euclid's theorem, I think.
– Jan
Mar 15, 2022 at 23:41