Relationship between computational undecidability and axiomatic undecidability

On surface, these seem two completely different class of problems. One class represent statements which can't be proved or disproved in an axiomatic theory. For example

One can write down a concrete polynomial P∈Z[x1,...x9] such that the statement "there are integers m1,...,m9 with P(m1,...,m9)=0" can neither be proven nor disproven in ZFC

Other class represent problems which can't be computed within fixed time. For example

The mortal matrix problem: determining, given a finite set of n × n matrices with integer entries, whether they can be multiplied in some order, possibly with repetition, to yield the zero matrix.

Is there any definite relation(with Curry-Howard isomorphism) between them, like one class being subset of other or both being the same

• A similar question is asked at mathoverflow.net/q/130789/1946, with several good answers. – Joel David Hamkins Jun 12 '16 at 10:40
• Thanks. I tried to search for any similar question, but could not find any. This question is clearly a duplicate. – user93785 Jun 12 '16 at 14:05
• Amazing, the statement about the polynomial $p\in\mathbb{Z}[x_1,\ldots,x_9]$ that you mention! Could you give a reference about it? – Dominic van der Zypen Jun 15 '16 at 6:41
• projecteuclid.org/download/pdf_1/euclid.bams/1183547548 explicitly constructs a undecidable equation with 21 variable and also give reference to 9 variable case that was mentioned in the question . – user93785 Jun 15 '16 at 16:40

Certainly if $\{x\in\mathbb{N}: P(x)\}$ is incomputable, then - for any computable and true set of axioms $T$ - there will be some (in fact, infinitely many) $n$ such that $T$ neither proves nor disproves "$P(n)$." This is simply because we can effectively enumerate the theorems of $T$: if $T$ decided each instance of $P(n)$ (and did so correctly - hence the "true" above), then we could compute $\{x: P(x)\}$.
Conversely, individual instances of undecidable problems don't necessarily translate to incomputable sets - for example, $ZFC$ doesn't prove or disprove "$2^{\aleph_0}=\aleph_1$," but it's not really clear how to translate this into a decision problem - but in examples like the Diophantine equations one, there's a bit more structure: what's actually proved is that for every computable and true set of axioms $T$, there is some polynomial $P$ in finitely many (seven?) variables such that $T$ neither proves nor disproves "$P$ has a zero." These "schematic" instances of undecidability do tend to have an underlying incomputable set! Specifically, we usually have an effective procedure for passing from a computable true $T$ to an instance of the problem which $T$ doesn't decide (for example, this is true for Diophantine equations). In that case, the set of instances which have the desired property - e.g. Diophantine equations with zeroes - is incomputable, since otherwise we could form a silly set of axioms which is computable and decides each instance of the problem!
• Side comment: much less than $T$ being true is needed above, but that's a separate question. – Noah Schweber Jun 12 '16 at 6:08