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
Illustrated below is the simplest example of a proof known as “Reductio ad absurdum” which in Latin is “reduction to the absurd”. The argument is shown on the left, where the rules are cited on the right.
- ~P --> Q
- ~Q
- ~P
- Q --> Elim (1,3)
- “absurdity” “absurdity” Intro (2,5)
- ~~P ~ Intro (3—5)
- P ~ Elim 6
[edit] Related
- Stanford University has produced an application called "Fitch".
- An online Java application for proof building is also available http://logik.phl.univie.ac.at/~chris/gateway/formular-uk-fitch.html.
[edit] References
- Jon Barwise and John Etchemendy, Language proof and logic, Seven Bridges Press and CSLI, 1999.
