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: T) => P(x))
AllE[T]: 
P(v) where v is a particular individual in the domain (i.e, v has type T)
Let ( (a: T) => SubProof(
...
P(a)
)),
AllI[T] : 
∀ ((x: T) => P(x))
Rule syntax summaries:
(
...
r ( ∀ ((x: T) => P(x)) ) by SomeJustification,
s ( P(v) ) by AllE[T](r), //where v has been previously shown to have type T
...
)
(
...
r Let ( (a: T) => SubProof( //where a is a fresh, previously unused, individual
...
t ( P(a) ) by SomeJustification
)),
u ( ∀ ((x: T) => P(x)) ) by AllI[T](r),
)
Rules with existential quantifier (∃
)
Rule summaries:
P(d) where d is an individual of type T
ExistsI[T]: 
∃((x: T) => P(x))
Let ((a: T) => SubProof( // where a is a new, fresh name
Assume( P(a) ), // a MUST NOT appear in Q
∃((x: T) => P(x)) ...
Q
)),
ExistsE[T]: 
Q
Rule syntax summaries:
(
...
r ( P(d) ) by SomeJustification, //where d has been shown to have type T
s ( ∃((x: T) => P(x)) ) by ExistsI[T](r),
...
)
(
...
b ( ∃((x: T) => P(x)) ) by SomeJustification,
c Let ( (a: T) => SubProof( //where a is a previously unused individual
d Assume( P(a) ),
...
f ( Q ) by SomeJustification //where a does NOT appear in Q
)),
g ( Q ) by ExistsE[T](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: T) => (S(x) ∧ Pz(x)) )
, then we cannot use AndE
– the toplevel operator is a universal quantifier, and the ∧
statement is “bound up” in that quantifier. We would only be able to use AndE
after we had used AllE[T]
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
AndE[T]
to plug that individual into the forall statement.  If you have
p∧q
, useAndE1
to extractp
by itself and thenAndE2
to extractq
by itself.  If you have
p →: q
andp
, useImplyE
to getq
.  If you have
p
and¬p
, useNegE
to claim a contradiction,F
.
 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: T) => P(x))
? Use
AllI[T]
. Open a subproof, introduce a fresha
, and get toP(a)
by the end of the subproof. After the subproof, useAllI[T]
to conclude∀ ((x: T) => P(x))
.
 Use

Are you trying to prove something of the form
∃((x: T) => P(x))
? You will often 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: T) => P(x))
by the last line of the subproof. After the subproof, useExistsE[T]
to restate∃((x: T) => P(x))
.
 You will often have another thereexists (

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

Are you trying to prove something of the form
¬p
? Use
NegI
. Open a subproof, assumep
, and get a contradiction,F
, by the end of the subproof. After the subproof, useNegI
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, useAndI
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 eitherOrI1
orOrI2
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
ExistsE[T]
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).