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

Parent topics