Connection between two notions of undecidability

Question

As far as I understand, there are two common notions of "undecidability" that I will call

• "Mathematical undecidability":="the statement can neither be proved nor disproved from the axioms", equivalently, it is true in some model and false in some other model, and
• "Algorithmic undecidability":="there is no algorithm that, for a given input, corretly decides yes/no". More formally, the possible inputs are ordered and the set of indices of true statements is not a recursive set.

If I'm (at least partially) right in the above, I would like to understand the link between those two notions. On wikipedia, I read

The connection between these two is that if a decision problem is undecidable (in the recursion theoretical sense) then there is no consistent, effective formal system which proves for every question A in the problem either "the answer to A is yes" or "the answer to A is no".

This is quite vaguely formulated.

Question:

Is it true that for every algorithmically undecidable problem, for some particular instance of the input, the statement is mathematically undecidable (using Peano arithmetic)?

Answer 1

If a problem is ALGORITHMICALLY undecideable (no algorithm can decide the statement for every input) , then it is undecideable in any sufficiently strong formal system. Otherwise you could program the rules of the formal system and decide the problem.

"Sufficiently strong" means : The representation theorem holds. This is already true for the peano axioms. So, there must be an instance for which PA can neither proof that it is true nor that it is false.

The representation theorem states that every computable function can be formalized in the system.

Answer 2

Here is an answer which is a bit closer to the quote from Wikipedia. If you have some property $\phi(n)$ in the language of PA and if, for every natural number constant $\overline{n}$, either PA proves $\phi(\overline{n})$ or PA disproves $\phi(\overline{n})$, then $\phi(n)$ is algorithmically decidable: given an input $\overline{n}$, enumerate proofs in PA until you find one that either proves $\phi(\overline{n})$ or disproves it. This is guaranteed to terminate by our assumption on $\phi$ and when it terminates we know whether $\phi(\overline{n})$ is true or not (because PA is sound).