Transformational Proof (Predicate Logic)

Builds off of Transformational Proof in Propositional Logic.

List of Additional Rules

  • forall_over_and
  • exists_over_or
  • move_exists
    • where is not free in
  • move_forall
    • where is not free in
  • dm
  • swap_vars

Property

Natural deduction proofs for predicate logic are sound but incomplete, so we usually prefer natural deduction instead.

Example

Prove with Set Theory:

We will prove:

proof

Tip

Shortcut: to prove , instead of proving , prove

Example

Prove with set theory:

We will prove:

proof