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).^[1] 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.

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,^[1] which was used extensively in undergraduate instruction.

Later logicians and educators such as Patrick Suppes^[2] and E. J. Lemmon^[3] 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.

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

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 |__                        
1 |   |__ P                  
2 |   |   |__ not P          
3 |   |   |   contradiction  
4 |   |   not not P          
  |
5 |   |__ not not P          
6 |   |   P                  
  |
7 |   P iff not not P        

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

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

• 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.

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.

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

• Fitch, Frederic Brenton (1952). Symbolic Logic: An introduction. New York: The Ronald Press Company. LCCN 52006196.

• Barker-Plummer, Dave; Barwise, Jon; Etchemendy, John (2011) . Language, Proof and Logic (2 ed.). CSLI Publications. p. 606. ISBN 9781575866321.
• Lemmon, E. J. (1965). Beginning Logic. Nelson.
• Suppes, Patrick (1957). Introduction to Logic. Van Nostrand.

• Brogaard, Berit; Salerno, Joe (Fall 2019). "Fitch's Paradox of Knowability". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy.
• "An online Java application for proof building". Archived from the original on 2 October 2006. Retrieved 6 May 2025.
• "A Web implementation of Fitch proof system (propositional and first-order)". proofmod.mindconnect.cc. Retrieved 6 May 2025.
• "The Jape general-purpose proof assistant". GitHub. Retrieved 6 May 2025. (see Jape)
• "Resources for typesetting proofs in Fitch notation with LaTeX". Logic Matters. Retrieved 6 May 2025. (see LaTeX)
• "FitchJS: An open source web app to construct proofs in Fitch notation (and export to LaTeX)". Retrieved 6 May 2025.
• "Natural deduction proof editor and checker in Fitch notation". Retrieved 6 May 2025.