Return to Question

• Regarding Joel's answer: this argument would be a striking satisfactory answer if it is proved that knowing the value of $N$ is indecidable in ZFC. Maybe one can work out an example where $\pi$ is replaced by some other real number.

• Regarding Goldstern's answer (and subsequent comment/answers): I don't so much think that the argument is a cheat than it does not answer my edited question (edit made after the initial answer). My point is the following. Either some open question $Q$ is decidable in ZFC, in which case we all agree that the program "Yes" or the program "No" answers $Q$, but by inspection of the programs we can decide which one performs the required task once we know which answer is a fact, which is not a formal issue anymore. Either $Q$ is indecidable in ZFC and we cannot prove, in ZFC, the existence of an algorithm answering it (though I'm not sure of this part of my argument). Now if we attach $Q$ to our axioms set then we are back to the previous case, were answering $Q$ has become explicitely tautological. So I believe Goldstern's example does not meet the requirement of my question.

• Timothy's answer is great since it offers a very nice comprehensive summary of the issue as I perceive it. If the unofficial answer to my question is that pessimistic statement, then let it be. The sloppy mathematician in me is perfectly happy with matters as they are ;)

To conclude, I think I should accept Peter Shor's answer, since he gives an example which, as I understand it, answers my query. I'll do that in a little while.

• Regarding Joel's answer: this argument would be a striking satisfactory answer if it is proved that knowing the value of $N$ is indecidable in ZFC. Maybe one can work out an example where $\pi$ is replaced by some other real number.

• Regarding Goldstern's answer (and subsequent comment/answers): I don't so much think that the argument is a cheat than it does not answer my edited question (edit made after the initial answer). My point is the following. Either some open question $Q$ is decidable in ZFC, in which case we all agree that the program "Yes" or the program "No" answers $Q$, but by inspection of the programs we can decide which one performs the required task once we know which answer is a fact, which is not a formal issue anymore. Either $Q$ is indecidable in ZFC and we cannot prove, in ZFC, the existence of an algorithm answering it (though I'm not sure of this part of my argument). Now if we attach $Q$ to our axioms set then we are back to the previous case, were answering $Q$ has become explicitely tautological. So I believe Goldstern's example does not meet the requirement of my question.

• Timothy's answer is great since it offers a very nice comprehensive summary of the issue as I perceive it. If the unofficial answer to my question is that pessimistic statement, then let it be. The sloppy mathematician in me is perfectly happy with matters as they are ;)

  To conclude, I think I should accept Peter Shor's answer, since he gives an example which, as I understand it, answers my query. I'll do that in a little while.

(Final) edit: I thank everybody who took the pain to answer my rookie's question... I would like to formulate some comments regarding the (legitimate) objections that has been raised. First we may assume that the formal system is ZFC, in order to fix ideas. My question was not about "mass problems" (although the examples presented below really are interesting), I was rather asking about a specific task, so it relates more to undecidability problems, as was pointed out by Mark Sapir.

Actually MyFavouriteProblem concerns effective computability of holomorphic dynamical systems satisfying MyFavoriteProperty, which were known to exists by some "abstract" argument and for which I gave a more "constructive" proof. It is doubtlessly a practical improvement (my PC can do the computing), but I wanted to know if from a theoretical point of view some progress really has been made (actually to settle a friendly argument with a colleague of mine). So the starting point to this question lies in algorithms performing computations with arbitrary floating-point precision on complex numbers, understood as Taylor coefficients of power series (needs some infinite memory here, I'm afraid, but I don't think it really matters).

• Regarding Joel's answer: this argument would be a striking satisfactory answer if it is proved that knowing the value of $N$ is indecidable in ZFC. Maybe one can work out an example where $\pi$ is replaced by some other real number.

• Regarding Goldstern's answer (and subsequent comment/answers): I don't so much think that the argument is a cheat than it does not answer my edited question (edit made after the initial answer). My point is the following. Either some open question $Q$ is decidable in ZFC, in which case we all agree that the program "Yes" or the program "No" answers $Q$, but by inspection of the programs we can decide which one performs the required task once we know which answer is a fact, which is not a formal issue anymore. Either $Q$ is indecidable in ZFC and we cannot prove, in ZFC, the existence of an algorithm answering it (though I'm not sure of this part of my argument). Now if we attach $Q$ to our axioms set then we are back to the previous case, were answering $Q$ has become explicitely tautological. So I believe Goldstern's example does not meet the requirement of my question.

• Timothy's answer is great since it offers a very nice comprehensive summary of the issue as I perceive it. If the unofficial answer to my question is that pessimistic statement, then let it be. The sloppy mathematician in me is perfectly happy with matters as they are ;)

To conclude, I think I should accept Peter Shor's answer, since he gives an example which, as I understand it, answers my query. I'll do that in a little while.