Chapter 17.1-6: Basic Rules for TFL

The idea of a Formal Proof

• A formal proof/derivation is a sequence of sentences, some of which are marked as being initial assumptions (or premises)

• The last line of the formal proof is the conclusion

• Start proof by writing the premise

• Number every line of the proof

• Draw a line under the premise

Reiteration

• If you already have shown something in the course of a proof, the reiteration rule allows you to repeat it on a new line

• Write line number followed by “R” to indicate reiteration was used on a given line (Write this at the end of the line)

Conjunction

• Conjunctions can pull sentences from different parts of the proof together no matter the order (Conjunction introduction rule, bc introduces /\ symbol to proof)

• You can also choose to only include one component of a conjunction in the conclusion, in which case you are eliminating the conjunction symbol (Conjunction elimination rule)

• Write eliminated conjunctions as /\E at the end of the line (Take out other variable)

• Conjunction elimination rule can only be used when conjunction is the main logical operator

• For legibility purposes, you can drop outermost brackets in proofs

Conditional