Natural Deduction Rules for Monadic Predicate Logic
(Revised 5 January 2011)


Quantifier Rules


E (Universal Quantifier Elimination)
For any variable v and constant c,
if you have derived vφ,
then you can write down φv/c,
depending on everything vφ depends on.


I (Existential Quantifier Introduction)
For any variable v and constant c,
if you have derived φv/c,
and vφ is a well-formed formula of MPL,
then you can write down vφ,
depending on everything φv/c depends on.


I (Universal Quantifier Introduction)
For any variable v and constant c,
if you have derived φv/c, and c does not occur in φ,
and c does not occur in anything φv/c depends on,
and vφ is a well-formed formula of MPL,
then you can write down vφ,
depending on everything φv/c depends on.


E (Existential Quantifier Elimination)
For any variable v and constant c,
if you have derived vφ, assumed φv/c, and derived ψ,
and c does not occur in ψ, φ, or anything ψ depends on (except φv/c),
then you can write down ψ a second time, depending on everything
the first ψ depends on (except the assumption φv/c) together with
everything vφ depends on.


Connective and other rules

A (Rule of Assumption)
You can write down any MPL wff, depending on itself.


&I (Conjunction Introduction)
If you have derived φ and ψ,
you can write down (φ&ψ),
depending on everything φ and ψ depend on.


&E (Conjunction Elimination)
If you have derived (φ&ψ),
you can write down φ or ψ,
depending on everything (φ&ψ) depends on.


I (Conditional Introduction)
If you have assumed φ, and you have derived ψ,
you can write down (φψ),
depending on everything ψ depends on except φ.


E (Conditional Elimination or Modus Ponens)
If you have derived (φψ) and φ,
you can write down ψ,
depending on everything (φψ) and φ depend on.


~I (Negation Introduction)
If you have assumed ψ, and you have derived (φ&~φ),
then you can write down ~ψ,
depending on everything (φ&~φ) depends on except ψ.


~E (Negation Elimination)
If you have assumed ~ψ, and you have derived (φ&~φ),
then you can write down ψ,
depending on everything (φ&~φ) depends on except ~ψ.


I (Disjunction Introduction)
If you have derived φ,
you can write down (φψ) or (ψφ),
depending on everything φ depends on.
(ψ is any MPL wff.)


E (Disjunction Elimination or Disjunctive Syllogism)
If you have derived (φψ) and ~ψ,
you can write down φ,
depending on everything (φψ) and ~ψ depend on.

If you have derived (φψ) and ~φ,
you can write down ψ,
depending on everything (φψ) and ~φ depend on.


PC (Proof by Cases)
If you have derived (φψ) and (φα) and (ψβ),
then you can write down (αβ),
depending on everything (φψ) and
α) and (ψβ) depend on.


I (Biconditional Introduction)
If you have derived ((φψ)&(ψφ)),
you can write down (φψ),
depending on everything ((φψ)&(ψφ)) depends on.


E (Biconditional Elimination)
If you have derived (φψ),
you can write down ((φψ)&(ψφ))
depending on everything (φψ) depends on.