Fitch-style calculus

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.

Example

This illustrates the use of subproofs

0                     [assumption]

  1 P                 [assumption]
    2  not P          [assumption]
    3  contradiction  [contradiction introduction: 1, 2]
  4  not not P        [negation introduction: 2]

  5  not not P        [assumption]
  6  P                [negation elimination: 5]

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 P oif not not P, from 5 to 6 we have shown P if not not P; hence we are allowed to introduce the biconditional

Related

• Stanford University has produced an application called "Fitch ".

• An online Java application for proof building is also available .

• Johan W. Klüwer has made a LaTeX package for typesetting fitch-style proofs (guide).

• A Web implementation of Fitch proof system (propositional and first-order) is available at http://www.proofmood.com/

• Richard Bornat and Bernard Sufrin produced, and still maintain, a general-purpose proof assistant, Jape, that will display proofs, including partially constructed proofs, in the Fitch style. It is available at http://japeforall.org.uk.

See also

• Natural deduction

References

• Jon Barwise and John Etchemendy, Language proof and logic, Seven Bridges Press and CSLI, 1999.

External links

• Fitch Calculus
• Fitch's Paradox of Knowability