[FOM] DC vs. CC

[Andrej Bauer]

Look at Chapter 8 (in particular Section 8.2) of

   T. Jech, The Axiom of Choice, North-Holland, Amsterdam, 1973.

where permutation models of set theory are used to show that DC is not
implied by CC. Direct link to the relevant page:

http://books.google.si/books?id=I64yC4JnKtYC&lpg=PP1&ots=qgis2Y8f0s&dq=T.%20Jech%2C%20The%20Axiom%20of%20Choice%2C&pg=PA122#v=onepage&q&f=false

A realizability model is very likely going to satisfy DC because all
you need to realize DC is a primitive recursion. Hmm, ok perhaps we
can fiddle with realizability. Does DC hold in extensional
realizability?

With kind regards,

Andrej