# Name for introducing negation with quantifiers

The rewriting of $\varphi\to \psi$ into the logically equivalent $\neg \psi\to\neg \varphi$ is called contraposition.

Is there a similar word for rewriting $\forall x.\varphi$ into $\neg\exists x.\neg \varphi$?

The two operations are similar in that they replace one logical construction with one in which the subformulas of the original appear negated instead.

Background: I came across this when I noticed that the set-theoretic Axiom of Regularity seems much more intuitive and motivated if instead of the usual formulation

R. Every nonempty set $A$ has an element that is disjoint from $A$.

one thinks of it as

R'. There is no nonempty set $A$ such that every element of $A$ has an element that is itself in $A$.

(The set that R' claims doesn't exist would be an in-universe witness of one or more infinitely descending $\in$-chains (at least if Dependent Choice holds at the metalevel)).

But then I discovered that I don't have a nice succinct way to describe the rewriting that got me from R to R'.

• To me the rewriting here is very different. Contraposition still have the "→" connective around. The other rewriting allows you to eliminate universal qunatifiers if you want to (it's a possible definition of universal quantification in a system which only has existential quantification at it's basis). Also, I think you mean that the proper subformulas of the original have gotten negated, since the subformula (¬ψ→¬φ) is not negated. Examples of all subformulas getting replaced by their negations is Kpq by NANpNq and Apq by NKNpNq. Commented Oct 18, 2014 at 3:28

Is there a similar word for rewriting ∀x.φ into ¬∃x.¬φ?

Or at least there surely isn't one in common usage.

Making that kind of move in a proof in a lecture, I would probably have just said "By [the familiar] quantifier equivalence, ..."

By the way, the observation that Regularity is more intuitively appealing in the version $\mathbf{R}'$ is surely exactly right (I think some of the intro set books make the same point, but it is certainly a point worth making!).

Contraposition in classical logic can be "reduced" to the equivalence between :

$$p \rightarrow q$$ and $$\lnot p \lor q$$.

Thus, from :

$$\varphi \rightarrow \psi$$

using Commutativity : $$(\lnot \varphi \lor \psi) \leftrightarrow (\psi \lor \lnot \varphi)$$, and Double Negation we get :

$$\lnot \psi \rightarrow \lnot \varphi$$.

For the quantifiers, we can exploit the "analogy" between $$\forall$$ and an infinite conjunction and $$\exists$$ and an infinite disjunction.

Thus, starting from the correspondance between :

$$\forall x \varphi(x)$$ and $$\varphi(x_1) \land \varphi(x_2) \land \ldots$$

and applying a sort of "infinite" De Morgan, we have that :

$$\lnot \forall x \varphi(x)$$ correspond to : $$\lnot \varphi(x_1) \lor \lnot \varphi(x_2) \lor \ldots$$

which again can be read as : $$\exists x \lnot \varphi(x)$$.

Thus, if we want to "baptize" it, I think that "De Morgan" is more appropriate than "Contraposition".

Note

We have to note that all three equivalences used :

$$(p \rightarrow q) \leftrightarrow (\lnot p \lor q)$$

$$\lnot \lnot p \leftrightarrow p$$

$$\lnot (p \land q) \leftrightarrow (\lnot p \lor \lnot q)$$

hold only in classical logic.

Since the universal quantifier in $\varphi$ is equivalent to a conjunction of $[\overline{a}/x]\varphi$ of all elements $a$ of the universe $U$ (and the same holds for the existential quantifier in terms of disjunctions), they are regarded to be generalizations of De Morgan's laws, as others answered already:

\begin{align} \neg \forall x (\varphi) & \equiv \neg \bigwedge_{ a \in U} [\overline{a}/x]\varphi \tag{1} \\ &\equiv \bigvee_{a \in U} [\overline{a}/x]\neg\varphi \tag{2} \\ &\equiv \exists x \neg (\varphi) \tag{3} \end{align}

About your observation on the Axiom of Regularity in Set theory, I would say I myself experience the same phenomenon about the Compactness Theorem:

$Γ$ has a model ⇔ each finite subset $Δ$ of $Γ$ has a model.

Particularly, I feel that ($\Leftarrow$) sounds counter intuitive, when in its contrapositive form

$Γ$ has no model ⇒ Some finite subset $Δ$ of $Γ$ has no model.

it seems more transparent.

• ... especially when one remembers that "has no model" is equivalent to "can prove a contradiction", thanks to Gödel. Commented Oct 20, 2014 at 12:25
• @HenningMakholm Fully agree! Commented Oct 20, 2014 at 12:35