Fitch is a browser-based editor for constructing Fitch-like proofs in Herbrand Logic. It provides basic editing commands for constructing such proofs; it allows users to copy and paste proofs between browser windows; and it allows users to save proofs to local files and to read proofs from local files.


The syntax used by Fitch is a variant of the traditional syntax for Herbrand Logic that uses only Ascii characters. The editor uses ~ for ¬; use & for ∧; use | for ∨; use => for ⇒; use <=> for ⇔; use A for ∀; use E for ∃; and use : for . in quantified sentences. Also, for variables it uses strings of alphanumeric characters that begin with a capital letter. For example, to write the sentence ∀x.∃y.(p(x) ∧ q(y) ⇒ r(y)∨¬s(y)) is written AX:EY:(p(X)&q(Y)=>r(Y)|~s(Y)).

Editing Commands

The Premise button allows you to add a top-level premise to a proof. Reiteration allows you to repeat an earlier item. The Truthtable button allows you to add conclusions that are logically entailed by checked premises based on truthtable analysis. The Shortcut button allows you to add conclusions that are proved in other proof buffers. (See below.) To delete one or more lines from a proof, check the desired lines and click Delete. Note that any dependent results will also be deleted. The Replace button allows you to replace all occurrences of a symbol with an arbitrary expression. The Coalesce button merges each checked line in a proof (the result) with an earlier line (the source).

Rules of Inference

To apply a rule of inference, check the lines you wish to use as premises and click the button for the desired rule of inference. In some cases, a dialog box will appear to allow you to enter additional data. Note that the Assumption button is special in that it allows you to create an assumption context. Implication Elimination is greyed out unless you are in the context of an assumption.

Domain Closure is enabled once you enter sentences containing object constants provided that there are no function constants. Induction is enabled once you enter sentences containing functions constants. The lines at the top of each proof indicate the object constants and function constants that occur somewhere in the proof.

Changing Insertion Point

If you want to change the insertion point for results, click on the line number where you would like to insert your results. This will move the insertion point to that line and add a blank line to show the location of the insertion point. Clicking on the blank line will move the insertion point back to the end of the proof. Note that, when the insertion point is located anywhere but the end of a proof, some operations are disabled - you can add a premise or reiterate or add a truth table conclusion or a shortcut but other rules of inference are disabled as they can easily lead to malformed proofs.


Clicking the Undo button replaces the current proof with the proof that existed just prior to the most recent operation. At present, Undo goes back just one step, i.e it does not save an entire history.

Copy and Paste

Fitch allows you to develop multiple proofs at the same time in different windows and to copy and paste proofs across multiple windows. To copy a proof to the clipboard, select the lines you want copied and press the Copy button. (Note that any lines that do not have justifications in the set of selected lines are converted to premises in the copy placed on the clipboard.) To insert a proof from the clipboard into another proof, press the Paste button. You can then use the Coalesce button to merge lines from the pasted proof with lines in the proof into which it is pasted.

Save and Load

The Save button saves the proof to a file of your choice on your local disk. To reload a proof saved in this way, press the Load button and select the filename of the proof you want to load. Fitch will read that proof and enter it into the proof editor (overwriting the current contents).

Comments and complaints to genesereth@stanford.edu.