# Can all unprovable statements in a given mathematical theory be determined with the addition of a finite number of new axioms?

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.

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

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$.
• 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.) Jan 24, 2018 at 1:11