# Unable to get Null Quantification intuitively [closed]

$$∀x(A(x) → P) ⇔ ∃xA(x) → P$$

I know its proof but unable to get it intuitively. Please give some examples.

## closed as off-topic by user21820, kimchi lover, José Carlos Santos, Xander Henderson, Don ThousandOct 1 at 1:43

This question appears to be off-topic. The users who voted to close gave this specific reason:

• "This question is missing context or other details: Please provide additional context, which ideally explains why the question is relevant to you and our community. Some forms of context include: background and motivation, relevant definitions, source, possible strategies, your current progress, why the question is interesting or important, etc." – user21820, kimchi lover, José Carlos Santos, Xander Henderson, Don Thousand
If this question can be reworded to fit the rules in the help center, please edit the question.

• There's only one way to get intuition: exercise. – Professor Vector Feb 23 '18 at 9:26

Either $P$ is false, or it isn't.

If $P$ is false, then the first sentence says that for all $x$, $A(x)$ is false and the second sentence says that there does not exist an $x$ such that $A(x)$ is true. Those two seem equivalent to me.

If $P$ is true, then all implications are true anyways and therefore the two sides are clearly equivalent.

"Intuition"... quite hard.

Consider the following heuristic argument, assuming the tautological equivalence: $(p \to q) \equiv (\lnot p \lor q)$.

We can rewrite the formula as follows:

$\forall x (\lnot Ax \lor P) \Leftrightarrow (\lnot \exists x Ax \lor P)$.

Now, the issue is: $\forall$ does not distribute over "or", in general. But here we have that $x$ is not free in $P.$

Thus, we can distribute $\forall$ getting:

$(\forall x \lnot Ax \lor P) \Leftrightarrow (\lnot \exists x Ax \lor P)$.

Say there was some game with several players

Let $A(x)$ be '$x$ received a bribe'

Let $P$ be 'the game was rigged'

OK, so now $\exists x \ A(x) \rightarrow P$ is 'if some payer received a bribe, then the game was rigged'

And $\forall x (A(x) \rightarrow P)$ means 'for every player we can say that if that player received a bribe, then the game was rigged'

Here is a concrete example. Assume we are on an airplane where someone (called "the patient") gets sick, and any doctor among the passengers will be able to save the patient's life.

• Let $A(x)$ mean "passenger $x$ is a doctor".
• Let $P$ mean "the patient will survive".

$\forall x(A(x) \rightarrow P)$ now means "for all passengers, if the passenger is a doctor then the patient will survive".

$\exists x A(x) \rightarrow P$ now means "if there exists a passenger who is a doctor then the patient will survive".

It should be obvious that these statements have the same logical meaning.

While it's only useful (naively...) for constructively provable statements, I find the BHK interpretation to provide a lot of intuition in those cases, which are numerous.

In the BHK interpretation, we interpret $P\to Q$, as a function that takes evidence for $P$ to evidence for $Q$. $\forall x\in X.P(x)$ is interpreted as a (dependent) product which we can think of as a function $X\to\bigcup_{x\in X}P(x)$ which maps $x$ into evidence for $P(x)$. Finally, $\exists x\in X.P(x)$ is interpreted as a pair of an $x\in X$ and evidence for $P(x)$.

For the equivalence $$\forall x\in X.(A(x)\to P)\iff(\exists x\in X.A(x))\to P$$ the left hand side looks like a function that takes an $x$ and produces a function that takes evidence for $A(x)$ and produces evidence for $P$. The right hand side looks like a function that takes a pair of an $x$ and evidence for $A(x)$ and produces evidence for $P$. Their equivalence is essentially just the standard currying isomorphism.

Specifically, given evidence for the left hand side, which is a function $g$, we can produce evidence for the right hand side, namely $f(x,a)=g(x)(a)$. Conversely, if we were given $f$, we could make $g$ as $g(x)=a\mapsto f(x,a)$.

With this perspective, many constructive results are fairly obvious. For example, $P\to\forall x.Q(x)\iff\forall x.(P\to Q(x))$ is just swapping the order of arguments (of a curried function), as is $\forall x.\forall y.P(x,y)\iff\forall y.\forall x.P(x,y)$, and also $P\to(Q\to R)\iff Q\to(P\to R)$.