Thanks for a beautiful example with the Cantor set! And the Morel result provides a characterization of sorts (although the stated fact is very easy to prove). I guess in Baumgartner's model, none of the omega_1 dense orders are rigid. Lastly, why is your answer community wiki? It is a pity, since this prevents you from earning the votes your answer has deserved.

Can we get a summary of the characterization put up here?

@Kevin Lin: Tarski proved that there is an algorithm to decide the truth or falsity of any first order statement in the real-closed field (R,+,l,0,<). The concepts of points, lines, planes, circles, conics, spheres, paraboloids, etc. are all expressible in this language, using the usual polynomials. Thus, we have a decision procedure for Cartesian (as opposed to Euclidean) geometry. And the algorithm handles any R^n simply by working with coordinates.

I'm not sure what the right generalization is. There was something special about omega in my argument, since with the product topology the basic open sets have finite support, and this was what allowed for the diagonalization argument at the end. Perhaps for larger cardinals, there might be a clever workaround...

I am not sure exactly how you would like to divide model theory and meta-mathematics, but surely this topic fits naturally into a discussion of elimination of quantifiers, which would seem to be an important part of model theory, no? About your second comment, alas, it is true. Nevertheless, I shall wax poetic about the significance of our having come to a great enough understanding of geometry that we have a decision procedure.

Yes, I agree...

Oh, I see you wanted either a reference or a counterexample, whereas I gave a proof. I'm sorry that I don't know a reference, but since it appears to be true, it must have been known classically, so surely there is a reference. What a fun problem!

These problematic Boolean algebras are those corresponding for the forcing to add a Cohen subset to omega_1. This is the canonical method of forcing the Continuum Hypothesis. Such a B has a dense set that is countably closed (every countable descending sequence in the dense set has a nonzero lower bound).

Thanks for accepting the answer. What other properties on f did you want? If you really want to handle every Boolean algebra, then it might not be possible to have much more. I say this because I found this answer in part by looking at particular Boolean algebras that I thought might be a counterexample to your property, and I proved for them that every f with your conditions is locally constant. That is, for these B every f has a maximal antichain A below whose elements f is constant. This suggested the solution I gave above.

Indeed, the Computable IVT as I stated it is equivalent to (a), and this is what Weirich proves (and what the questioner seems to have asked). A major goal of computable analysis is to undertand the computable reals as a mathematical structure, using classical logic, and it is statement (a) that implies, for example, that the computable reals are a real-closed field. (See Weirich Corollary 6.3.10.) Statement (b), in contrast, requires a uniform algorithm, which is a stronger notion. Such uniformity issues arise throughout compubility theory, both on the natural numbers and on the reals.