Fitch-style calculus

From Wikipedia, the free encyclopedia
Jump to: navigation, search

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

See also[edit]


External links[edit]