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

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?

• I hate that old notation of $\supset$ for $\to$. (I get it, but I still hate it.) Jun 14 '18 at 13:48
• Recall that the truth-functional model of "if ..., then..." (see truth-table for the conditional connective : $\to$) does not require any "causal connection" between antecedent and consequent: "If Plato is a philosopher, then 2+2=4" is TRUE. Jun 14 '18 at 13:49

$\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}$$

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)$1, 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)


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

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.

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}$.

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 ???}$$

• Indeed. It should be "There is a student whom, if is honest then you will buy me a drink" and "If every student is honest, then you will buy me a drink." $$\exists s\in \textsf{Student} : (\textsf{Honest}(s)\to\textsf{Drink})\\\downarrow\\(\forall s\in\textsf{Student}:\textsf{Honest}(s))\to\mathsf{Drink}$$ Jun 15 '18 at 9:44
• Oh you are right, all the cursive writing made me dizzy. Jun 15 '18 at 16:50