Incomplete theory proving its incompleteness by a formula neither provable true nor false in the theory

Question

Would it be possible that an incomplete theory had a formula that proved its incompleteness, but that same formula belonged to the set of formulae of that theory that can't be proven true or false, so you could never prove it's incomplete in first place?

Answer 1

I'm assuming what you actually mean is,

Would it be possible that an incomplete theory had a formula that expressed its incompleteness, but that same formula belonged to the set of formulae of that theory that can't be proven true or false by that theory, so you could never prove it's incomplete in first place?

If so, the answer is, "yes, easily".

A boring way to see this is to select a theory so weak that it proves hardly anything at all -- for example Robinson Arithmetic. It is just about strong enough that it's defensible to say that the standard (Gödelian) way of encoding statements about provability into the language of arithmetic is meaningful for it, but definitely not strong enough to prove interesting general statements about provability.

As a less boring example, your favorite foundational theory such as PA or ZFC will also be an example. Proving the theory to be incomplete would in particular prove it to be consistent, and we know from the second incompleteness theorem that PA or ZFC cannot prove their own consistency, unless they are in fact inconsistent.

Answer 2

In the presentations I have seen the proof of incompleteness is not in the base theory. We have a base theory, like Peano Arithmetic (PA), and we construct a sentence in the language of PA that we can argue outside of PA is undecidable inside of PA. That convinces us as observers that PA is incomplete.

The original Gödel proof constructed a predicate $Proof(x,y)$ that is true if $x$ is the number representing a proof of $y$. This predicate is primitive recursive, so (with great effort) can be made quantifier free. If we let $z$ be the number representing $0=S(0)$ (the formal version of $0=1$) the statement that PA is consistent can be represented as $\lnot \exists x Proof(x,z)$ because an inconsistent theory can prove anything it can express. PA does not prove this sentence undecidable. Outside of PA (often called in the metatheory) we can argue that if PA could prove $Con(PA)=\lnot \exists x Proof(x,z)$ it would be inconsistent. This is Gödel's second incompleteness theorem.