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.