Return to Answer

Here is another possible interpretation of the question. Let $p : \mathbb N \to \mathbb N$ be some function. To avoid "cheats", we will also say that we know each value $p(x)$. That is, for every numeral $x$ there exists a numeral $y$ such that we can prove in some sound theory (say ZFC) that $p(x) = y$. ZFC also knows that $p$ is a total function. Is it possible for ZFC to prove that a $p$ is computable without proving any specific turing machine computes it?

Well, $p$ is actually computable, for one. That is because the following algorithm computes $p$:

1. Given $x$, search for a proof of the form $p(x) = y$.
2. When such a proof is found, output $y$.

However, ZFC can not prove this algorithm is correct due to Gödel's incompleteness theorem. We have successfully eliminated all uncomputable problems for consideration though, as well as ones that just ask if some conjecture is true or false.

Let $p$ be a function that following function:

$p(x) \equiv 0$ if there is no contradiction in ZFC whose proof is shorter than $x$. Otherwise, $p(x) \equiv 1$ if the continuum hypothesis holds or $p(x) \equiv 2$ if its negation holds.

For each $x$, ZFC proves $p(x) = 0$, since it can exhaustively check for a contradiction. It also proves $p$ is total, since it is a well-formed total function. ZFC even proves that $p$ is computable. One of the following algorithms does the trick:

• Case 1, CH holds: Given x, search for a proof of a contradiction shorter than $x$. If found, output $0$. Otherwise, output $1$.
• Case 2, CH does not hold: search for a proof of a contradiction shorter than $x$. If found, output $0$. Otherwise, output $2$.

However, there is no particular turing machine $M$ which ZFC can proof computes $p$. If it did, then ZFC + CH would prove that the inconsistency of ZFC implies there is some $x$ for which $M(x) = p(x) = 1$. Since this is an arithmetical statement, ZFC + $\lnot$CH also proves it. It also proves that there is no $x$ for which $M(x) = 1$. Therefore, it can conclude that ZFC is consistient. This violates the fact that ZFC and ZFC + $\lnot$CH are equiconsistient. So there is no $M$ that ZFC claims can compute $p$.

So:

• ZFC proves $p(x) = 0$ for all numerals $x$.
• ZFC proves $p$ is total.
• ZFC proves $p$ is computable.
• There is no turing machine $M$ that ZFC proves computes $p$.

So I guess an algorithm for $p$ would count as unknowable algorithm as far as ZFC is concerned. The algorithm is "given $x$, output $0$", btw. $p$ can probably be adapted to work for other formal systems as well, or even to work for humans (although you could not actually prove any theorems in the human case, because, well, humans).

Here is another possible interpretation of the question. Let $p : \mathbb N \to \mathbb N$ be some function. To avoid "cheats", we will also say that we know each value $p(x)$. That is, for every numeral $x$ there exists a numeral $y$ such that we can prove in some sound theory (say ZFC) that $p(x) = y$. ZFC also knows that $p$ is a total function. Is it possible for ZFC to prove that a $p$ is computable without proving any specific turing machine computes it?

Well, $p$ is actually computable, for one. That is because the following algorithm computes $p$:

1. Given $x$, search for a proof of the form $p(x) = y$.
2. When such a proof is found, output $y$.

However, ZFC can not prove this algorithm is correct due to Gödel's incompleteness theorem. We have successfully eliminated all uncomputable problems for consideration though, as well as ones that just ask if some conjecture is true or false.

Let $p$ be a function that following function:

$p(x) \equiv 0$ if there is no contradiction in ZFC whose proof is shorter than $x$. Otherwise, $p(x) \equiv 1$ if the continuum hypothesis holds or $p(x) \equiv 2$ if its negation holds.

For each $x$, ZFC proves $p(x) = 0$, since it can exhaustively check for a contradiction. It also proves $p$ is total, since it is a well-formed total function. ZFC even proves that $p$ is computable. One of the following algorithms does the trick:

• Case 1, CH holds: Given x, search for a proof of a contradiction shorter than $x$. If found, output $0$. Otherwise, output $1$.
• Case 2, CH does not hold: search for a proof of a contradiction shorter than $x$. If found, output $0$. Otherwise, output $2$.

However, there is no particular turing machine $M$ which ZFC can proof computes $p$. If it did, then ZFC + CH would prove that the inconsistency of ZFC implies there is some $x$ for which $M(x) = 1$. Since this is an arithmetical statement, ZFC + $\lnot$CH also proves it. It also proves that there is no $x$ for which $M(x) = 1$. Therefore, it can conclude that ZFC is consistient. This violates the fact that ZFC and ZFC + $\lnot$CH are equiconsistient. So there is no $M$ that ZFC claims can compute $p$.

So:

• ZFC proves $p(x) = 0$ for all numerals $x$.
• ZFC proves $p$ is total.
• ZFC proves $p$ is computable.
• There is no turing machine $M$ that ZFC proves computes $p$.

So I guess an algorithm for $p$ would count as unknowable algorithm as far as ZFC is concerned. The algorithm is "given $x$, output $0$", btw. $p$ can probably be adapted to work for other formal systems as well, or even to work for humans (although you could not actually prove any theorems in the human case, because, well, humans).

Here is another possible interpretation of the question. Let $p : \mathbb N \to \mathbb N$ be some function. To avoid "cheats", we will also say that we know each value $p(x)$. That is, for every numeral $x$ there exists a numeral $y$ such that we can prove in some sound theory (say ZFC) that $p(x) = y$. ZFC also knows that $p$ is a total function. Is it possible for ZFC to prove that a $p$ is computable without proving any specific turing machine computes it?

Well, $p$ is actually computable, for one. That is because the following algorithm computes $p$:

1. Given $x$, search for a proof of the form $p(x) = y$.
2. When such a proof is found, output $y$.

However, ZFC can not prove this algorithm is correct due to Gödel's incompleteness theorem. We have successfully eliminated all uncomputable problems for consideration though, as well as ones that just ask if some conjecture is true or false.

Let $p$ be a function that following function:

$p(x) \equiv 0$ if there is no contradiction in ZFC whose proof is shorter than $x$. Otherwise, $p(x) \equiv 1$ if the continuum hypothesis holds or $p(x) \equiv 2$ otherwise.

For each $x$, ZFC proves $p(x) = 0$, since it can exhaustively check for a contradiction. It also proves $p$ is total, since it is a well-formed total function. ZFC even proves that $p$ is computable. One of the following does the trick:

• Case 1, CH holds: Given x, search for a proof of a contradiction shorter than $x$. If found, output $0$. Otherwise, output $1$.
• Case 2, CH does not hold: search for a proof of a contradiction shorter than $x$. If found, output $0$. Otherwise, output $2$.

However, there is no particular turing machine $M$ which ZFC can proof computes $p$.

So:

• ZFC proves $p(x) = 0$ for all numerals $x$.
• ZFC proves $p$ is total.
• ZFC proves $p$ is computable.
• There is no turing machine $M$ that ZFC proves computes $p$.

So I guess an algorithm $p$ would count as unknowable algorithm as far as ZFC is concerned. The algorithm is "given $x$, output $0$", btw. $p$ can probably be adapted to work for other formal systems as well, or even to work for humans (although you could not actually prove any theorems in the human case, because, well, humans).

Here is another possible interpretation of the question. Let $p : \mathbb N \to \mathbb N$ be some function. To avoid "cheats", we will also say that we know each value $p(x)$. That is, for every numeral $x$ there exists a numeral $y$ such that we can prove in some sound theory (say ZFC) that $p(x) = y$. ZFC also knows that $p$ is a total function. Is it possible for ZFC to prove that a $p$ is computable without proving any specific turing machine computes it?

Well, $p$ is actually computable, for one. That is because the following algorithm computes $p$:

1. Given $x$, search for a proof of the form $p(x) = y$.
2. When such a proof is found, output $y$.

However, ZFC can not prove this algorithm is correct due to Gödel's incompleteness theorem. We have successfully eliminated all uncomputable problems for consideration though, as well as ones that just ask if some conjecture is true or false.

Let $p$ be a function that following function:

$p(x) \equiv 0$ if there is no contradiction in ZFC whose proof is shorter than $x$. Otherwise, $p(x) \equiv 1$ if the continuum hypothesis holds or $p(x) \equiv 2$ if its negation holds.

For each $x$, ZFC proves $p(x) = 0$, since it can exhaustively check for a contradiction. It also proves $p$ is total, since it is a well-formed total function. ZFC even proves that $p$ is computable. One of the following algorithms does the trick:

• Case 1, CH holds: Given x, search for a proof of a contradiction shorter than $x$. If found, output $0$. Otherwise, output $1$.
• Case 2, CH does not hold: search for a proof of a contradiction shorter than $x$. If found, output $0$. Otherwise, output $2$.

However, there is no particular turing machine $M$ which ZFC can proof computes $p$. If it did, then ZFC + CH would prove that the inconsistency of ZFC implies there is some $x$ for which $M(x) = p(x) = 1$. Since this is an arithmetical statement, ZFC + $\lnot$CH also proves it. It also proves that there is no $x$ for which $M(x) = 1$. Therefore, it can conclude that ZFC is consistient. This violates the fact that ZFC and ZFC + $\lnot$CH are equiconsistient. So there is no $M$ that ZFC claims can compute $p$.

So:

• ZFC proves $p(x) = 0$ for all numerals $x$.
• ZFC proves $p$ is total.
• ZFC proves $p$ is computable.
• There is no turing machine $M$ that ZFC proves computes $p$.

So I guess an algorithm for $p$ would count as unknowable algorithm as far as ZFC is concerned. The algorithm is "given $x$, output $0$", btw. $p$ can probably be adapted to work for other formal systems as well, or even to work for humans (although you could not actually prove any theorems in the human case, because, well, humans).

Here is another possible interpretation of the question. Let $p : \mathbb N \to \mathbb N$ be some function. To avoid "cheats", we will also say that we know each value $p(x)$. That is, for every numeral $x$ there exists a numeral $y$ such that we can prove in some sound theory (say ZFC) that $p(x) = y$. ZFC also knows that $p$ is a total function. Is it possible for ZFC to prove that a $p$ is computable without proving any specific turing machine computes it?

Well, $p$ is actually computable, for one. That is because the following algorithm computes $p$:

1. Given $x$, search for a proof of the form $p(x) = y$.
2. When such a proof is found, output $y$.

However, ZFC can not prove this algorithm is correct due to Gödel's incompleteness theorem. We have successfully eliminated all uncomputable problems for consideration though, as well as ones that just ask if some conjecture is true or false.

Let $p$ be a function that following function:

$p(x) \equiv 0$ if there is no contradiction in ZFC whose proof is shorter than $x$. Otherwise, $p(x) \equiv 1$ if the continuum hypothesis holds or $p(x) \equiv 2$ otherwise.

For each $x$, ZFC proves $p(x) = 0$, since it can exhaustively check for a contradiction. It also proves $p$ is total, since it is a well-formed total function. ZFC even proves that $p$ is computable. One of the following does the trick:

• Case 1, CH holds: Given x, search for a proof of a contradiction shorter than $x$. If found, output $0$. Otherwise, output $1$.
• Case 2, CH does not hold: search for a proof of a contradiction shorter than $x$. If found, output $0$. Otherwise, output $2$.

However, there is no particular turing machine $M$ which ZFC can proof computes $p$. If it did, ZFC could prove its own consistency (which would violate Gödel's incompleteness theorem) as follows:

$M$ computes $p$. Also, ZFC proves this. Assume there is some $x$ for which $M(x) \neq 0$. Then ZFC can prove this by simulating $M$ on $x$. (For all that I, ZFC, know, ZFC might also prove $M(x) = 0$. This is not a problem.) ZFC plus the continuum hypothesis proves $M(x) = p(x) = 1$. ZFC plus the negation of the continuum hypothesis proves $M(x) = p(x) = 2$. This, however, is a contradiction, since the continuum hypothesis does not add any arithmetical consequences to ZFC. So $\forall x. p(x) = M(x) = 0$, which implies ZFC has no contradictions, and is therefore consistient.

So:

• ZFC proves $p(x) = 0$ for all numerals $x$.
• ZFC proves $p$ is total.
• ZFC proves $p$ is computable.
• There is no turing machine $M$ that ZFC proves computes $p$.

So I guess an algorithm $p$ would count as unknowable algorithm as far as ZFC is concerned. The algorithm is "given $x$, output $0$", btw. $p$ can probably be adapted to work for other formal systems as well, or even to work for humans (although you could not actually prove any theorems in the human case, because, well, humans).

Here is another possible interpretation of the question. Let $p : \mathbb N \to \mathbb N$ be some function. To avoid "cheats", we will also say that we know each value $p(x)$. That is, for every numeral $x$ there exists a numeral $y$ such that we can prove in some sound theory (say ZFC) that $p(x) = y$. ZFC also knows that $p$ is a total function. Is it possible for ZFC to prove that a $p$ is computable without proving any specific turing machine computes it?

Well, $p$ is actually computable, for one. That is because the following algorithm computes $p$:

1. Given $x$, search for a proof of the form $p(x) = y$.
2. When such a proof is found, output $y$.

However, ZFC can not prove this algorithm is correct due to Gödel's incompleteness theorem. We have successfully eliminated all uncomputable problems for consideration though, as well as ones that just ask if some conjecture is true or false.

Let $p$ be a function that following function:

$p(x) \equiv 0$ if there is no contradiction in ZFC whose proof is shorter than $x$. Otherwise, $p(x) \equiv 1$ if the continuum hypothesis holds or $p(x) \equiv 2$ otherwise.

For each $x$, ZFC proves $p(x) = 0$, since it can exhaustively check for a contradiction. It also proves $p$ is total, since it is a well-formed total function. ZFC even proves that $p$ is computable. One of the following does the trick:

• Case 1, CH holds: Given x, search for a proof of a contradiction shorter than $x$. If found, output $0$. Otherwise, output $1$.
• Case 2, CH does not hold: search for a proof of a contradiction shorter than $x$. If found, output $0$. Otherwise, output $2$.

However, there is no particular turing machine $M$ which ZFC can proof computes $p$.

So:

• ZFC proves $p(x) = 0$ for all numerals $x$.
• ZFC proves $p$ is total.
• ZFC proves $p$ is computable.
• There is no turing machine $M$ that ZFC proves computes $p$.

So I guess an algorithm $p$ would count as unknowable algorithm as far as ZFC is concerned. The algorithm is "given $x$, output $0$", btw. $p$ can probably be adapted to work for other formal systems as well, or even to work for humans (although you could not actually prove any theorems in the human case, because, well, humans).