It shows that the sentences of the form $\forall x, \neg Dem(x,sub(n,y,n))$ are true but unprovable, where $y$ is the Godel number mapped to the symbol $Y$ in arithmetic language, and $n$ is the Godel number of the sentence $\forall x, \neg Dem(x, sub(Y,y,Y))$
Suppose for some $y$, the sentence $\forall x, \neg Dem(x,sub(n,y,n))$ has the Godel number 1000. Then following is a true but unprovable property of the number 1000:
"The number 1000 can never be at the end of a sequence of natural numbers $x_{k}, k=1,2,3,….n$, such that every $x_{k}$ is either a Godel number of an axiom or of a sentence logically deducible from the axioms."
Properties like this, however, are a very narrow class of the properties of natural numbers. Is this even an arithmetic property? I'm asking this because this property does not involve operations of arithmetic like addition, multiplication. Instead, it involves decoding the number to a language of symbols and using rules of logical deduction. Arithmetic properties are something like '$\forall x, 10x\neq 5, x\in Z$'
Even if this is accepted as an arithmetic property, it is a very narrow class of arithmetic properties. These properties are also dependent on the map that we use for the one-to-one correspondence between integers and symbols (there are multiple maps possible). Does the Incompleteness theorem say anything about non- self referential properties of numbers?
Best Answer
As others have said, the very distinction you're trying to draw is fuzzy to the point of meaninglessness, and there are very natural examples of undecidable (with respect to any of the usual theories) sentences. However, there's a very nice fact which hasn't been mentioned yet and I think puts the final nail in the coffin:
It's hard to get more concrete and arithmetic than Diophantine equations!
Here as usual "reasonable" means "computably axiomatizable, consistent, and extending $Q$" (although even that is overkill: we can replace "extending $Q$" with "interpreting $R$" or even weaker hypotheses - see here, Section $4$). The result above is a more-or-less immediate consequence of the proof of the MRDP theorem: basically, we can assign to $T$ a Diophantine equation $\mathcal{E}_T$ such that putative solutions to $\mathcal{E}_T$ correspond to putative contradictions in $T$. Of course, the $\mathcal{E}_T$s so produced are truly god-awful, but they are honest-to-goodness Diophantine equations