The problem with constructive halting oracles is, they assume the ability to output an arbitrary natural number. But, realistic agents can observe only a finite number of bits per unit of time. Therefore, there is no way to directly observe a constructive halting oracle. We can consider a realization of a constructive halting oracle in which the oracle outputs a natural number one digit at a time. The problem is, since you don't know how long the number is, a candidate oracle might never stop producing digits. In particular, take any non-standard model of PA and consider an oracle that behaves accordingly. On some machines that don't halt, such an oracle will claim they do halt, but when asked for the time it will produce an infinite stream of digits. There is no way to distinguish such an oracle from the real thing (without assuming axioms beyond PA).
Moreover, this is a special case of a general theorem: if there is any computable procedure that asymptotically tests a complete hypothesis about the environment, then this hypothesis must describe a computable environment. This still allows for testable incomplete hypotheses that postulate hypercomputation in the environment, for example "this box is a halting oracle in some model of PA". But, there is a sense in which the hypothesis itself is computable.
(Btw I made this observation before)
This is really important and I missed this, thanks. I've added a note at the top of the post.
I think your argument will also work for PA and many other theories. It's known as game semantics:
The simplest application of game semantics is to propositional logic. Each formula of this language is interpreted as a game between two players, known as the "Verifier" and the "Falsifier". The Verifier is given "ownership" of all the disjunctions in the formula, and the Falsifier is likewise given ownership of all the conjunctions. Each move of the game consists of allowing the owner of the dominant connective to pick one of its branches; play will then continue in that subformula, with whichever player controls its dominant connective making the next move. Play ends when a primitive proposition has been so chosen by the two players; at this point the Verifier is deemed the winner if the resulting proposition is true, and the Falsifier is deemed the winner if it is false. The original formula will be considered true precisely when the Verifier has a winning strategy, while it will be false whenever the Falsifier has the winning strategy.
Indeed, a constructive halting oracle can be thought of as a black-box that takes a PA statement, chooses whether to play Verifier or Falsifier, and then plays that, letting the user play the other part. Thanks for making this connection.
[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:
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.
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:
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.