4
$\begingroup$

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.

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

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.

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

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.

$\endgroup$
  • $\begingroup$ Is that why it was so difficult to prove? The statement is false! $\endgroup$ – mjw Feb 18 at 18:32
  • 3
    $\begingroup$ 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. $\endgroup$ – Noah Schweber Feb 18 at 18:32
  • $\begingroup$ That said, I don't know how Lean handles it - if Lean allows an empty universe, then you're right. $\endgroup$ – Noah Schweber Feb 18 at 18:33
  • $\begingroup$ @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. $\endgroup$ – J.G. Feb 18 at 18:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.