Negácia kvantifikátorov viazaných na množinu

[Martin Sleziak]

Povedali sme si, že výroky s kvantifikátormi vieme negovať veľmi jednoducho, pričom základom je nasledovná ekvivalencia:
$$\neg[(\forall x)P(x)] \Leftrightarrow (\exists x) \neg P(x).$$

Tiež sme si povedali, že nasledujúce veci v skutočnosti chápeme takto:
$(\forall x\in A)P(x) \overset{\mathrm{def}}\Leftrightarrow (\forall x) (x\in A \Rightarrow P(x)); \\
(\exists x\in A)P(x) \overset{\mathrm{def}}\Leftrightarrow (\exists x) (x\in A \land P(x)).$
(V kontexte, v ktorom pracujeme, je to dôležité aj preto, že takýmto spôsobom bude $(\forall x\in A)P(x)$ predstavovať formulu jazyka teórie množín, ak $P(x)$ je tiež formula jazyka teórie množín.)

Ako nepovinná d.ú. zostalo na rozmyslenie, či aj potom môžeme takto mechanicky negovať výroky, t.j. či platí
$$\neg[(\forall x\in A)P(x)] \Leftrightarrow (\exists x\in A) \neg P(x).$$

Spoiler:

Malo by byť jasné, že to naozaj platí, ale keby sme to chceli formálne skontrolovať, tak chceme znegovať výrok $(\forall x) (x\in A \Rightarrow P(x))$, pričom postupne dostaneme:
$\neg(\forall x) (x\in A \Rightarrow P(x)) \Leftrightarrow\\
(\exists x) \neg (x\in A \Rightarrow P(x)) \Leftrightarrow\\
(\exists x) (x\in A \land \neg P(x)) \Leftrightarrow\\
(\exists x\in A) \neg P(x)
$