First off, I'm not sure if "intangible" is standard terminology, Wikipedia defines an intangible object to be: "objects that are proved to exist, but which cannot be explicitly constructed". So if someone could point me towards better terminology, I'd appreciate it.
The linked article from Wikipedia claims that the axiom of choice implies the existence of such intangible objects, using non-measurable sets as an example. I was wondering if the law of the excluded middle gives us similar examples of intangible objects. If there are no such examples, is it possible to prove that all objects proven to exist using the LEM also exist constructively? Would that even be possible to prove?
With LEM there is a very simple (but extremely long) proof that there exists a shortest program, in some fixed computer language, that prints the first million questions on Stack Overflow.
For a string of that complexity, no reasonable foundational system for mathematics, such as ZF set theory, can determine an optimal program or its length. Valid theorems of the form "the minimum program length is 1267301" or "the following program [...code...] is optimal" are not provable in ZFC once the shortest program for the string is significantly longer than a program describing ZFC.
The consequence is that LEM and very little additional logical strength show that a shortest program "exists", but proving that a particular program is the object that was shown to exist is impossible even in very strong systems of axioms for mathematics.