> In fact, is there any way to establish the existence of an example without exhibiting it specifically?
It struck me the other day that one easy way to get failure of the Excluded Middle is to be calculating in an overly-concrete representation. Then there will in general be a whole block of things that, since they really "ought" to be part of an equivalence class (semantically equivalent but syntactically unequal), don't invert when taking the pseudo-complement of another thing, and hence X|~X doesn't cover everything.
What applications of constructive logic clearly do not arise in this manner?
It struck me the other day that one easy way to get failure of the Excluded Middle is to be calculating in an overly-concrete representation. Then there will in general be a whole block of things that, since they really "ought" to be part of an equivalence class (semantically equivalent but syntactically unequal), don't invert when taking the pseudo-complement of another thing, and hence X|~X doesn't cover everything.
What applications of constructive logic clearly do not arise in this manner?