Infinite-time Turing machines and the formal Church's thesis Infinite-time Turing machines are known to either halt or loop in countable time.
In the spirit of double-negation translation, is there a statement which is: classically equivalent to this; consistent with the formal Church's thesis, that all total functions on the integers are recursive; and (this part is of course subjective) which actually tells us something "meaningful or informative" beyond the vacuous sense in which any such translation does?
 A: I believe this is a very good question. I have been trying to find the answer for some questions very closely related to one which I describe in this post (been able to give very little time in last many months though). And as of yet, neither at a decisive solution and nor stuck. Of course one of these may be true in near future though. 
Now coming to the question, in one of my earlier questions(Trace-Recursive Functions and Natural/Unnatural Operations), I defined a class of function called "trace functions". I asked a few questions regarding them. I asked three questions regarding them, but actually, here (in this answer that is) we only restrict ourselves to the first question asked there (marked as (a) there).
As to why "trace functions" have any relevance here, let me first state a certain definition, and then it will become fairly clear as to why they are relevant. Consider a function $f:\omega{_C}{_K} \rightarrow \mathbb{N}$. Define a restriction of this function $f$ (denoted by $f_\alpha:\alpha \rightarrow \mathbb{N}$) as: $f_\alpha(x)=f(x)$ for all values $x$ in the domain of $f_\alpha$. We say that the function $f$ saturates if there exists some value $\beta$ such that for all $\omega{_C}{_K}>x \ge \beta$ we have $range(f_\beta)=range(f_x)$. Note that I am distinguishing range from co-domain here (which will be $\mathbb{N}$ on both sides of the equality). The smallest such value of $\beta$ can be called the saturation point. For example, an example of a function that doesn't saturate is one which corresponding to any $\alpha \in \omega{_C}{_K} $ returns the index of smallest program which generates the less-than relation (corresponding to well-order of $\alpha$ in terms of $\mathbb{N}$).
Now denote the collection of all trace functions by the set $T$. Consider the proposition: "Every function in the set $T$ (whose range is a subset of $\mathbb{N}$) saturates". The main question ends at this point. What follows in next few paragraphs reflects my own view on this matter in terms of significance of the question (in terms of answer see first paragraph).  
A negative answer to the question by itself doesn't "necessarily" settle anything (notice the use of "necessarily" though). However, I would argue that a positive answer to the question settles a certain general form of mathematical version of Church's thesis (I consider the more basic mathematical version to be correct without any doubt). We can also say that a positive answer to the question proves "Saturation Problem" (in case someone found the last sentence to be overly opinionated). I would say that a positive answer also gives some more credence to formal Church's thesis (but looking at it somewhat skeptically, perhaps it would just be further confirmation for someone who already believes it). My impression is that perhaps with a positive answer, a lot of the old philosophical problems/debates of maths simply retain their perennial nature. I personally also feel that a positive answer to this question also means that there is perhaps not that much significant difference between "constructive" and "intuitionistic". 
Now a slightly philosophical point that is almost necessary to make (to give some justification to the comments in last paragraph). Looking at it from critical perspective, someone could just go on to give countless examples of "reasonable" functions $h_0,h_1,h_2,h_3,h_4,.....,h{_9}{_9}$ (all with domain $\omega{_C}{_K}$ and co-domain $\mathbb{N}$) and demonstrate that all of them saturate. My argument is that when one will look closely at all these functions, something of a systematic pattern will emerge. We will find that all of those functions will belong to the set  $T$. As a random example, if you take a function such as $x \mapsto \varphi_x(0)$, the corresponding function will belong to the set $T$ (though for the specific problem in this post we are just concerned with functions whose range is a subset of $\mathbb{N}$).   
This is why one of the potential issues that could arise with choosing collection of functions $T_1$ so that $T_1 \subset T$. The potential problem with $T_1$ could be that even if we settle the answer to the corresponding question in negative (that is, all function in $T_1$ saturate), if someone demonstrates a simple "reasonable" function $h_0$ so that $h_0 \notin T_1$, the corresponding result loses the philosophical significance. If one informally denotes the collection of natural/good functions ($\omega{_C}{_K}$ to $\omega{_C}{_K}$) as $A$, then we can write $T_1 \nsubseteq A$. The problem is whether $A$ can be considered a collection in a strict mathematical sense or not. And that, in my opinion, really comes down to having a (mathematical) notion of a good notation (the first two comments below the question I linked describe my reason for this line of thinking). Now suppose (for the sake of argument that follows) that such a notion existed but we missed it for some reason. If someone does accept the reasoning I mentioned in the comments (in linked question), then we have $T \supseteq  A$ (the reasoning is that the "story" of a calculation is represented in the trace). Write $saturate(T)$ to mean that all function in $T$ (with appropriate range) saturate (and same for $A$). Note that then we have $saturate(T) \rightarrow saturate(A)$.
EDIT: It was mentioned in comments (by Noah Schweber and Andrej Bauer) that it is hard to see whether the answer has relevance to question at hand. I don't know whether this will be sufficient to convince someone or not, but it seems reasonable to add a few direct comments in this regard. Unfortunately though, perhaps this answer has gone way too long with this edit (possibly more than length suitable for this site). I probably wouldn't have posted this if I knew it would get that long.
Firstly, one could mention that, given the definition of set $T$ mentioned in linked thread, if one adds the rather (very) basic condition to underlying recursive well-orders that successor relation must be computable in them, then it can be proved (rather easily) that the function which is computed as a result is also step-recursive. In other words the representation of corresponding function will also be computable in (some) arbitrarily large recursive well-orders. 
I hope the point mentioned in last paragraph makes sense, because it is important. Now the collection $A$ was mentioned in the answer (last paragraph before edit). Consider the following possibilities: (i) $A$ doesn't have any mathematical existence (and hence isn't a set) (ii) $A$ doesn't have any mathematical existence (and hence isn't a set) but exists in the sense that we can actually find a (mathematical) set $T$ such that every member of $T$ is also a member of $A$ (iii) $A$ has a precise mathematical characterization and we don't know it (iv) $A$ has a precise mathematical characterization and we know it.  
The answer I gave applies to possibilities (ii),(iii),(iv) .... doesn't matter which of them holds currently. The answer does not apply for possibility (i). I understand that possibility (ii) is a bit strange (so you don't have to agree with me that it is reasonable). I just included it for the sake of being exhaustive and because it seems reasonable to me personally.
But how does it relate to formal CT? Here is how I see it. Computable well-order relations for arbitrarily large elements of $\omega{_C}{_K}$ exist due to formal CT anyway. So far so good, but in my opinion formal CT is based on rejection (without deeper contemplation) of a potential contingency ..... whether that contingency is true or not is another matter.
Now let's discuss that contingency. Before discussing it I should mention that in my answer I assumed $T \supseteq A$ (and the last two paragraphs just before the edit were about trying to justify it). The contingency is that suppose some function in $A$ doesn't saturate. Now suppose that function (say $f$) is step-recursive (which as mentioned is basically satisfied by adding a rather modest condition to functions in $T$) and it forms a bijection with $\omega{_C}{_K}$. But now because the function $f$ is step-recursive, there exist arbitrarily large numbers $\alpha$ below the limit $\omega{_C}{_K}$ in which the representation of $f$ is computable. And the cumulative effect of those computable representations of $f$ is to give a total function in the limit which is non-recursive. Surely you could say that perhaps there is some potentially convoluted reason, where you could still deny the resulting function from actually being called a function. But anyway the burden would still be on person saying it isn't a (total) function. Nevertheless, this is still a rather subtle issue, and many important side issues could result from considering questions related to it. I am simply not qualified enough to analyze them mathematically though I can identify some points conceptually (bringing those conceptual points here is not suitable). But still, there are certain reasons I convincingly believe this objection to not hold any weight. For now though, we move on to other points.   
The idea is simply to mark the occurrence of smallest point at which a number occurs in $f$ and compare it smallest occurrence point of other numbers. A simple trick of this type is ruled out when all functions in $A$ are saturating. Because, given the function $f \in A$ is step-recursive, one will keep getting new partial recursive function (in the limit that $f$ it reaches its saturation point). But once you reach it you still have just an ordinary partial recursive function. And furthermore, going beyond for computable representations of $f$ for elements higher than saturation point, the resulting partial recursive function doesn't change.   
That's why I was trying to say that if we have $T \supseteq A$, we also have $saturate(T) \rightarrow saturate(A)$ and hence proving $saturate(T)$ keeps the possibility of any such function $f \in A$ threatening to violate internal coherence (for the lack of better word) of formal CT out of the window (personally I don't believe it is just about formal CT, but that would be too off-topic). 
One could still make potential objection like "Such a function $f$ sounds impossible". But in this case if one can't give an example that shows $T \nsupseteq A$ in a convincing manner, then one simply has to prove $saturate(T)$. Or prove $saturate(B)$ for any $B$ such that $B \supseteq A$. If one believes that such an $f$ is impossible, then one could give heuristic arguments of some sort, but in my opinion such arguments would fall short of proving saturation of some/any superset of $A$. Or one could simply that the premise of this answer is false (which is fine too).
And finally, here are few brief sentences about my current view on this as it stands. Below I refer to possibilities (i),(ii),(iii),(iv) for ones mentioned for collection $A$ (third paragraph of EDIT). I don't think that the core problems are either the precise characterisation of $A$ or the truth vaue of $saturate(A)$ (given $A$ exists as a mathematical collection). These are derivatve problems in my view and the core problem is finding a precise notion for a good well-ordering, if it exists in the first place. If such a precise characterisation doesn't exist then neither does one exist for the collection $A$ (and it isn't a collection in the strict mathematical sense). In that case I believe that possibility (ii) should be true (I don't believe in possibility (i)). [Opinion] == And furthermore, then it is highly likely that $saturate(T)$ is true ==. If a precise characterisation of a good well-order does exist, then I think a precise characterisation of $A$ does exist. [Opinion] == But it might no longer be that important because I consider it more likely in this case that $saturate(A)$ is false rather than true ==. And well, in the case $saturate(A)$ does turn out to be true (less likely in my view), I guess good for formal CT.  
