@FrançoisG.Dorais: since you mentioned that Siegel's Lemma was probably provable in $EFA$, what factors would possibly keep it from being provable in $EFA$?

Thanks. This is very helpful.

@FrançoisG.Dorais: it is provability in $EFA$ that interests me (and yes, that's the theorem I am referring to). I have been led to believe that the two systems of second-order arithmetic I have mentioned in my question have the same consistency strength as $EFA$ and are conservative over it for $\Pi_2$ sentences (via the Wikipedia entry for $EFA$). How would you go about proving that Seigel's Lemma is provable in $EFA$ (or could give me a reference where that has been already done)?

(cont.) considered as a "well-defined mathematical question" (at least from the point of view of mathematical philosophy). Hope this helps.

(cont.) an order-preserving mapping of the Kleene-Brouwer ordering (of our computation) into this interval. The resulting points may be thought of as moments of time at which steps of the generalized computation occur. Thus, for example, the generalized machine which solves the ordinary halting problem might, for a given input, perform its steps at times 1/2, 3/4, 7/8,...,1."]. If this quote from Rogers would be deemed a well-defined mathematical description (at least from the point of view of mathematical philosophy), then my question (you got it right in your comment) should be

@LSpice: Do you believe that an 'oracle' must be an "(infinite) input string" (as Prof. Bauer holds)? Given Prof. Davis' observation as quoted by me in my edit, it must, assuming that Prof. Bauer is correct in his assertion. But the "generalized machine" described by Rogers is as much a 'fiction' as Prof Bauer's 'infinite input string', however, Prof. Rogers' description of the generalized machine allows that a convergent computation of such a machine can be carried out in a finite amount of time ["Let the unit interval (of real numbers) be thought of as a finite interval of time. Take

Again, why the downvote?

Why the downvote?

Given what you wrote in your last comment, would you say that the Diaconescu set {$a$, $b$} is recursively enumerable?

Why would that not be the the case with Burgin's example?

True enough, but that doesn't answer my question. Without LEM, is it possible that neither of the disjuncts can be asserted (I seem to recall that Brouwer asserted that very thing, i.e. that given either $a$ $\lor$ $\neg$$a$, there are circumstances in which neither $a$ nor $\neg$$a$ can be asserted. Is that also the case with Burgin's example?)?