Fitch-style calculus
From Wikipedia, the free encyclopedia
Fitch-style calculus is a method for constructing formal proofs used in first-order logic. It was invented by American logician Frederic Brenton Fitch. 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.
Contents |
[edit] 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
[edit] Related
- Stanford University has produced an application called "Fitch".
- An online Java application for proof building is also available [1].
[edit] References
- Jon Barwise and John Etchemendy, Language proof and logic, Seven Bridges Press and CSLI, 1999.
