The question "how would the coin have landed if I had guessed tails?" seems to me like a reasonably well-defined physical question about how accurately you can flip a coin without having the result be affected by random noise such as someone saying "heads" or "tails" (as well as quantum fluctuations). It's not clear to me what the answer to this question is, though I would guess that the coin's counterfactual probability of landing heads is somewhere strictly between 0% and 50%.
I'm confused, isn't the "objective probability" of heads 1/2 because that is the probability of heads in the definition of the setup? The halver versus thirder debate is about subjective probability, not objective probability, as far as I can tell. I'm not sure why you are mentioning objective probability at all, it does not appear to be relevant. (Though it is also possible that I do not know what you mean by "objective probability".)
This argument seems to depend on the fact that Sleeping Beauty is not actually copied, but just dissociated from her past self and so that from her perspective it seems like she is copied. If you deal with actual copies then it is not clear what is the sensible way for them to all pass around a science journal to record their experiences, or all keep their own science journals, or all keep their own but then recombine somehow, or whatever. Though if this thought experiment gives you SIA intuitions on the Sleeping Beauty problem then maybe those intuitions will still carry over to other scenarios.
I don't know what you mean by "should be allowed to put whatever prior I want". I mean, I guess nobody will stop you. But if your beliefs are well approximated by a particular prior, then pretending that they are approximated by a different prior is going to cause a mismatch between your beliefs and your beliefs about your beliefs.
[Nitpick: The Kelly criterion assumes not only that you will be confronted with a large number of similar bets, but also that you have some base level of risk-aversion (concave utility function) that repeated bets can smooth out into a logarithmic utility function. If you start with a linear utility function then repeating the bets still gives you linear utility, and the optimal strategy is to make every bet all-or-nothing whenever you have an advantage. At least, this is true before taking into account the resource constraints of the system you are betting against.]
OK, that makes sense.
MUH doesn't imply the existence of halting oracles. Indeed, the Computable Universe Hypothesis is supposed to be an extension of the Mathematical Universe Hypothesis, but CUH says that halting oracles do not exist.
I will have to think more about the issue of continuity vs uniform continuity. I suppose my last remaining argument would be the fact that Bishop--Bridges' classic book on constructive analysis uses uniform continuity on bounded sets rather than continuity, which suggests that it is probably better for constructive analysis at least. But maybe they did not analyze the issue carefully enough, or maybe the relevant issues here are for some reason different.
To fix the argument that every locally compact Polish space admits a proper metric, let be as before and let if and if . Next, let , where is a countable dense sequence. Then is continuous and everywhere finite. Moreover, if , then and thus is compact. It follows that the metric is proper.
Anyway I have fixed the typo in my previous post.
I don't know why my comment doesn't have a reply button. Maybe it is related to the fact that my comment shows up as "deleted" when I am not logged in.
Sorry, I seem to be getting a little lazy with these proofs. Hopefully I haven't missed anything this time.
New proof: ... We can extract a subsequence such that if and , then for all , and for all and , either (A) and or (B) and . By extracting a further subsequence we can assume that which of (A) or (B) holds depends only on and not on . By swapping and if necessary we can assume that case (A) always holds.
Lemma: For each there is at most one such that .
Proof: Suppose and , with . Then , a contradiction.
It follows that by extracting a further subsequence we can assume that for all .
Now let be an increasing uniformly continuous function such that and for all . Finally, let . Then for all we have . On the other hand, for all we have , for we have , and for we have . Thus . Clearly, cannot be a fiber of . Moreover, since the functions and are both uniformly continuous, so is .
Regarding your responses to my points:
I guess I don't disagree with what you write regarding my points 1 and 4.
It seems to be harder than expected to explain my intuitions regarding singularities in point 3. Basically, I think the reasons that abstract continuity came to be considered standard are mostly the fact that in concrete applications you have to worry about singularities, and this makes uniform continuity a little more technically annoying. But in the kind of problem we are considering here, it seems that continuity is really more annoying to deal with than uniform continuity, with little added benefit. I guess it also depends on what kinds of functions you expect to actually come up, which is a heuristic judgement. Anyway it might not be productive to continue this line of reasoning further as maybe our disagreements just come down to intuitions.
Regarding my point 2, I wasn't very clear when I said that uniform continuity gives you an algorithm, what I meant was that if you have an algorithm for computing the images of points in the dense sequence and for computing the modulus of continuity function, then uniform continuity gives you an algorithm. The function would be the kind of thing I would handle with uniform continuity away from singularities (to fix a definition for this, let us say that you are uniformly continuous away from singularities if you are uniformly continuous on sets of the form , where is some set of singularities).
In your definition of , I think you mean to write max instead of min. But I see your point, though the example seems a little pathological to me.
Anyway, it seems that you agree that it makes sense to restrict to Polish spaces based on computability considerations, which is part of what I was trying to say in 2.
If you have a locally compact Polish space, then you can find a metric with respect to which the space is proper (i.e. bounded subsets are compact): let , where is compact. With respect to this metric, continuity is the same as uniform continuity on bounded sets, so my proof should work then.
Proposition: Let be a Polish space that is not locally compact. Then (with the compact-open topology) is not first countable.
Proof: Suppose otherwise. Then the function has a countable neighborhood basis of sets of the form where is compact and is open. Since is not locally compact, there exists a point such that is not compact for any . For each , we can choose . Let , and note that is compact. Then is a neighborhood of . But then for some . This contradicts the fact that , since we can find a bump function which is on but at .
It does still seem to me that most of the useful intuition comes from point 4 of my previous comment, though.
I am going to take some license with your question because I think you are asking the wrong question. Arbitrary topological spaces and abstract continuity are rarely the right notions in real-world situations. Rather, uniform continuity on bounded sets usually better corresponds to the intuitive notion of "a small change in input produces a small change in output".
Thus, suppose that is a complete separable metric space and that is uniformly continuous on bounded sets. Then we can show that there exists a function which is uniformly continuous on bounded sets but not a fiber of (i.e. there is no such that for all ). Indeed, consider two cases:
is uniformly discrete. Then every map from to is uniformly continuous, so we get a contradiction from cardinality considerations.
is not uniformly discrete. Then for each n, since f is uniformly continuous on it has a modulus of continuity on this set, i.e. a continuous increasing function such that for all . Since is not uniformly discrete, there is a function such that for infinitely many , there exist such that . (To construct it, take pairs with , extract a subsequence that behaves geometrically nicely, and then find a function such that for all in the subsequence.) Clearly, cannot be a fiber of .
Sure, in that case there is a 0% counterfactual chance of heads, your words aren't going to flip the coin.