Why doesn't universality imply existence?

Question

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.

Answer 1

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.

Answer 2

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.