3

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

user93785
  • 31
  • 2
    A similar question is asked at http://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 06:41
  • https://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

1 Answers1

3

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!

Noah Schweber
  • 18,932