Be-Fitched!

Constructing proofs using the Fitch system can often be hard and unintuitive, especially for those who encounter it for the first time. We have identified the following guidelines which are based on the properties of the Goal or of the Premises that could potentially help you with Fitch-style proofs.

Guidelines based on propeties of the Goal:

1. Goal is of the form φ ⇒ ψ
   • Assume φ
   • Prove ψ
   • Apply Implication Introduction to prove φ ⇒ ψ


2. Goal is of the form ¬φ
   • Assume φ
   • Find a sentence ψ
     • Prove φ ⇒ ψ
     • Prove φ ⇒ ¬ψ
   • Apply Negation Introduction to prove ¬φ

   The idea behind G2 is to assume φ and show that this leads to a contradiction i.e. ψ and ¬ψ. Good candidates for ψ when applying Negation Elimination on φ ⇒ ψ and φ ⇒ ¬ψ are the premises or the assumptions (for the sub-proof).

   Consider the following example.
   Premises: q, p ⇒ ¬q
   Goal: ¬p
   Keys to applying G2 to this example is to
   • Use φ = p
   • Find a suitable ψ to prove p ⇒ ψ, and p ⇒ ¬ψ
   Since p ⇒ ¬q is available as a premise (we don’t need to prove it!), if use ψ = q and prove p ⇒ q, then by applying Negation Introduction, we can prove ¬ p. Proving p ⇒ q is quite trivial at this point using G1 and Reiteration.
   


3. Goal is of the form φ (with no negation on the outside)
   • Assume ¬φ and proceed in a manner similar to G2 (see above) to prove ¬¬φ
   • Apply Negation Elimination on the result ¬¬φ to prove φ


4. Goal is of the form φ₁ ∨ φ₂ … ∨ φ_n
   • Prove any φ_i (1 ≤ i ≤ n)
   • Apply OR Introduction to prove φ₁ ∨ φ₂ … ∨ φ_n


5. Goal is of the form φ₁ ∧ φ₂ … ∧ φ_n
   • Prove φ_i for every i, 1 ≤ i ≤ n
   • Apply AND Introduction to prove φ₁ ∧ φ₂ … ∧ φ_n

Guidelines based on propeties of Premises:

1. There exists a Premise of the form φ ⇒ ψ and the Goal is ψ
   • Prove φ
   • Apply Implication Elimination on φ and φ ⇒ ψ to prove ψ
   This strategy can be seen as a dual of the strategy G1.


2. There exists a Premise of the form φ₁ ∨ φ₂ … ∨ φ_n and the Goal is ψ
   • Prove φ_i ⇒ ψ for every i, 1 ≤ i ≤ n
   • Apply OR Elimination to prove φ₁ ∨ φ₂ … ∨ φ_n ⇒ ψ
   • Apply Implication Elimination on the above result and the premise to prove ψ

Comprehensive example

• We can apply either of G3 (since goal has no negations on outside) or P2 (a premise is of the form φ₁ ∨ φ₂ … ∨ φ_n).
• Applying G3 at the start takes us to a dead-end.
• However, if we apply P2, we have to prove p ⇒ q and q ⇒ q (the latter is trivial!).
• To prove p ⇒ q we apply G1 i.e. start by assuming p. We have to prove q given the premises p ∨ q and ¬p and the assumption p.
• NOW, we can apply the strategy G3 (which earlier led us to a dead-end). The remainder of the proof is left as an exercise for the reader.

REMEMBER:

• Apply G1-G5 to reverse-engineer which sub-goals to prove prior to proving the goal.
• Apply P1-P2 to figure out which sub-goals to prove next starting from the premises or an assumption (in case of a sub-proof).