Predicate logic


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

Proof available

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

Proof available

THEOREM    \(\exists x,y : P(x, y) \vdash \exists y,x : P(x, y)\)

Proof available

THEOREM    \(\forall x,y : P(x, y) \vdash \forall y,x : P(x, y)\)

Proof available

THEOREM    \(\forall x : P(x) \wedge Q(x) \vdash [\forall x : P(x)] \wedge [\forall x : Q(x)]\)

Proof available

THEOREM    \([\forall x : P(x)] \wedge [\forall x : Q(x)] \vdash \forall x : P(x) \wedge Q(x)\)

Proof available

THEOREM    \(\forall x : P(x) \wedge Q(x) \dashv\vdash [\forall x : P(x)] \wedge [\forall x : Q(x)]\)

Proof unavailable

THEOREM    \(\exists x : P(x) \vee Q(x) \vdash [\exists x : P(x)] \vee [\exists x : Q(x)]\)

Proof available

THEOREM    \([\exists x : P(x)] \vee [\exists x : Q(x)] \vdash \exists x : P(x) \vee Q(x)\)

Proof available

THEOREM    \(\exists x : P(x) \vee Q(x) \dashv\vdash [\exists x : P(x)] \vee [\exists x : Q(x)]\)

Proof unavailable

THEOREM    \(\forall x : P(x) \Rightarrow Q(x) \vdash [\forall x : P(x)] \Rightarrow [\forall x : Q(x)]\)

Proof available

THEOREM    \(P \Rightarrow Q \Rightarrow R \vdash P \wedge Q \Rightarrow R\)

Proof available

THEOREM    \(P \wedge Q \Rightarrow R \vdash P \Rightarrow Q \Rightarrow R\)

Proof available

THEOREM    \(P \Rightarrow Q \Rightarrow R \dashv\vdash P \wedge Q \Rightarrow R\)

Proof unavailable