How to construct a proof with Fitch

Enter the premises (use Crtl-R to separate them if there is more than one).
After entering the premises, add a proof step with Crtl-A.
For each proof step, either apply a rule, or enter a new subproof with Crtl-E
If you want to apply a rule,

enter the sentence that you want to derive
choose the rule (click with the mouse on the trianlge)
and choose the support (click onto sentences and subproofs with the mouse, they will be hightlighted in blue). The support may cite only sentences in the current (sub)proof or in proofs at a higher level.
click "Check step". If you get an X, the step is logically not correct. If you get a *, the sentence is not well-formed.

If you want to enter a new subproof,
- type Crtl-P
- proceed as described in "How to construct a proof with Fitch"
  (notice: sometimes you will not need any assumption in the subproof, but just introduce a local constant, to be used with the quantifier rules. This can be done by clicking to the left of the cursor after having entered the subproof.)
- type Ctrl-E
Now you can either add the next proof step with Ctrl-A an go to step 3. above...
...or, if you have reached your final goal, your proof is ready.

It is often advisable not to proceed step by step. Instead, look also at the goal that you want to show. This may give you hints how to proceed. Then you can create the overall structure of the proof, and later fill in the holes.

Moving the focus: either with the up and down keys, or by klicking to the left of the vertical line.

Deleting steps: with Ctrl-D.

If the program hangs, often Ctrl-A Ctrl-D helps.

If the program crashes (which sometimes may happen), create a new shell and type "pkill wine". If this does not help, type "pkill -9 wine".

Proof strategies

General remark: First, try to construct an informal proof. It will guide you when formalizing it.
Look at the proof rules (the are summarized in the book on page 557 ff.)
Try out to design a general strategy. Sometimes, it is advisable to look at the premises and look at the rules: which rules can be used to infer something from the premises. Sometimes, it is advisable to work backwards and look at the conclusion first: which rule can be used to infer the conclusion?
Strategies for the boolean connectives: see section 6.5 of the LPL book
Strategies for quantifiers: see here (with thanks to Richard Zach)