Fitch-style calculus
Encyclopedia
Fitch-style calculus, also known as Fitch diagrams (named after Frederic Fitch), 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 sentence
s 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.
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
Formal proof
A formal proof or derivation is a finite sequence of sentences each of which is an axiom or follows from the preceding sentences in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a formal system...
used in first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
. It was invented by American logician Frederic Brenton Fitch
Frederic Brenton Fitch
Frederic Brenton Fitch was an American logician, the inventor of Fitch-style calculus, and a Sterling Professor Emeritus at Yale University...
. Fitch-style proofs involve the atomic sentence
Atomic sentence
In logic, an atomic sentence is a type of declarative sentence which is either true or false and which cannot be broken down into other simpler sentences...
s of first order logic, which are arranged in premises, lemmas
Lemma (mathematics)
In mathematics, a lemma is a proven proposition which is used as a stepping stone to a larger result rather than as a statement in-and-of itself...
, 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
Tautology (logic)
In logic, a tautology is a formula which is true in every possible interpretation. Philosopher Ludwig Wittgenstein first applied the term to redundancies of propositional logic in 1921; it had been used earlier to refer to rhetorical tautologies, and continues to be used in that alternate sense...
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 UniversityStanford UniversityThe Leland Stanford Junior University, commonly referred to as Stanford University or Stanford, is a private research university on an campus located near Palo Alto, California. It is situated in the northwestern Santa Clara Valley on the San Francisco Peninsula, approximately northwest of San...
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.
- Johan W. Klüwer has made a LaTeXLaTeXLaTeX is a document markup language and document preparation system for the TeX typesetting program. Within the typesetting system, its name is styled as . The term LaTeX refers only to the language in which documents are written, not to the editor used to write those documents. In order to...
package for typesettingTypesettingTypesetting is the composition of text by means of types.Typesetting requires the prior process of designing a font and storing it in some manner...
fitch-style proofs (guide).