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 1 Example 2 Related 3 References 4 External links

[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.

1. ~P --> Q
2. ~Q
3. ~P
4. Q --> Elim (1,3)
5. “absurdity” “absurdity” Intro (2,5)
6. ~~P ~ Intro (3—5)
7. 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.

[edit] External links

• http://www.cc.utah.edu/~nahaj/logic/structures/systems/fitch.html
• http://plato.stanford.edu/entries/fitch-paradox/