Fitch-style calculus, also known as Fitch diagrams (named after Frederic Fitch), is a method for constructing formal proofs used in first-order logic. Fitch-style proofs involve the atomic sentences of first order logic, which are arranged in premises, lemmas, and subproofs.
Each step in a Fitch-style proof, except premises and subproof premises, requires a citation of a rule of first-order logic in order to justify the step. After a step is justified, then another step may be constructed upon this, until a desired conclusion has been reached.
This illustrates the use of subproofs
0 | [assumption] 1 | |__ P [assumption] 2 | | |__ not P [assumption] 3 | | | contradiction [contradiction introduction: 1, 2] . | | <----------------- end subproof 4 | | not not P [negation introduction: 2] . | <--------------------- end subproof 5 | |__ not not P [assumption] 6 | | P [negation elimination: 5] . | <--------------------- end subproof 7 | P iff not not P [biconditional 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
3. We have introduced a contradiction since we have "a statement" and not "a statement"
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 Fitch 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
- Jon Barwise and John Etchemendy, Language, Proof and Logic 1st edition as PDF, Seven Bridges Press and CSLI, 1999.