Oops, you’re right. I was thinking of cases where you are trying to generate answers to a query, which is different from testing one candidate answer.
Let me start over:
My suspicion, which I haven’t proved, is that Russell’s Paradox is a result of specifying a logic, and not specifying the algorithms used to evaluate statements in that logic or to answer queries. In any complete specification of a logic, including both the rules and the computational steps taken to evaluate or query-answer, you will probably find that you can prove what the outcome of the Russell’s paradox query is.
In other words, “formal logic” is too sloppy; my intuition is that in Russell’s paradox, it hides problems with order of execution.
Not really. In most standard axiomatic descriptions of set theory, like say ZFC, one doesn’t need to think at all about computability of set relations. This is a good thing. We want for example the Busy Beaver function to be well-defined. And we want to be able to talk about things like the behavior of Turing machines when connected to non-computable oracles. If we insist that our set theoretic relationships be computable this sort of thing becomes very hard to talk about.
Huh? The Busy Beaver function is all about computability. The function itself is not computable; but you know that only because you’ve spelled out how the computation works, and can show that there is an answer but that it is not computable.
ZFC was designed to avoid Russell’s Paradox; it does this by getting closer to a computable description of set theory. The definition itself is actually computational; a set of axioms of implication are just rewrite rules. It is ambiguous only in that it fails to specify what order rewrite rule applies first.
I have no problem with using non-computable oracles. But the way Turing machines interact with those oracles is computationally explicit. The view I’m expressing suggests you could run into troubles if you posed an oracle a question that hid ambiguities that would be resolved by a computational specification of the oracle. But I’ve never seen any use of an oracle that did that. People don’t use oracles for Russell’s paradox-like problems; they typically use them for non-computable functions.
How are you defining computable? Naively I would think it would be something like describable by a Turing machine that outputs the result after finite time. But Busy Beaver won’t do that. There may be definitional issues at work here.
Oops, you’re right. I was thinking of cases where you are trying to generate answers to a query, which is different from testing one candidate answer.
Let me start over:
My suspicion, which I haven’t proved, is that Russell’s Paradox is a result of specifying a logic, and not specifying the algorithms used to evaluate statements in that logic or to answer queries. In any complete specification of a logic, including both the rules and the computational steps taken to evaluate or query-answer, you will probably find that you can prove what the outcome of the Russell’s paradox query is.
In other words, “formal logic” is too sloppy; my intuition is that in Russell’s paradox, it hides problems with order of execution.
Not really. In most standard axiomatic descriptions of set theory, like say ZFC, one doesn’t need to think at all about computability of set relations. This is a good thing. We want for example the Busy Beaver function to be well-defined. And we want to be able to talk about things like the behavior of Turing machines when connected to non-computable oracles. If we insist that our set theoretic relationships be computable this sort of thing becomes very hard to talk about.
Huh? The Busy Beaver function is all about computability. The function itself is not computable; but you know that only because you’ve spelled out how the computation works, and can show that there is an answer but that it is not computable.
ZFC was designed to avoid Russell’s Paradox; it does this by getting closer to a computable description of set theory. The definition itself is actually computational; a set of axioms of implication are just rewrite rules. It is ambiguous only in that it fails to specify what order rewrite rule applies first.
I have no problem with using non-computable oracles. But the way Turing machines interact with those oracles is computationally explicit. The view I’m expressing suggests you could run into troubles if you posed an oracle a question that hid ambiguities that would be resolved by a computational specification of the oracle. But I’ve never seen any use of an oracle that did that. People don’t use oracles for Russell’s paradox-like problems; they typically use them for non-computable functions.
How are you defining computable? Naively I would think it would be something like describable by a Turing machine that outputs the result after finite time. But Busy Beaver won’t do that. There may be definitional issues at work here.
The busy beaver function isn’t computable; but it is posed within a well-defined computational model.
Ok. So when do you consider something to be within an acceptable computational model or not?