Context: I've been reading through the Dover English translation of Godel's paper "On Formally Undecidable Propositions of Principia Mathematica and Related Systems".
It seems the key to producing Godel formulas is the generalization operation, such as the formula "17 Gen r". Without generalization, it seems impossible to create an unprovable formula.
Looking through the axioms and proof schema earlier in the paper, I did not see any that would allow introduction of generalization. This suggests to me that many generalized formula are unprovable in Godel's system in the sense that any proof of a generalized formula would require another generalized formula as a premise. Assuming there's no infinite regress, then working backwards means we end up with a primal generalized formula which has no proof, since there is no precursor generalized formula. Unless there is a "super generalized formula" that can prove most other generalized formula, which seems implausible, this means there are loads and loads of unprovable generalized formula.
In which case, "17 Gen r" is not particularly notable in being unprovable, except for the fact that we can interpret it as saying "this formula is unprovable" and consequently more formally prove its unprovability.
Am I missing something here?