PD Derivation Rules

Derivation Rules
Alex Guevara

All the Derivation Rules of SD and

$`\forall\text{'}$ Rules

Universal Introduction $(\forall\text{I})$

	$\mathscr{P}(a/x)$
$\rhd$	$(\forall x)\mathscr{P}$

Provided:

$a$ does not occur in an undischarged assumption.
$a$ does not occur in $(\forall x)\mathscr{P}.$

Universal Elimination $(\forall\text{E})$

	$(\forall x)\mathscr{P}$
$\rhd$	$\mathscr{P}(a/x)$

$`\exists\text{'}$ Rules

Existential Introduction $(\exists\text{I})$

	$\mathscr{P}(a/x)$
$\rhd$	$(\exists x)\mathscr{P}$

Existential Elimination $(\exists\text{E})$

	$(\exists x)\mathscr{P}$
		$\mathscr{P}(a/x)$
		$\mathscr{Q}$
$\rhd$	$\mathscr{Q}$

Provided:

$a$ does not occur in an undischarged assumption.
$a$ does not occur in $(\exists x)\mathscr{P}.$
$a$ does not occur in $\mathscr{Q}.$