[tines]

I'm confused then because the paper linked in the OP states:

> The true source of uncomputeable functions is not the axiom if choice (which is valid intuitionistically) but the law of the excluded middle and indirect proof [emphasis original]

[pfortuny]

It is choice in constructible mathematics: something “totally different” from “zf” choice. Existence means “can construct”, essentially. There are “less” things in constructible mathematics than in zf. This is a rough explanation.