Summary and Strategies
In this section, we summarize all available rules in propositional logic, and discuss strategies for approaching proofs.
Rules with universal quantifier (∀
)
Rule summaries:
∀ x P(x)
∀e: 
P(v) where v is a particular individual in the domain
{ a (a is fresh)
... P(a) }
∀i: 
∀ x P(x)
Rule syntax summaries:
{
...
r. ∀ x P(x) (...)
s. P(v) ∀e r v
...
}
{
...
r. {
s. a
...
t. P(a) (...)
}
u. ∀ x P(x) ∀i r
}
Rules with existential quantifier (∃
)
Rule summaries:
P(d) where d is an individual
∃i: 
∃ x P(x)
{a P(a) assume // where a is a new, fresh name
∃ x P(x) ... Q } // a MUST NOT appear in Q
∃e: 
Q
Rule syntax summaries:
{
...
r. P(d) (...)
s. ∃ x P(x) ∃i r d
...
}
{
...
b. ∃ x P(x) (...)
c. {
d. a P(a) assume
...
e. Q (...)
}
f. Q ∃e b c
}
Reminder: propositional logic rules are still available
When doing proofs in predicate logic, remember that all the deduction rules from propositional logic are still available. You will often want to use the same strategies we saw there – not introduction to prove a NOT, implies introduction to create an implies statement, OR elimination to process an OR statement, etc.
However, keep in mind that propositional logic rules can only be used on claims without quantifiers as their toplevel operator. For example, if we have the statement ∀ x (S(x) ∧ Pz(x))
, then we cannot use ∧e
– the toplevel operator is a universal quantifier, and the ∧
statement is “bound up” in that quantifier. We would only be able to use ∧e
after we had used ∀ e
to eliminate the quantifier.
Strategies

Write down all premises first. Can you extract anything from the premises?
 If you have a forall statement and an available individual, use
∀e
to plug that individual into the forall statement.  If you have
p∧q
, use∧e1
to extractp
by itself and then∧e2
to extractq
by itself.  If you have
p→q
andp
, use→e
to getq
.  If you have
p
and¬p
, use¬e
to claim a contradiction,⊥
.
 If you have a forall statement and an available individual, use

Look at the toplevel operator of what you are trying to prove.

Are you trying to prove something of the form
∀ x P(x)
? Use
∀i
. Open a subproof, introduce a fresha
, and get toP(a)
by the end of the subproof. After the subproof, use∀i
to conclude∀ x P(x)
.
 Use

Are you trying to prove something of the form
∃ x P(x)
? You will usually have another thereexists (
∃
) statement available as a premise or previous claim. Open a subproof, and assume an alias for the individual in your thereexists statement. Get to∃ x P(x)
by the last line of the subproof. After the subproof, use∃e
to restate∃ x P(x)
.
 You will usually have another thereexists (

Are you trying to prove something of the form
p→q
? Use
→i
. Open a subproof, assumep
, and get toq
by the end of the subproof. After the subproof, use→i
to concludep→q
.
 Use

Are you trying to prove something of the form
¬p
? Use
¬i
. Open a subproof, assumep
, and get a contradiction,⊥
, by the end of the subproof. After the subproof, use¬i
to conclude¬p
.
 Use

Are you trying to prove something of the form
p ∧ q
? Try to prove
p
by itself and thenq
by itself. Afterward, use∧i
to concludep ∧ q
.
 Try to prove

Are you trying to prove something of the form
p ∨ q
? See if you have either
p
orq
by itself – if you do, use either∨i1
or∨i2
to concludep ∨ q
.
 See if you have either


You’ll need to nest the approaches from step 2. Once you are in a subproof, think about what you are trying to prove by the end of that subproof. Follow the strategy in step 2 to prove your current goal, nesting subproofs as needed. As you work, stop and scan the claims that you have available. See if you can extract anything from them as you did for the premises in step 1.

No match, or still stuck?
 Do you have a thereexists statement available? Try using
∃e
to reach your goal.  Do you have an OR statement available? Try using OR elimination to prove your goal conclusion.
 Do your statements have NOT operators, but don’t fit the form for using
¬i
? Try usingpbc
. If you are trying to prove something of the formp
, open a subproof, assume¬p
, and try to reach a contradiction by the end of the subproof. Afterward, usepbc
to concludep
.  As a last resort, try pasting in the proof for the law of the excluded middle (see section 4.5). Then use OR elimination on
p ∨ ¬p
.
 Do you have a thereexists statement available? Try using
Think of doing a proof as solving a maze, and of all our deduction rules as possible directions you can turn. If you have claims that match a deduction rule, then you can try applying the rule (i.e, “turning that direction”). As you work, you may apply more and more rules until the proof falls into place (you exit the maze)…or, you might get stuck. If this happens, it doesn’t mean that you have done anything wrong – it just means that you have reached a dead end and need to try something else. You backtrack, and try a different approach instead (try turning in a different direction).