It says it enables to associate a program with each proof in Zermelo-Fraenkel set theory. You can also, in principle associate a program to each value of the busy beaver function, or even uncountably many of them (for example for each value of the BB function a complex-valued function that based of the square of the value of the BB function as a constant in each of the complex-valued functions of each value). Even though you cannot compute the values of the busy beaver function.
That means you can associate programs to uncomputable functions, like the function of definition.
I can also associate a program to X = ?; for example rand(60). That however assumes that the natural number in question is a constant, which as I said above does not logically follow from the instruction of choosing one natural number. You can logically instruct something, and do something different. That is not a contradiction in terms of logic.
But as I said above that program would not compute X, it would merely be associated to X, which is a different notion. For example I can associate the BB function to X, but that does not make X computable, and indeed the opposite follows, as X could have the values of the BB function, which is proven to not be computable. So X could be not computable, and as it could be not computable, it is uncomputable in this context, as the question is if you can compute X without first defining it, which you cannot. Once you defined X=3, you can of course program a computer to deduce X=3, but that happens after the definition, and is not the definition of X in this context (which was asked to be done by a person) but a computational replication of an earlier definition, which is still a definition but not a choice, or even the acknowledgement that there is a choice between choice and no choice (meaning just saying X=Y which is a bit of a non-choice in this context but still valid).
You can find programs for axioms, like if have the axiom S(0)=1 I can find a program that display s(0)=1 on my screen. That is just not a definition, it is a replication or association. I can even find a program that displays 0=1 and is correct about that if I define 0 to mean the natural number 0 the symbol 1 to mean the natural number 0. All of these things are possible and valid, although a bit wild syntactically.
No, I do not think it is wrong.
It says it enables to associate a program with each proof in Zermelo-Fraenkel set theory. You can also, in principle associate a program to each value of the busy beaver function, or even uncountably many of them (for example for each value of the BB function a complex-valued function that based of the square of the value of the BB function as a constant in each of the complex-valued functions of each value). Even though you cannot compute the values of the busy beaver function.
That means you can associate programs to uncomputable functions, like the function of definition.
I can also associate a program to X = ?; for example rand(60). That however assumes that the natural number in question is a constant, which as I said above does not logically follow from the instruction of choosing one natural number. You can logically instruct something, and do something different. That is not a contradiction in terms of logic.
But as I said above that program would not compute X, it would merely be associated to X, which is a different notion. For example I can associate the BB function to X, but that does not make X computable, and indeed the opposite follows, as X could have the values of the BB function, which is proven to not be computable. So X could be not computable, and as it could be not computable, it is uncomputable in this context, as the question is if you can compute X without first defining it, which you cannot. Once you defined X=3, you can of course program a computer to deduce X=3, but that happens after the definition, and is not the definition of X in this context (which was asked to be done by a person) but a computational replication of an earlier definition, which is still a definition but not a choice, or even the acknowledgement that there is a choice between choice and no choice (meaning just saying X=Y which is a bit of a non-choice in this context but still valid).
You can find programs for axioms, like if have the axiom S(0)=1 I can find a program that display s(0)=1 on my screen. That is just not a definition, it is a replication or association. I can even find a program that displays 0=1 and is correct about that if I define 0 to mean the natural number 0 the symbol 1 to mean the natural number 0. All of these things are possible and valid, although a bit wild syntactically.