5 votes

Is there computational interpretation for countable choice?

In realizability theory another computational interpretation of countable choice is a procedure for computing canonical forms of natural numbers. I explained this in detail in this answer to a similar ...
Andrej Bauer's user avatar
  • 8,621
5 votes

Is there computational interpretation for countable choice?

It really depends on what you call countable choice, and in particular the semantics of your Prop fragment. Assuming you phrase CC as ...
Pierre-Marie Pédrot's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible