How to use of the constant " False" in a predicate logic implication appearing in a proof of : X included in EmptySet <=> X is empty While trying to prove the basic fact that : any set included in the EmptySet is empty, I was led to use the propositional constant " false" in a conditional quantified statement. Is the following proof correct? In case it is, what is the name of the rule allowing to go from line (3) to line (4)? It looks like modus tollens, but is it actually? Is it , so to say, an " a fortiori" modus tollens? Is there a basic rule saying : from X --> **f** , infer ~X (1) A is included in the EmptySet (2) <=> for all x, x belongs to A --> x belongs to the EmptySet (3) <=> for all x, x belongs to A ---> **f** (4) <=> for all x, ~ ( x belongs to A) (5) <=> it is false that there is an x such that x belongs to A (6) <=> A = the EmptySet

It is the Negation Introduction rule.

If the Language has the _falsum_) constant $\bot$, the rule amounts to :

> $\text {from } P \to \bot, \text { derive } \lnot P$.

In fact, we can define _negation_ from $\bot$ :

> $\lnot P \leftrightarrow P \to \bot$.