PD+ Derivation Rules

All the Derivation Rules of SD+ and of PD and

Quantifier Negation $(\text{QN})$

\( \sim(\forall x)\mathscr{P} \;\lhd\rhd\; (\exists x)\sim\mathscr{P} \)

\( \sim(\exists x)\mathscr{P} \;\lhd\rhd\; (\forall x)\sim\mathscr{P} \)

PDI Derivation Rules

All the Derivation Rules of PD and $`=\text{'}$ Rules

Identity Introduction $(=\text{I})$

$\rhd$

$(\forall x)x=x$

Identity Elimination $(=\text{E})$

	$a=b$
	$\mathscr{P}$
$\rhd$	$\mathscr{P}(a//b)$