Summary and Strategies
When examining more complex propositional logic sequents, it can be challenging to know where to start. In this section, we summarize all available rules in propositional logic, and discuss stratgies for approaching proofs.
AND rules
Rule summaries:
P Q P ∧ Q P ∧ Q
∧i :  ∧e1 :  ∧e2 : 
P ∧ Q P Q
Rule syntax summaries:
{
...
x. p (...)
y. q (...)
z. p ∧ q ∧i x y
...
}
{
...
x. p ∧ q (...)
y. p ∧e1 x
z. q ∧e2 x
...
}
OR rules
Rule summaries:
{ P assume { Q assume
P Q P ∨ Q ... R } ... R }
∨i1 :  ∨i2 :  ∨e : 
P ∨ Q P ∨ Q R
Rule syntax summaries:
{
...
x. p (...)
y. p ∨ q ∨i1 x
...
}
{
...
x. q (...)
y. p ∨ q ∨i2 x
...
}
{
...
a. p ∨ q (...)
b. {
c. p assume
...
d. r (...)
}
f. {
g. q assume
...
h. r (...)
}
i. r ∨e a b f
...
}
Implies rules
Rule summaries:
{ P assume
P → Q P ... Q }
→e :  →i : 
Q P → Q
Rule syntax summaries:
{
...
x. p → q (...)
y. p (...)
z. q →e x y
}
{
...
a. {
b. p assume
///
c. q (...)
}
d. p → q →i a
}
Negation rules
Rule summaries:
{ P assume { ¬ P assume
P ¬ P ... ⊥ } ⊥e ... ⊥ }
¬ e :  ¬ i :  ⊥e :  pbc: 
⊥ ¬ P Q P
Rule syntax summaries:
{
x. p (...)
y. ¬ p (...)
z. ⊥ ¬ e x y
}
{
a. {
b. p assume
...
c. ⊥ (...)
}
d. ¬ p ¬ i a
}
{
x. ⊥ (...)
z. q ⊥e x
}
{
a. {
b. ¬ p assume
...
c. ⊥ (...)
}
d. p pbc a
}
Strategies
 Write down all premises first. Can you extract anything from the premises?
 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
 Look at the toplevel operator of what you are trying to prove.

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 propositions 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 an OR statement available? Try using OR elimination to prove your goal conclusion.
 Do your propositions 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
.
Proofs can be quite challenging. You might follow one approach, get stuck, and not be able to make progress. If this happens, backtrack and follow a different approach. If you are using Logika to verify your work, make sure it does not mark any lines in the proof in red – this means that you’ve made an invalid conclusion along the way, or that your justification for a particular line doesn’t follow the expected format. Try to fix these errors before continuing on with the proof.