What's the intuition behind $(\exists y)(\mathscr{C}(y)\supset\mathscr{D})\supset((\forall x)\mathscr{C}(x)\supset\mathscr{D})$

Question

Let $\mathscr{C}$ and $\mathscr{D}$ be wfs. Suppose $y$ is not free for $\mathscr{D}$, and $\mathscr{C}(x)$ and $\mathscr{C}(y)$ are similar. Then in any first-order theory, it is a theorem that $$(\exists y)(\mathscr{C}(y)\supset\mathscr{D})\supset((\forall x)\mathscr{C}(x)\supset\mathscr{D})$$ (cf. Mendelson's Introduction to Mathematical Logic, Lemma 2.30).

I am trying to understand, not how to prove this formula, but how to grasp it intuitively -- the formulas I've encountered in mathematical logic have, until now, all been intuitively agreeable.

For example, suppose that $\mathscr{C}(y)$ means "Day $y$ is rainy", and $\mathscr{D}$ means "Bring an umbrella". Then what is this theorem imply about rainy days and umbrellas? Better yet, what's another example that would help make intuitive sense of this theorem?

Answer 1

$\big(\exists y~(\mathscr C(y)\supset\mathscr D)\big)\supset\big((\forall x~\mathscr C(x))\supset\mathscr D\big)$ aka: $\mathscr D$ if for everything $\mathscr C()$, if for something $\mathscr D$ if $\mathscr C()$.

If there exists something of which its being $\mathscr C(~)$ would imply $\mathscr D$, then if $\mathscr C(~)$ holds for everything, then $\mathscr D$ is implied; by reason that should $\mathscr C(~)$ hold for everything, it would hold for some thing for which that implies $\mathscr D$.

Per your example: If there is some particular day where, if it rained, you would need an umbrella, then if it rains every day, you will need an umbrella.

---

$$\begin{array}{|l} \hline~~\begin{array}{|l}\exists y~(\mathscr C(y)\supset\mathscr D)\quad:\textsf{assume} \\\hline~\begin{array}{|l}\forall x~\mathscr C(x)\quad:\textsf{assume} \\\hline~\begin{array}{|l}[a]~\mathscr C(a)\supset\mathscr D\quad:\textsf{existential elimination} \\\hline \mathscr C(a)\quad:\textsf{universal elimination to witness}\\ \mathscr D \quad:\textsf{conditional elimination}\end{array}\\\mathscr D\quad:\textsf{witness free}\end{array}\\(\forall x~\mathscr C(x))\supset\mathscr D\quad:\textsf{conditional introduction}\end{array}\\(\exists x~(\mathscr C(x)\supset\mathscr D))\supset((\forall x~\mathscr C(x))\supset\mathscr D)\quad:\textsf{conditional introduction}\end{array}$$

Answer 2

Assume the premise, i.e. that $(\exists y)(\mathscr{C}(y)\to\mathscr{D})$ holds.

This means that for some $d$ in the domain of the interpretation we have that :

$\mathscr{C}(d)\to\mathscr{D}$ is TRUE.

Now, two cases :

(i) $\mathscr{D}$ is TRUE. Thus, also $(\forall x)\mathscr{C}(x)\to\mathscr{D}$ is TRUE.

(ii) $\mathscr{D}$ is FALSE. But $\mathscr{C}(d)\to\mathscr{D}$ is TRUE, and thus we are forced to conclude that $\mathscr{C}(d)$ is FALSE.

But if $\mathscr{C}(d)$ is FALSE for some $d$, we have that $(\forall x)\mathscr{C}(x)$ is FALSE and thus $(\forall x)\mathscr{C}(x)\to\mathscr{D}$ is TRUE.

---

In the step (ii) of the argument above, it is essential that $y$ is not free in $\mathscr{D}$.

Answer 3

How about this:

There is an example that, if it makes intuitive sense of this formula, then you will be happy. So, if all examples make intuitive sense of this formula, then you will be happy.

Answer 4

Since this is a constructively valid theorem, it has a straightforward computational reading. Here's an informal description of that.

The theorem states: if I give you a $y$ and a proof of $\mathscr C(y)\to \mathscr D$, and I also give you a proof $\forall x.\mathscr C(x)$¹, then clearly you can take the $y$ you were given and instantiate $\forall x.\mathscr C(x)$ with it getting $\mathscr C(y)$ which you can then use with the proof of $\mathscr C(y)\to\mathscr D$ you were given to produce a proof of $\mathscr D$.

Here's a literal computational interpretation in Agda:

open import Data.Product

thm : {A Q : Set}{P : A → Set} → ∃[ y ] (P y → Q) → ((x : A) → P x) → Q
thm (y , prf) f = prf (f y)

¹ $P\to(Q\to R) \iff (P\land Q) \to R$

Answer 5

They used to say about Federal Reserve Chairman Alan Greenspan

If he smiles, the stock market will go up.

$$\exists m \in {\rm Man} ~:~ ({\rm Smiles}(m) \to {\rm StockIncrease})$$

So suppose someone said to you

Today, everyone is smiling.

Could you draw any conclusions about the stock market?

$$(\forall m \in {\rm Man} ~:~ {\rm Smiling}(m)) \to {\rm ???}$$