Relationship between computational undecidability and axiomatic undecidability

Question

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

Answer 1

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!