Fitch notation

Fitch notation, also known as Fitch diagrams (named after Frederic Fitch), is a method of presenting natural deduction proofs in propositional calculus and first-order logics using a structured, line-by-line format that explicitly shows assumptions, inferences, and their scope. It was invented by Frederic Brenton Fitch in the 1930s and later popularized through his textbook ''Symbolic Logic'' (1952). Fitch notation is notable for its use of indentation or boxes to indicate the scope of subordinate assumptions, making it one of the most pedagogically accessible systems for teaching formal logic.

History

Fitch developed his system of natural deduction as part of his doctoral work at Princeton University in 1934, under the supervision of Alonzo Church. His approach introduced the key idea of subordinate proofs, where assumptions could be opened within a subderivation and discharged later, such as when proving implications or negations. While his system was initially circulated in unpublished form, it became widely known through his book ''Symbolic Logic'', which was used extensively in undergraduate instruction.

Later logicians and educators such as Patrick Suppes and E. J. Lemmon rebranded Fitch's system. While they introduced graphical changes—such as replacing indentation with vertical bars—the underlying structure of Fitch-style natural deduction remained intact. These variations are often referred to as the Suppes–Lemmon format, though they are fundamentally based on Fitch's original notation.

Structure

Fitch notation presents proofs as a sequence of numbered lines, where each line includes:
* A logical formula
* A justification (a rule name and line references)
* Optionally, indentation or brackets to show the scope of assumptions

Example

Each row in a Fitch-style proof is either:
* an assumption or subproof assumption.
* a sentence justified by the citation of (1) a rule of inference and (2) the prior line or lines of the proof that license that rule.

Introducing a new assumption increases the level of indentation, and begins a new vertical "scope" bar that continues to indent subsequent lines until the assumption is discharged. This mechanism immediately conveys which assumptions are active for any given line in the proof, without the assumptions needing to be rewritten on every line (as with sequent-style proofs).

The following example displays the main features of Fitch notation:

0 , __                         ssumption, want P if not P1 ,    , __ P                   ssumption, want not P2 ,    ,    , __ not P           ssumption, for reduction3 ,    ,    ,    contradiction   ontradiction introduction: 1, 24 ,    ,    not not P           egation introduction: 2  , 
5 ,    , __ not not P           ssumption, want P6 ,    ,    P                   egation elimination: 5  , 
7 ,    P iff not not P         iconditional introduction: 1 - 4, 5 - 6

0. The null assumption, ''i.e.'', we are proving a tautology


1. Our first subproof: we assume the l.h.s. to show the r.h.s. follows


2. A subsubproof: we are free to assume what we want. Here we aim for a reductio ad absurdum


3. We now have a contradiction


4. We are allowed to prefix the statement that "caused" the contradiction with a not


5. Our second subproof: we assume the r.h.s. to show the l.h.s. follows


6. We invoke the rule that allows us to remove an even number of nots from a statement prefix


7. From 1 to 4 we have shown if P then not not P, from 5 to 6 we have shown P if not not P; hence we are allowed to introduce the biconditional in 7, where ''iff'' stands for ''if and only if''

Features

* Subordinate proofs: Nested derivations with temporarily assumed premises
* Assumption discharge: Explicit rules like $\to$ introduction and $\neg$ introduction for closing assumptions
* Line-referenced justification: Each step cites lines and rules used
* Human readability: The format closely mirrors natural informal reasoning

Comparison with Other Systems

* Gentzen-style natural deduction presents proofs as trees, with assumptions at the leaves and conclusions at the root. Unlike Fitch notation, it does not use subordinate boxes or indentation to manage temporary assumptions. Instead, all assumptions are explicitly present in the leaf nodes of the proof tree. This uniform treatment of assumptions makes Gentzen systems particularly well-suited to structural proof transformations and facilitates modularization and meta-theoretical analysis, such as cut-elimination.
* Hilbert system proofs rely on axioms and only a few inference rules, making them concise but abstract and less intuitive.
* The Suppes–Lemmon notation follows Fitch's logic and alters its visual layout for typesetting and instructional clarity.

Influence

Fitch notation is widely used in logic textbooks and teaching. It also underlies several proof assistant tools. Its structured style has become a standard for teaching formal logic in undergraduate education.

See also

* Natural deduction
* Frederic Fitch
* Sequent calculus
* Proof theory
* Hilbert system
* Suppes–Lemmon notation

Notes

References

*

*
*
*

External links

*
*
*
* (see Jape)
* (see LaTeX)
*
* {{cite web, url=https://proofs.openlogicproject.org/, title= Natural deduction proof editor and checker in Fitch notation, access-date=2025-05-06

Philosophical logic
Logical calculi