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.
To answer your question “is it possible to prove that all objects proven to exist using the LEM also exist constructively?” the answer is negative. Namely, there are “objects” that can be proved to exist using LEM that don’t exist constructively. For example, the extreme value theorem (EVT) familiar from calculus is invalid in constructive mathematics. The reason is that the classical proof of the existence of an extremum “object” exploits LEM. Additional details in the specific case of EVT can be found in this article: http://dx.doi.org/10.1007/s11787-014-0102-8
I’d like to add this answer now that I have a little more insight into the question — to hopefully help others who read this in the future.
Specifically, to address the title question: Not necessarily. Of course, over propositional logic we may assume LEM without any worries, because there are no existential statements, and thus the question of “existence” really doesn’t make sense except at the level of the meta-theory formalizing the logic. Thus, for simplicity’s sake, consider first order logic over some signature.
As others have pointed out, over ZFC (and perhaps comparable systems) LEM implies the existence of so-called “intangible objects” (I still haven’t seen this term used anywhere in the literature besides that wikipedia article). However, this is not be the case for every foundational system based on first order logic. For example, it is well known that for certain domains of mathematics, we can prove LEM constructively, and thus, if we work in a formal system that formalizes only such domains, adding LEM will not lead the existence of intangibles.
Perhaps more interestingly we could ask if there are formal systems which are not strong enough to prove LEM, and yet formalize a decidable domain of mathematics (where the decidability here is of course something provable in the metatheory, not in the formal system itself).