> 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?
> ...all of these concepts of usefulness are rather limited, and we only mean by them, that each science should have applications outside its own area, and that there is some general direction in this sequence of applications towards practical ones...
This phrasing suggests an "(in)exact sequence" of sciences, in which the image of a foundational science for a discipline (ex: Physics for Chemistry) is in the kernel of applications to an overlying science (ex: Chemistry to Biology).
The Man from the Future: The Visionary Life of John von Neumann by Ananyo Battacharya[0].
It’s a really good biography of John von Neumann. The book follows both his life and the impact of his work carried on by people who came after him. I can recommend this book.
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?