Skip to main content
2 of 2
Added "proof theory" in solidarity to my advisor.
Jason Rute
  • 6.3k
  • 2
  • 30
  • 53

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.

Jason Rute
  • 6.3k
  • 2
  • 30
  • 53