Name for introducing negation with quantifiers

Question

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'.

Answer 1

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

Short answer: No.

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!).

Answer 2

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.

Answer 3

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.