monads and Turing machines

[Ingo Blechschmidt]

Dear José,

On Sun Feb 26 03:01:56 2023, José Manuel Rodríguez Caballero wrote:
> Some questions could be: Any suggestions for formalizing this framework?

what you describe sounds very much like Lévy collapse, i.e. a version
of forcing which can render any specific set countable. Phrased in
computational terms, the monad which makes this work is then a version
of the "eventually monad" from computer science. (In case we pass down
to the double negation topology, as is usual in set-theoretic forcing
but which for Lévy collapse is not necessary, we obtain the more
familiar state monad.)

I don't know of a written reference for this specific point of view to
forcing, though it surely has been known to some for a long time. I'll
attach a paper draft in a separate mail to you personally; when my
coauthor Peter Schuster and I feel more comfortable with it, I'll also
share it publicly.

Cheers,
Ingo