# Why doesn't universality imply existence?

I am currently learning the Lean proof assistant, and I had a hard time proving the following implication: $$\forall x, p (x) \implies \exists x,p(x)$$ I gave up after some time and I decided to do some research instead, but I couldn't find anything on the topic. It seems really strange to me, because obviously if a predicate is true for all x's, then there exists some x which satisfies the predicate.

Thanks.

• "... but I couldn't find anything on the topic." Lean pickings. – mjw Feb 18 at 18:36
• @mjw Aaarrgh... – Noah Schweber Feb 18 at 19:12
• @NoahSchweber: Not much to lean on. – user21820 Feb 19 at 3:45
• Every Fields Medalist I know says the statement is false. – Acccumulation Feb 19 at 5:54
• @Acccumulation Every Fields Medalist I know says the statement is true. – mgradowski Feb 19 at 6:43

In first-order set theory (and first-order logic in general), we always have $$(\forall x. P(x)) \rightarrow \exists x. P(x)$$

However, we do not have $$(\forall x \in A. P(x)) \rightarrow \exists x \in A. P(x)$$ unless $$A$$ is non-empty. Why? Because $$\forall x \in A. P(x)$$ abbreviates $$\forall x. x \in A \rightarrow P(x)$$, while $$\exists x \in A. P(x)$$ does not abbreviate $$\exists x. x \in A \rightarrow P(x)$$, but rather $$\exists x. x \in A \wedge P(x)$$.

If we take $$A=\emptyset$$, then $$\forall x. x \in \emptyset \rightarrow P(x)$$ is vacuously true, but $$\exists x. x\in \emptyset \wedge P(x)$$ is always false, since $$x \in \emptyset$$ never holds. So the former does not imply the latter, unless $$A \neq \emptyset$$.

In dependent type theory, the underlying formal theory of Lean, there is no direct equivalent to the "unbounded" quantifiers $$\forall x$$ and $$\exists x$$ of first-order logic. Whenever one writes ∃ x, p x in Lean, it's really just an abbreviation for ∃ x : T, p x, where T is some type determined by the type of p. For example, if we take is_even from the Lean tutorial, then ∃ x, is_even x abbreviates ∃ x : ℕ, is_even x.

So if α is a type variable, then proving (∀ x : α, p x) → ∃ x : α, p x is not possible: if it was, we would be able to substitute any type, including the empty type (see here) for α. However, if you fix any inhabited (~non-empty) type, e.g. by setting α = ℕ, then you will be able to prove (∀ x : ℕ, p x) → ∃ x : ℕ, p x.

• Writing { _ : inhabited α } , where α is the type variable indeed makes the proof possible. Thanks. – mgradowski Feb 18 at 19:23
• Worth noting that logics allowing empty domains are called inclusive logics. – user76284 Feb 19 at 4:11

Everything being a $$P$$ doesn't imply there is a $$P$$, as there might not be anything (in the universe we're quantifying over). Universal quantification really tells you certain things don't exist - in this case, non-$$P$$s. For example, we know all odd perfect numbers satisfy an impressive list of results, but for all we know there might not be any such numbers.

Edit, based on a point @NoahSchweber made: in first-order logic, we usually insist a universe cannot be empty, because it leads to inference-thwarting complications such as this.

• Is that why it was so difficult to prove? The statement is false! – mjw Feb 18 at 18:32
• Actually, in the usual semantics for first-order logic (which rules out empty universes) the sentence $\forall x p(x)\implies\exists x p(x)$ is valid - it's its "relativizations" like "$\forall x\in A(p(x))\implies \exists x\in A(p(x))$" which are not valid in general. – Noah Schweber Feb 18 at 18:32
• That said, I don't know how Lean handles it - if Lean allows an empty universe, then you're right. – Noah Schweber Feb 18 at 18:33
• @NoahSchweber Whatever Lean does, your observation is definitely worth adding to my answer. I've done so, with the most relevant link I could to substantiate your statement. – J.G. Feb 18 at 18:37