by Thorsten on November 2, 2007.
Tagged as: Lunches.
It is strange: on the one hand the axiom of choice is singled out as the source of non-constructivity in classical theories on the other the axiom of choice is actually provable in a constructive theory like Martin-Loef’s Type Theory. What is the cause of this apparent contradiction? I showed that while the proof-relevant axiom of choice is provable in Type Theory, a proof-irrelevant version where we are not allowed to make choices based on the witness of an existential proof is not and even worse we can show that it implies the principle of excluded middle for propositional reasoning. This is a construction due to Diaconescu which I sketched on the whiteboard. I also noticed that the countable axiom of choice or indeed ore general the axiom of choice over any type not involving quotients (this excludes in particular the Reals) is implied by the setoid model and hence type-theoretically hunky dory. I finished with the question, how to generalize the axiom of predicative topoi (which do not entail those choice principles) to fully reflect the setoid model.
I forgot to mention that my presentation was based on a discussion on the Epigram mailing list early this year, in particular in reply to an issue raised by Bas Spitters.