The same epistemological problem exists in a discrete context. My favorite example is https://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theorem https://e

The same epistemological problem exists in a discrete context. My favorite example is https://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theorem https://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theo.... There is a proof by contradiction that any class of graphs with the property that it is closed under minors can be characterized by a finite list of forbidden minors. Which therefore means that there is a polynomial time algorithm for membership in the class. The classic example is that "planar graphs" have the necessary property, and there are exactly two forbidden minors. However it is a pure existence proof. And the following facts are also known. We do not have a general way to construct the forbidden minors. Or a way to find out how many there are. Or any way to verify whether any given list of them is complete. And not just, "We don't know how to do it." But, "No such algorithm exists." (More precisely that being able to answer those questions in general leads to contradictions.) So despite the entirely discrete nature of this problem (there are only a countable number of such classes), we find ourselves asserting the existence of a finite thing that we cannot find, bound the size of, or verify the correctness of if someone presented a reasonable candidate for our inspection. In what meaningful way does this thing exist?