This question is related to Godel's incompleteness theorem, which states that no sufficiently complex formal system can be both consistent and complete.

Is it possible to add axioms to a formal system $P$ to generate a new formal system $P'$ such that $P'$ is consistent and all unprovable statements in $P$ have proof in $P'$? (The way that this would circumvent Godel's incompleteness theorem is that there would be new unprovable statements in $P'$ that weren't in $P$).

For example, primitive recursive arithmetic is a formal system in which everything is provable, however it can only express a subset of the theories that can be expressed by Peano arithmatic. In the same way, $P'$ would be more expressive than $P$, and primitive recursive arithmatic represents a trivial case of $P$ where the above question is true. I am interested in $P$ where there exist unprovable statements.

  • 3
    $\begingroup$ For the parenthesis at the end: How could the addition of new axioms possibly make something unprovable that wasn't already? $\endgroup$ Jan 24, 2018 at 0:48
  • $\begingroup$ $P'$ would be more expressive than $P$ in the same way that Peano arithmetic is more expressive than primitive recursive arithmetic. $\endgroup$ Jan 24, 2018 at 0:55
  • $\begingroup$ How will you stop $P'$ from being able to solve the halting problem? $\endgroup$
    – DanielV
    Jan 24, 2018 at 1:02

1 Answer 1


Adding more expressivity is not going to help you if Gödel's incompleteness theorem applies to $P$.

One of the premises of Gödel's theorem is that the language of the theory can express a certain amount of arithmetic sentences (level $\Pi^0_1$ in the arithmetical hierarchy, if I recall correctly).

If we add more expressivity to $P$, producing $P'$ with a finite number of consistent additional axioms, then Gödel's theorem still applies to $P'$. But the $P'$-undecidable sentence that the theorem produces will be one of the arithmetic sentences that already $P$ could express.

So $P'$ will have an undecidable sentence that was in the language of $P$.

  • $\begingroup$ What if $P'$ also extends the language of $P$ with new relation or function symbols? (For example, maybe $P'$ adds a function symbol which represents an oracle on "$n$ is an encoding of a true statement" and then you add axioms that the oracle gives consistent answers. Though I haven't thought that through and there could very well be subtle issues with trying to do that.) $\endgroup$ Jan 24, 2018 at 1:11
  • 1
    $\begingroup$ @DanielSchepler: Extending the language is exactly what I'm showing doesn't help. (Note that the question title stipulated a finite number of new axioms; I dare you to attempt to specify a truth oracle for arithmetic within that constraint). $\endgroup$ Jan 24, 2018 at 1:14

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.