# The topos for forcing in computability theory

My understanding is that forcing (such as Cohen forcing) can be described via a topos. For example this nlab article on forcing describes forcing as a "the topos of sheaves on a suitable site."

My question concerns forcing in computability theory, for example as described in Chapter 3 or these lecture notes of Richard Shore. The idea is that the generics are those which meet all computable dense sets of forcing conditions. (Computable can mean a few things. Often it is taken to mean a $\Sigma^0_1$ set of forcing conditions. Also, usually the forcing posets are countable.) Since there are only countably many such dense sets, such effective generics exist.

Is there a known/canonical type of topos corresponding to the forcing in computability theory?

Any references would be appreciated.

FYI: My background is in computability theory, proof theory, and computable analysis. I know little about topos theory, but I am willing to learn a bit. I am mostly asking this question because I want to compare some ideas I have about effective versions of Solovay forcing with some work by others about the topos corresponding to Solovay forcing. Also, it is always nice to learn new things.

• Did you also want the forcing partial order to be a (close to) computable relation? – Bjørn Kjos-Hanssen Feb 6 '15 at 9:20
• @BjørnKjos-Hanssen, I would be happy to know the answer in that case. (The application I have in mind is a bit more general, but I think knowing what is going on in the case of a computable forcing poset is sufficient for me to get a general idea of what is going on.) – Jason Rute Feb 6 '15 at 14:38
• Have you, since asking the question two years ago, learned about a topos-theoretic treatment of forcing in computability theory? – Ingo Blechschmidt May 31 '17 at 14:18