LPL cover image

Fitch - Macintosh

Fitch is an application that makes it easy to construct formal proofs in first-order logic.

Getting started

We begin with instructions on how to start and stop Fitch , and explain the basic layout of the screen.

The Fitch application is contained inside the folder called Fitch Folder. Also in this folder is a folder called Fitch Exercise Files, in which you will find the exercise files referred to in the book.

When Fitch is running, you will see (from top to bottom) the ubiquitous narrow menu bar, a wider, gray “tool bar,” and a large, mostly blank window, called the “proof window,” with a blue “goal strip” at the bottom. Here are the basic facts to remember about each of these.

The menus

Fitch has the following menus:

The tool bar

The strip containing logical symbols and predicates located at the top of the proof window is called the “tool bar.” It is analogous to the Keyboard window in Tarski's World, and is used for writing and editing in the proof window. Moving your cursor over an item on the tool bar turns it into a button. Clicking on the button enters the symbol or predicate into the proof. The portion of the tool bar containing predicates can be scrolled back and forth using the double-arrow buttons on the tool bar. Try this so that you can see what is available. There are too many predicate and constant symbols to make them all visible at once.

On the far left of the tool bar are two buttons that are used to switch back and forth between two tools. You will normally use the top, pointer tool. The selection rectangle tool is used for cutting and pasting multiple steps in a proof.

On the far right of the tool bar are three buttons that allow you to check an individual step in your proof, verify the whole proof, or see the constraints on the goals of the proof.

The proof window

The proof window is itself divided into two areas. The larger top part or “pane” is where you construct proofs. When you add steps or subproofs to proofs, for example, this is where they will show up. When you add a step to a proof, the word Rule? appears on the right. This is a popup menu that you click on to choose the rule you want to use at the step.

The bottom pane of the proof window is where the problem's goals appear, that is, the sentences to be proven. If the goal strip is not visible, choose Show Goal Strip from the Goal menu. To hide it, and give yourself more room in the proof pane, choose Hide Goal Strip from the Goal menu.

At the extreme bottom of the proof window, under the goal strip, is a Status Line that displays comments and error messages. The status line is the bottom gray strip where you sometimes see scroll bars. It is initially blank, but it is used to present a lot of useful information, especially when proof steps don't check out. You can also check the step of the proof in focus by simply clicking on the status line.

Creating and editing proofs

The body of a proof appears in the large pane in the middle of the window, sandwiched between the tool bar and the goal strip. In this section, we explain how to create, modify, and navigate around a proof. Before doing this, we present a list of some of the graphical elements you will encounter in the proof pane:

Proof line and Fitch Bar. Proofs and subproofs are demarcated by a vertical gray line. Attached to the line is a horizontal bar called the Fitch bar. The bar separates the assumptions of the proof from the steps that follow from those assumptions.
Focus Slider. The focus slider appears just to the left of the proof and points to the currently focused step. If there are goals in the goal strip, the focus slider can also point at one of the goals. There is only one focus slider in the window at any time.
Step Bullet. This little square icon indicates the presence of a step in the proof. You can either add a new sentence at the step, if none is present, or you can edit an existing sentence. If step numbers are displayed (Show Step Numbers from the Proof menu), the step bullet is replace by the step number.
Goal Bullet. This “turnstile” icon precedes each of the goal sentences in the goal strip (unless one is in focus, in which case the turnstile is replaced by the focus slider).
Constant Box. The constant box appears at the top of subproofs in which a new constant or constants have been introduced. The constant box depicted here indicates that a is a newly introduced constant. The downarrow to its left indicates a menu where constants can be added or removed from this box.
Rule menu icon. This indicates a popup menu where you can choose a rule to justify a step of the proof.

Step numbers

Normally, Fitch does not display step numbers, but simply indicates the steps with bullets. Choosing Show Step Numbers from the Proof menu will replace the bullets with numbers. When you display step numbers, the support steps are indicated by number next to the rule name, exactly as they are shown in the text.

The current focus

As you work on a proof, there is always one step that is “in focus.” This step is indicated by a small triangle on the far left of the proof, called the Focus Slider. The focused step is the step affected when you perform any of the editing functions. It is also the step that is checked if you click on the Check Step button or on the status line at the very bottom of the proof window.

Moving the focus

There are three ways to change the focus from one step to another: You can drag the focus slider up and down, you can click in the focus slider area next to the step you want to focus on, or you can use the arrow keys on the keyboard to move the focus up and down.

Clicking on a step other than the currently focused step won't move the focus, unless you click in the focus slider area to the left. This is because clicking on steps is the way we enter supports for the currently focused step. (See Specifying a step's support)

Adding new steps

To add a new step to a proof, choose Add Step After or Add Step Before from the Proof menu. These commands will give you a new proof step immediately after or before the step you were focused on, unless you were focused on a premise, in which case the new step will be the first step following the premises. To add a step at the end of the proof, focus on the last step of the proof and choose Add Step After. If you are working backwards in a proof, you will often want to add a step immediately before the step in focus, using Add Step Before. Steps can be inserted in the middle of a proof in the obvious way, by first moving the focus and then choosing the appropriate add step command.

New steps added within a subproof will appear in the same subproof. Starting and ending subproofs require different commands. (See Starting and ending subproofs.) Adding premises to a proof is discussed here. Normally, though, you will not be adding premises to your proofs, since the exercise files contain the premises already.

Entering sentences into steps

When you add a new step to a proof, the step icon (a small box) will appear. At this point you can enter a sentence. To enter a sentence, either use the tool bar or type directly from the keyboard. To type the logical symbols from the keyboard, you can use these keyboard equivalents.

SymbolKeySymbolKey
~#
&|
$%
@/
_\
^

These are the same keyboard equivalents used in Tarski's World and Boole.

In general, entering sentences is faster using the tool bar. However some sentences must be entered using the keyboard, since the predicates, names, or sentence letters may not appear on the tool bar. For example, you will have to type parts of the sentence P (Q R), since P, Q, and R don't appear on the tool bar.

Deleting steps

To delete a step, focus on the step and choose Delete Step from the Proof menu. If you delete the assumption step of a subproof (the step just above the Fitch bar), the entire subproof containing that step will be deleted. Be careful in deleting assumption steps, since you could lose a lot of work. If you simply want to change the assumption, just edit the sentence.

You can either cut or delete a range of steps by using the selection rectangle on the tool bar. Use the rectangle tool to select the steps you want and then cut or delete them.

Specifying a step's rule

When you add a new step, the word “Rule?” appears to the right of the step. To specify a rule for the step, click down on the word “Rule?” A popup menu will appear. This menu has three submenus plus the rule of Reit.

The three submenus are attached to Intro, Elim, and Con. Moving the cursor over these submenus will cause a second menu to appear with a list of further options. To specify the rule of, say, Negation Introduction, first move the cursor over the item Intro. Then, when the second menu appears, move the cursor to the item $\neg$ (or “not”) and release the mouse button.

Similarly, to specify the rule of Taut Con, first move the cursor over the item Con and then choose Taut from the second menu.

You can also specify a rule from the keyboard, by typing the appropriate keystroke equivalent.

RuleEquivRuleEquiv
ElimOpt-& IntroShift-Opt-&
ElimOpt-| IntroShift-Opt-|
ElimOpt-~ IntroShift-Opt-~
ElimOpt-^ IntroShift-Opt-^
ElimOpt-$ IntroShift-Opt-$
ElimOpt-% IntroShift-Opt-%
= ElimOpt-== IntroShift-Opt-=
ElimOpt-@ IntroShift-Opt-@
ElimOpt-/ IntroShift-Opt-/
ReitOpt-RFO ConOpt-F
Taut ConOpt-TAna ConShift-Opt-A

Note that in using these keyboard equivalents, you should not hold down the shift key unless it is explicitly mentioned in the table. For example, to specify the rule $\forall$ Elim, you will actually type Option-2; holding down the shift key will change the rule to $\forall$ Intro instead. In most cases, we have listed the shifted (“uppercase”) characters because they are easier to remember. For example, it is easier to remember that $\wedge$ Elim is Option-& than to think of it as Option-7.

Changing a step's rule

To change the rule of an existing step, you must first move the focus to that step. Then specify the new rule using either the popup menu or the keystroke equivalents.

Specifying a step's supports

Most rules require that you cite other steps as justification or “support.” To specify the supports for a step, focus on that step and click on the steps to be cited. The steps you click on will highlight. If your support is a subproof, clicking anywhere in the subproof will highlight the whole subproof. If you click on a step or subproof that has already been cited, it will be uncited.

To see a step's supports, just focus on the step in question. The supporting steps will then become highlighted. To change a step's supports, focus on the step and click on the steps you wish to add or delete from the step's supports.

If you are displaying step numbers in a proof, then the support steps are not indicated with highlighting, but rather by step numbers appearing to the right of the rule name. Thus with step numbers displayed, your proofs will look like the proofs in the text.

Checking steps and verifying proofs

To check whether a step is correct, focus on the step and either press the Check Step button on the toolbar or click on the status line at the bottom of the window. You can also check a step by hitting the Enter key on the numeric keypad.

You can check all of the steps in your proof, plus the goals, by clicking Verify Proof on the toolbar or by choosing Verify Proof on the Proof menu.

After you check a step, one of four symbols will appear to the left of the rule name.

Check mark. A check mark means that the step is logically correct.
X. An X means that the step is logically incorrect.
Asterisk. An asterisk means that the sentence at that step is not syntactically well-formed.
Question mark. A question mark will appear if a Con rule is unable to determine thqe validity of your step.

If you don't get a check mark for one of your steps, focus on that step and look at the message in the status line. With luck, it will provide you with some helpful information about why your step did not check out.

Rule Defaults

Many of rules have defaults that can save you considerable time when constructing a proof. For example, if you choose the rule $\rightarrow$ Elim, cite two sentences of the form P Q and P, and then check the step, will automatically fill in the step with the sentence Q. To get to provide a default for a step, the sentence must be blank, that is, there must not be any text already in that step. If the sentence is blank when the step is checked, will try to provide a default sentence for that step. The defaults for the rules are described in detail in the textbook.

The Taut Con, FO Con, and Ana Con procedures do not have defaults.

Starting and ending subproofs

A subproof is started by choosing New Subproof from the Proof menu. When you start a new subproof, you can enter a sentence (or boxed constant) in the first step. Once you are within a subproof, any new steps you add will be part of that subproof. To add a step after a subproof, you need to know how to end the subproof. To end the subproof, focus on any step in the subproof and choose End Subproof from the Proof menu. This will end the subproof and give you a new step following that subproof.

If, when you end a subproof, the last step of the subproof is empty, then that step will just be moved out of the subproof. This means you can end two embedded subproofs by choosing End Subproof twice. The first time, you will end the innermost subproof and get a new step in the outer subproof. The second time, the new step will be shifted out of that subproof as well.

Boxed constants in subproofs

When you start a subproof, a downward-pointing triangle appears where the step bullet would normally appear. This triangle indicates the presence of a popup menu. If you click down on the triangle, the menu will appear. In this case, the menu presents you with a list of all the names available in . Choosing one of these names adds the name as a boxed constant--unless it is already boxed, in which case it is removed from the box. Boxed constants are used in the rules $\forall$ Intro, and $\exists$ Elim.

Deleting subproofs

To delete a subproof, focus on the assumption step that begins the subproof and choose Delete Step from the Proof menu. This will delete the entire subproof, so make sure you really want to do that. If you simply want to change the assumption step, edit the sentence, don't delete the step.

Goals

The goals for a problem are represented by sentences that appear in the goal strip at the bottom of the proof window. These are the sentences that are to be proven in your proof. If the goal strip is not visible and you would like it to be, choose Show Goal Strip from the Goal menu. If the goal strip is visible but you would like more room for the proof, choose Hide Goal Strip from the Goal menu.

When you are working on a problem and think that you have satisfied one or more of the goals, choose Verify Proof from the Proof menu. Either a check or an X will appear to the right of each goal. If an X appears, focus on the goal by clicking on it, and read the error message that will appear in the status bar.

Copying and pasting

Fitch allows you to cut, copy, and paste various parts of a proof. Mastering these operations will make the construction of proofs much easier.

When you cut or copy something from a proof, it is placed on the “clipboard.” The clipboard is a part of the computer's memory that you can't see, but which stores whatever you have cut or copied so you can later paste it somewhere else in the proof. The difference between cut and copy is that the former deletes the item in question from its current place in the proof, while the latter leaves the proof itself untouched, and stores a copy of the item on the clipboard.

Once something is on the clipboard, you can paste copies of it into the proof as many times as you want. It will remain on the clipboard until something else is cut or copied, at which point the new item replaces what used to be on the clipboard.

Copying and pasting sentences

To cut or copy a sentence, or part of a sentence, you must first be focused on the step that contains the sentence. Select the portion you want by clicking down at one end and dragging to the other, holding the mouse button down as you drag. Once it is selected, choose Copy or Cut from the Edit menu. Both of these commands place a copy of the selected text on the clipboard; the second simultaneously deletes it from the step.

If you want to copy an entire sentence from a step, you simply focus on the step and choose Copy from the Edit menu. There is no need to select the sentence. This places a copy of the whole sentence from that step on the clipboard, ready to paste elsewhere in the proof (or in another proof). This shortcut is particularly useful if you want to copy one of the premised when the authoring mode is off, for in that case the premise will be locked and you will not be able to select it.

Once the sentence is on the clipboard, you can paste it into another step by moving to that step and choosing Paste from the Edit menu. The text will appear wherever text typed from the keyboard would, so if you want to paste it into the middle of some existing text, make sure the blinking insertion point is located where you want the text to appear.

Copying and pasting goal sentences

You can copy a goal sentence by focusing on it and choosing Copy from the Edit menu. This is an easy way to grab the desired sentence and paste it into your proof.

Copying and pasting ranges of steps

Fitch allows you to cut or copy a range of steps and paste them at another location in the same proof or in another proof. This is especially useful if your proof requires several similar subproofs, each containing a similar sequence of steps.

To cut or copy steps, you must first select them using the selection rectangle tool on the far left of the tool bar. Its icon is a rectangle. When you choose on this button, you are ready to select a sequence of steps.

To select a sequence of steps, click down at the center of the first step in the sequence and drag straight down to the last step. A rectangle will appear, showing which steps are selected. If the rectangle doesn't contain the steps you want, click somewhere else in the proof and the rectangle will disappear. You can then try selecting the steps again. Note, however, that will not allow the selection rectangle to cut a subproof in half: you must either select steps entirely from within a subproof, or else select the subproof as a whole. When the rectangle contains exactly the steps you want, choose Cutor Copy from the Edit menu. Both of these commands place a copy of the steps on the clipboard; Cut also deletes the selected steps from the proof.

Once a sequence of steps is on the clipboard, choosing Paste will insert the steps at the point of focus. If you are currently focused on an empty step, the pasted steps will replace the empty step. If you are currently focused on a step that is not empty, the pasted steps will be inserted after the focused step.

If you want to paste steps into your proof immediately following a subproof, but not as part of the subproof, you will have to end the subproof before pasting. This will give you an empty step outside the subproof and Paste will replace this empty step with the steps on the clipboard.

When you paste steps into a proof, will try to keep track of the appropriate supports for those steps. Sometimes, though, the supports for the pasted steps will no longer be “legal” in the new location, for example if you paste a step into the proof at a point earlier than one of its support steps. In such cases, will remove the illegal support from the step's list of supports.

Note that the selection tool also gives you a handy way to delete a large number of steps. Rather than repeatedly choosing Delete Step from the Proof menu, simply select all of the steps you wish to delete, and choose Clear from the Edit menu. Simply hitting the Delete key will also delete the selected range of steps.

When you are finished with the selection tool, don't forget to go to the tool bar and switch back to the normal, pointer tool. While you have the selection tool, you will not be able to cite support steps.

Printing proofs

To print a proof, choose Print... from the File menu. When you do this, you will be given the standard print dialog box. Once you have chosen any printer options you want to use, click on the Print button in the dialog box. In the printed proof adds numbers to all of the steps and uses these numbers to indicate each step's supports so that the printed proofs look like the proofs in the textbook.

Setting up exercises

Fitch has two modes of operation, user mode and author mode. Students normally use the program in user mode, so exercise files are always opened in user mode. This mode allows you to construct proofs, but not to change the premises or goals of the proof, which of course is not permitted in solving the exercises. (The Grade Grinder always checks to make sure that no changes have been made to the premises or goals of a proof.)

Author mode is used for creating new exercises, and so new files are always opened in author mode. This mode allows you to enter premises into the proof, add goals to the proof, and specify any constraints that apply to the goals.

You can tell which mode you are in by looking at Author Mode on the Edit menu. If there is a check in front of Author Mode, is in author mode; otherwise, it is in user mode. Choosing Author Mode will toggle between these two modes.

The current mode is saved with the file, so if you create a new problem, you should turn off author mode before saving it. Alternatively, you can use Save As Problem... from the File menu. This will change the mode of the saved file to user mode.

Adding and deleting premises

To add a premise, you must be in Author Mode. Choose Add Premise from the Proof menu. If you are currently focused on a premise step, the new premise will appear immediately after the focused step. If you are focused on a step in the body of the proof, the new premise will appear at the end of the list of premises.

To delete a premise, focus on its step and choose Delete Step from the Proof menu.

Adding and deleting goals

To add a goal to a problem, choose New Goal from the Goal menu and enter the goal sentence you want. As noted above, this can only be done in Author Mode. To delete a goal from a problem, click on the goal in the goal strip and choose Delete Goal from the Goal menu.

If you want to modify the constraints on a goal, choose Edit Goal Constraints from the Goal menu. When you initially add a goal, assumes that you want the goal to be proven using just the introduction and elimination rules of . If you want to allow the use of the Con procedures, or if you want to disallow the use of any standard rules, you will have to modify the constraints associated with the goal. Constraints are associated with individual goals, so a problem can have different constraints for different goals.

Saving new problems

To save a newly created file as an exercise to be solved, choose Save As Problem... from the File menu. This saves the file, but also turns on User Mode in the file, so that users will not accidentally change the premises or goals of the exercise.

Educomm medal logo
Winners of the
1997 Educom Award
Language, Proof, and Logic  •  Tarski's World

The Openproof Project  •  CSLI  •  Stanford University  •  CSLI Publications

All pages and images on this website are copyright material. © The Openproof™ Project 2005-2009.