Anyone who is familiar with Natural deduction will understand the proof without great difficulty. And he/she may wonder whether there is any essential difference between Fitch and the Natural deduction.
This brief manual assumes that you have read the help page for Truth Table in Proofmood. Also we assume that you have a nodding knowledge on formal proof systems such as Hilbert-Frege or Natural Deduction. Knowledge on Fitch system will certainly help but are not required.
Fitch system resembles the Natural deduction system in that it does not have any logical axioms--it only has inference rules. Each formula in a Fitch proof occupies a node in a tree: again this resembles the Natural deduction system. What characterizes, and distinguishes Fitch system from Natural deduction system is that a node in a proof tree may be labeled with a subproof as well as a formula. Subproofs effectively eliminates the need for the nasty business of discharging hypotheses.
A sample Fitch proof is given at the right. Anyone who is familiar with Natural deduction will understand the proof without great difficulty. And he/she may wonder whether there is any essential difference between Fitch and the Natural deduction.
To see the difference, look at the second example, which should be more interesting. Again this proof is not too difficult to follow. And I believe that it is considerably more difficult to construct this proof of
A → B ∨ C ├ (A → B) ∨ (A → C)
in other proof systems.
As you may have noticed, the tree in Fitch system is not just a tree--its order relation extends that of a tree in such a way that elder sibling is less than its younger siblings. For a formula in a node to use other nodes(lines or subproofs) as its premises, the position of the node must be "bigger than" those of the premise nodes.
Constructing Fitch derivations, aka Fitch formal proofs, needs some practice. I hope that the learning process is a pleasant experience, rather than a painful one.
Constructing a Fitch derivation is one thing and editing the derivation is another. A short manual like this is not suitable for explaining how to construct Fitch derivations. And a logician should be able to figure it out by him/herself.
Editing a derivation is of course specific to this particular software in Proofmood, and I'll explain briefly the basic and important stuffs about editing.
Editing formulas will pose no difficulties if you have read the help page for Truth Table. In order to introduce subproofs you just click the commands such as [Add Subproof] and [Insert Subproof]. Among the 10 commands, two need explanations, I think. One is [Add conclusion]. Here, the term 'conclusion' means any formula that is not a hypothesis. This command is used when you want to get the derivation in the right hand side from the one in the left hand side.
The other is [End Subproof]. This command is used when you want to get the derivation in the right hand side from the one in the left hand side.
Observe, in the example above, that the boundary of the subproof that contains the focused line (line #5 in the left derivation) is pink-colored.
Annotations such as ∨ elim 15-16,9-14,8 shown on line 17 in the (relatively long) proof given above is entered by entering the inference rule and entering the premises separately. Inference rules can be altered by clicking the current rule. When no rule is given, [Rule ?] will be shown there and you just click on it to designate an inference rule that was used to infer the line. Premises can be given by right-clicking the leftmost part of the premise line. When you move the mouse to the clicking zone at the leftmost part of the line, the shape of the mouse cursor changes and you can't miss it.
Like I said before, premises consist of lines and subproofs. If you right-click the clicking zone, the line number is added to the annotation of the currently focused line. If you click again, the premise is deleted. If you shift-right-click any line that contains the subproof n-m that you want designate as a premise, the n-m enters the annotation: here, n is the line number of the starting line of the subproof and m is the line number of the ending line.
It is important to note the difference between a comma and a dash in annotations. For instance, 3,5 means line 3 and line 5, and 3-5 means a subproof starting from line 3 and ending at line 5.
Finally, the Fitch derivation currently shown on the screen can be exported in two forms: one is a string that encodes the entire derivation. The other is the familiar LaTeX source, and I don't think I have to explain this again. The former is obtained by clicking [Output]. The encoded string will be shown in a pop-up window. Don't worry if you do not understand the string--it's for the computer, and not for human. You "select" this string by Ctrl-A or other standard trick for "selection". Then copy the selection into buffer by Ctrl-C. Then you can save the string by pasting the buffer into a text file, using your favorite text editor or word processor.
The encoded string can be decoded and shown on the screen by clicking [Input] and pasting it onto the pop-up window and then clicking [Go].
| intro | elim | intro | elim | ||
| ￢ |  |
 |
→ |  |
 |
| ∧ | 
 |
 |
↔ |  |
 |
| ∨ | 
 |
 |
⊥ |  |
 |
| Repeat |  |
LEM |  | ||