# Does the law of the excluded middle imply the existence of “intangibles”?

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.

• Can you elaborate on the last bit, please? – Stefan Mesken Dec 27 '15 at 10:36
• Let $P(k)$ be the proposition there exists a program of length $k$ that outputs the given long string, and that all programs of length less than $k$ do not output the string. The statement "there exists a unique $k < 1000000000000$ such that $P(k)$" is provable using LEM. Despite this existence proof, $k$ **cannot be explicitly constructed" in the sense that none of the statements $P(1), P(2), \dots P(1000000000000)$ are provable in ZFC, or in any other proof system with a significantly shorter algorithmic description than the long string. – zyx Dec 27 '15 at 14:56
• Now, for any known constructive formal proof system, such as CZF = Constructive ZF, that does not have LEM, as the "other proof system" that is unable to prove concrete statements like $P(628300)$, it is an exact parallel of the situation with Lebesgue measure. It is a property of constructive proof systems including CZF if they prove "there exists a $k$ such that $P(k)$" the proof can be converted to a proof of $P(k_0)$ for a specific $k_0$ Thus CZF+LEM proves that a $k$ exists, and CZF does not, so that there is no tangible construction or other constructive existence proof. – zyx Dec 27 '15 at 15:07

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 think the question is not about "for all $A$ there exists $B$" statements but existentially quantified ones, "exists $X$ such that...". In your answer, this would mean EVT for a particular function encoding one hard problem. Examples of that kind can be simplified to remove EVT by directly processing the underlying source of difficulty, such as a difficult 0-1 sequence. The intangible object is the maximum value of the sequence, which under LEM is equal to 0 or 1. Without LEM and for a hard enough sequence relative to fixed proof resources, it is not provable that this object exists. – zyx Dec 30 '15 at 7:14
• @zyx, true but there is no need even to talk about 0-1 sequences since the issue is simply a violation of trichotomy $(x=y)\wedge(x<y)\wedge(x>y)$. This is what leads to a failure of EVT. I would be interested in your thoughts on math.stackexchange.com/questions/1582790/… – Mikhail Katz Dec 30 '15 at 7:49

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).

• Probably the right notion you're looking for is "undefinable". Just for example, ZF has a model where every object is definable; precisely the collection of all definable sets over ZF modulo provable equality. This is because every existence axiom can be provably strengthened to a unique existence axiom. This clearly fails when you add AC, but works again if you increase it to GC (global choice). The reason is that GC gives you the ability to uniquely specify all the objects constructed by AC using the added function symbol $τ$. – user21820 Mar 8 '17 at 16:27