[ED NOTE: see Vanessa Kosoy’s comment here; this post assumes a setting in which the oracle may be assumed to return a standard natural.]
It is not immediately clear whether hypercomputers (i.e. objects that execute computations that Turing machines cannot) are even conceivable, hypothesizable, meaningful, clearly definable, and so on. They may be defined in the notation of Peano arithmetic or ZFC, however this does not imply conceivability/hypothesizability/etc. For example, a formalist mathematician may believe that the Continuum hypothesis does not have a meaningful truth value (as it is independent of ZFC), and likewise for some higher statements in the arithmetic hierarchy that are independent of Peano Arithmetic and/or ZFC.
A famous and useful criterion of scientific hypotheses, proposed by Karl Popper, is that they are falsifiable. Universal laws (of the form “∀x. p(x)”) are falsifiable for testable p, as they can be proven false by exhibiting some x such that p(X) is false. In an oracle-free computational setting, the falsifiable hypotheses are exactly those in ∏₁ (i.e. of the form “∀n. p(n)” for natural n and primitive recursive p).
However, ∏₁ hypotheses do not hypothesize hypercomputation; they hypothesize (computably checkable) universal laws of the naturals. To specify the falsifiability criterion for hypercomputers, we must introduce oracles.
Let a halting oracle be defined as a function O which maps Turing machine-specifications to Booleans, which outputs “true” on exactly those Turing machines which eventually halt. Then, we can ask: is the hypothesis that “O is a halting oracle” falsifiable?
We can immediately see that, if O ever outputs “false” for a Turing machine which does eventually halt, it is possible to exhibit a proof of this, by exhibiting both the Turing machine and the number of steps it takes to halts. On the other hand, if O ever outputs “true” for a Turing machine which never halts, it is not in general possible to prove this; to check such a proof in general would require solving the halting problem, which is uncomputable.
Therefore, the hypothesis that “O is a halting oracle” is not falsifiable in a computational setting with O as an oracle.
However, there is a different notion of halting oracle whose definition is falsifiable. Let a constructive halting oracle be defined as a function O which maps Turing machine-specifications to elements of the set {∅} ∪ ℕ (i.e. either a natural number or null), such that it returns ∅ on those Turing machines which never halt, and returns some natural on Turing machines that do halt, such that the machine halts by the number of steps given by that natural. This definition corresponds to the most natural definition of a halting oracle in Heyting arithmetic, a constructive variant of Peano Arithmetic.
We can see that:
If there exists a machine M such that O(M) = ∅ and M halts, it is possible to prove that O is not a constructive halting oracle, by exhibiting M and the time step on which M halts.
If there exists a machine M such that O(M) ≠ ∅ and M does not halt by O(M) time steps, it is possible to prove that O is not a constructive halting oracle, by exhibiting M.
Therefore, the hypothesis “O is a constructive halting oracle” is computably falsifiable.
What about higher-level constructive halting oracles, corresponding to Σₙ in the Heyting Arithmetic interpretation of the arithmetic hierarchy? The validity of a constructive Σₙ-oracle is, indeed, falsifiable for arbitrary n, as shown in the appendix.
Therefore, the hypothesis that some black-box is a (higher-level) constructive halting oracle is falsifiable, in an idealized computational setting. It is, then, meaningful to speak of some black-box being a hypercomputer or not, on an account of meaningfulness at least as expansive as the falsifiability criterion.
This provides a kind of bridge between empiricism and rationalism. While rationalism may reason directly about the logical implications of halting oracles, empiricism is more skeptical about the meaningfulness of the hypothesis. However, by the argument given, an empiricism that accepts the meaningfulness of falsifiable statements must accept the meaningfulness of the hypothesis that some black-box O is a constructive halting oracle.
I think this is a fairly powerful argument that hypercomputation should not be ruled out a-priori as “meaningless”, and should instead be considered a viable hypothesis a-priori, even if it is not likely given other evidence about physics, anthropics, etc.
Appendix: higher-level halting oracles
We will now reason directly about the Heyting arithmetic hierarchy rather than dealing with Turing machines for simplicity, though these are logically equivalent. Σₙ₊₁ propositions can be written as ∃x₁∀y₁...∃xₙ∀yₙ.f(x₁, y₁, …, xₙ, yₙ) for some primitive-recursive f. The converse of this proposition (which is in ∏ₙ₊₁) is of the form ∀x₁∃y₁...∀xₙ∃yₙ.¬f(x₁, y₁, …, xₙ, yₙ).
An oracle O constructively deciding Σₙ₊₁ is most naturally interpreted as a function from a specification of f to (∃x₁∀y₁...∃xₙ∀yₙ.f(x₁, y₁, …, xₙ, yₙ)) ∨ (∀x₁∃y₁...∀xₙ∃yₙ.¬f(x₁, y₁, …, xₙ, yₙ)); that is, it decides whether the Σₙ₊₁ proposition is true or its converse ∏ₙ₊₁ proposition is, and provides a witness either way.
What is a natural interpretation of the witness? A witness for Σₙ₊₁ maps y₁...yₙ to x₁...xₙ (and asserts f(x₁, y₁, …, xₙ, yₙ)), while a witness for ∏ₙ₊₁ maps x₁..xₙ to y₁...yₙ (and asserts ¬f(x₁, y₁, …, xₙ, yₙ)). (Note that the witness must satisfy regularity conditions, e.g. the x₁ returned by a Σₙ₊₁ witness must not depend on the witness’s input; we assume that even invalid witnesses still satisfy these regularity conditions, as it is easy to ensure they are satisfied by specifying the right witness type)
Now, we can ask four questions:
Fix f; suppose the Σₙ₊₁ proposition is true, and an invalid Σₙ₊₁-witness is returned; then, is it possible to prove the oracle false?
Fix f; suppose the ∏ₙ₊₁ proposition is true, and an invalid ∏ₙ₊₁-witness is returned; then, is it possible to prove the oracle false?
Fix f; suppose the Σₙ₊₁ proposition is true, and a ∏ₙ₊₁-witness is returned; then, is it possible to prove the oracle false?
Fix f; suppose the ∏ₙ₊₁ proposition is true, and a Σₙ₊₁-witness is returned; then, is it possible to prove the oracle false?
These conditions are necessary and sufficient for O’s correctness to be falsifiable, because O will satisfy one of the above 4 conditions for some f iff it is invalid.
First let’s consider question 1. Since the witness (call it g) is invalid, it maps some y₁...yₙ to some x₁...xₙ such that ¬f(x₁, y₁, …, xₙ, yₙ). We may thus prove the witness’s invalidity by exhibiting y₁...yₙ. So the answer is yes, and similarly for question 2.
Now for question 3. Let the witness be g. Since the Σₙ₊₁ proposition is true, there is some x₁ for which ∀y₁...∃xₙ∀yₙ.f(x₁, y₁, …, xₙ, yₙ). Now, we may feed x₁ into the witness g to get a y₁ for which the oracle asserts ∀x₂∃y₂...∀xₙ∃yₙ.¬f(x₁, y₁, …, xₙ, yₙ). (Note, g’s returned y₁ must not depend on x’s after x₁, by regularity, so we may set the rest of the x’s to 0)
We proceed recursively, yielding x₁...xₙ and y₁...yₙ for which f(x₁, y₁, …, xₙ, yₙ), and for which the oracle asserts ¬f(x₁, y₁, …, xₙ, yₙ), hence proving the oracle invalid (through exhibiting these x’s and y’s). So we may answer question 3 with a “yes”.
For question 4, the proof proceeds similarly, except we start by getting x₁ from the witness. The answer is, then, also “yes”.
Therefore, O’s validity as a constructive Σₙ₊₁-oracle is falsifiable.
On the falsifiability of hypercomputation
Link post
[ED NOTE: see Vanessa Kosoy’s comment here; this post assumes a setting in which the oracle may be assumed to return a standard natural.]
It is not immediately clear whether hypercomputers (i.e. objects that execute computations that Turing machines cannot) are even conceivable, hypothesizable, meaningful, clearly definable, and so on. They may be defined in the notation of Peano arithmetic or ZFC, however this does not imply conceivability/hypothesizability/etc. For example, a formalist mathematician may believe that the Continuum hypothesis does not have a meaningful truth value (as it is independent of ZFC), and likewise for some higher statements in the arithmetic hierarchy that are independent of Peano Arithmetic and/or ZFC.
A famous and useful criterion of scientific hypotheses, proposed by Karl Popper, is that they are falsifiable. Universal laws (of the form “∀x. p(x)”) are falsifiable for testable p, as they can be proven false by exhibiting some x such that p(X) is false. In an oracle-free computational setting, the falsifiable hypotheses are exactly those in ∏₁ (i.e. of the form “∀n. p(n)” for natural n and primitive recursive p).
However, ∏₁ hypotheses do not hypothesize hypercomputation; they hypothesize (computably checkable) universal laws of the naturals. To specify the falsifiability criterion for hypercomputers, we must introduce oracles.
Let a halting oracle be defined as a function O which maps Turing machine-specifications to Booleans, which outputs “true” on exactly those Turing machines which eventually halt. Then, we can ask: is the hypothesis that “O is a halting oracle” falsifiable?
We can immediately see that, if O ever outputs “false” for a Turing machine which does eventually halt, it is possible to exhibit a proof of this, by exhibiting both the Turing machine and the number of steps it takes to halts. On the other hand, if O ever outputs “true” for a Turing machine which never halts, it is not in general possible to prove this; to check such a proof in general would require solving the halting problem, which is uncomputable.
Therefore, the hypothesis that “O is a halting oracle” is not falsifiable in a computational setting with O as an oracle.
However, there is a different notion of halting oracle whose definition is falsifiable. Let a constructive halting oracle be defined as a function O which maps Turing machine-specifications to elements of the set {∅} ∪ ℕ (i.e. either a natural number or null), such that it returns ∅ on those Turing machines which never halt, and returns some natural on Turing machines that do halt, such that the machine halts by the number of steps given by that natural. This definition corresponds to the most natural definition of a halting oracle in Heyting arithmetic, a constructive variant of Peano Arithmetic.
We can see that:
If there exists a machine M such that O(M) = ∅ and M halts, it is possible to prove that O is not a constructive halting oracle, by exhibiting M and the time step on which M halts.
If there exists a machine M such that O(M) ≠ ∅ and M does not halt by O(M) time steps, it is possible to prove that O is not a constructive halting oracle, by exhibiting M.
Therefore, the hypothesis “O is a constructive halting oracle” is computably falsifiable.
What about higher-level constructive halting oracles, corresponding to Σₙ in the Heyting Arithmetic interpretation of the arithmetic hierarchy? The validity of a constructive Σₙ-oracle is, indeed, falsifiable for arbitrary n, as shown in the appendix.
Therefore, the hypothesis that some black-box is a (higher-level) constructive halting oracle is falsifiable, in an idealized computational setting. It is, then, meaningful to speak of some black-box being a hypercomputer or not, on an account of meaningfulness at least as expansive as the falsifiability criterion.
This provides a kind of bridge between empiricism and rationalism. While rationalism may reason directly about the logical implications of halting oracles, empiricism is more skeptical about the meaningfulness of the hypothesis. However, by the argument given, an empiricism that accepts the meaningfulness of falsifiable statements must accept the meaningfulness of the hypothesis that some black-box O is a constructive halting oracle.
I think this is a fairly powerful argument that hypercomputation should not be ruled out a-priori as “meaningless”, and should instead be considered a viable hypothesis a-priori, even if it is not likely given other evidence about physics, anthropics, etc.
Appendix: higher-level halting oracles
We will now reason directly about the Heyting arithmetic hierarchy rather than dealing with Turing machines for simplicity, though these are logically equivalent. Σₙ₊₁ propositions can be written as ∃x₁∀y₁...∃xₙ∀yₙ.f(x₁, y₁, …, xₙ, yₙ) for some primitive-recursive f. The converse of this proposition (which is in ∏ₙ₊₁) is of the form ∀x₁∃y₁...∀xₙ∃yₙ.¬f(x₁, y₁, …, xₙ, yₙ).
An oracle O constructively deciding Σₙ₊₁ is most naturally interpreted as a function from a specification of f to (∃x₁∀y₁...∃xₙ∀yₙ.f(x₁, y₁, …, xₙ, yₙ)) ∨ (∀x₁∃y₁...∀xₙ∃yₙ.¬f(x₁, y₁, …, xₙ, yₙ)); that is, it decides whether the Σₙ₊₁ proposition is true or its converse ∏ₙ₊₁ proposition is, and provides a witness either way.
What is a natural interpretation of the witness? A witness for Σₙ₊₁ maps y₁...yₙ to x₁...xₙ (and asserts f(x₁, y₁, …, xₙ, yₙ)), while a witness for ∏ₙ₊₁ maps x₁..xₙ to y₁...yₙ (and asserts ¬f(x₁, y₁, …, xₙ, yₙ)). (Note that the witness must satisfy regularity conditions, e.g. the x₁ returned by a Σₙ₊₁ witness must not depend on the witness’s input; we assume that even invalid witnesses still satisfy these regularity conditions, as it is easy to ensure they are satisfied by specifying the right witness type)
Now, we can ask four questions:
Fix f; suppose the Σₙ₊₁ proposition is true, and an invalid Σₙ₊₁-witness is returned; then, is it possible to prove the oracle false?
Fix f; suppose the ∏ₙ₊₁ proposition is true, and an invalid ∏ₙ₊₁-witness is returned; then, is it possible to prove the oracle false?
Fix f; suppose the Σₙ₊₁ proposition is true, and a ∏ₙ₊₁-witness is returned; then, is it possible to prove the oracle false?
Fix f; suppose the ∏ₙ₊₁ proposition is true, and a Σₙ₊₁-witness is returned; then, is it possible to prove the oracle false?
These conditions are necessary and sufficient for O’s correctness to be falsifiable, because O will satisfy one of the above 4 conditions for some f iff it is invalid.
First let’s consider question 1. Since the witness (call it g) is invalid, it maps some y₁...yₙ to some x₁...xₙ such that ¬f(x₁, y₁, …, xₙ, yₙ). We may thus prove the witness’s invalidity by exhibiting y₁...yₙ. So the answer is yes, and similarly for question 2.
Now for question 3. Let the witness be g. Since the Σₙ₊₁ proposition is true, there is some x₁ for which ∀y₁...∃xₙ∀yₙ.f(x₁, y₁, …, xₙ, yₙ). Now, we may feed x₁ into the witness g to get a y₁ for which the oracle asserts ∀x₂∃y₂...∀xₙ∃yₙ.¬f(x₁, y₁, …, xₙ, yₙ). (Note, g’s returned y₁ must not depend on x’s after x₁, by regularity, so we may set the rest of the x’s to 0)
We proceed recursively, yielding x₁...xₙ and y₁...yₙ for which f(x₁, y₁, …, xₙ, yₙ), and for which the oracle asserts ¬f(x₁, y₁, …, xₙ, yₙ), hence proving the oracle invalid (through exhibiting these x’s and y’s). So we may answer question 3 with a “yes”.
For question 4, the proof proceeds similarly, except we start by getting x₁ from the witness. The answer is, then, also “yes”.
Therefore, O’s validity as a constructive Σₙ₊₁-oracle is falsifiable.