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:
Each row in a Fitch-style proof is either:
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 |__ [assumption, want P if not P] 1 | |__ P [assumption, want not P] 2 | | |__ not P [assumption, for reduction] 3 | | | contradiction [contradiction introduction: 1, 2] 4 | | not not P [negation introduction: 2] | 5 | |__ not not P [assumption, want P] 6 | | P [negation elimination: 5] | 7 | P iff not not P [biconditional introduction: 1 - 4, 5 - 6]
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.
