# De Morgan's laws for classical predicate logic

LEMMA    $$\forall x : P(x) \vdash \neg \exists x : \neg P(x)$$

Proof available

LEMMA    $$\neg \exists x : \neg P(x) \vdash \forall x : P(x)$$

Proof available

THEOREM    $$\forall x : P(x) \dashv\vdash \neg \exists x : \neg P(x)$$

Proof unavailable

LEMMA    $$\forall x : \neg P(x) \vdash \neg \exists x : P(x)$$

Proof available

LEMMA    $$\neg \exists x : P(x) \vdash \forall x : \neg P(x)$$

Proof available

THEOREM    $$\forall x : \neg P(x) \dashv\vdash \neg \exists x : P(x)$$

Proof unavailable

LEMMA    $$\neg \forall x : P(x) \vdash \exists x : \neg P(x)$$

Proof available

LEMMA    $$\exists x : \neg P(x) \vdash \neg \forall x : P(x)$$

Proof available

THEOREM    $$\neg \forall x : P(x) \dashv\vdash \exists x : \neg P(x)$$

Proof unavailable

LEMMA    $$\neg \forall x : \neg P(x) \vdash \exists x : P(x)$$

Proof available

LEMMA    $$\exists x : P(x) \vdash \neg \forall x : \neg P(x)$$

Proof available

THEOREM    $$\neg \forall x : \neg P(x) \dashv\vdash \exists x : P(x)$$

Proof unavailable