Skip to main content
MathOverflow

Return to Question

Added "proof theory" in solidarity to my advisor.
Source Link
Jason Rute
Jason Rute
  • 6.3k
  • 2
  • 30
  • 53

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.

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 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.

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.

Source Link
Jason Rute
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 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.