BULLET PROOFS: Chapter 4

Basically the bullet proofs leave out the meat of a proof and just give you the bones so
• Inside the
`=<...>`
we need only list the theorem, or theorem number, not forgetting our
`|-`
and we need not mention the use of inference rules anywhere.
• For style 4.1 we now do not need to worry about the part of the proof after the "=<...>" bit of the proof i.e. no need to mention transitivity, or the derived inference rules for
`=>`
at the end.
• For the deduction theorem, if proving
`|- P_1 ^P_2^...^P_n => Q`
we only need to say "assume P_1, P_2,...,P_n" and then give a bullet proof of Q. That's all.
• For proof by cases, since we don't mention substitutions in bullet proofs, just bullet prove the theorem with true already substituted in, and then give a bullet prof of the theorem with false already substitued in. That's all.

Remember to substitute the same variable each time.

• For the other types (contrapositive, contradiction etc) we are just trying to prove say A is a theorem, from which we can deduce B is a theorem by (contradiction, contrapositive, whatever). For this all we have to do is give a bullet proof that A is a theorem.

Stephanie van Willigenburg