Fitch-style calculus

Fitch-style calculus

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.

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 " [http://www-csli.stanford.edu/LPL/ Fitch] ".

* An online Java application for proof building is also available [http://logik.phl.univie.ac.at/~chris/gateway/formular-uk-fitch.html] .

References

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

External links

* [http://www.cc.utah.edu/~nahaj/logic/structures/systems/fitch.html Fitch Calculus]
* [http://plato.stanford.edu/entries/fitch-paradox/ Fitch's Paradox of Knowability]


Wikimedia Foundation. 2010.

Игры ⚽ Нужна курсовая?

Look at other dictionaries:

  • Fitch — may refer to: Family name* Fitch (surname), a family name of Anglo Norman originPeople* Alan Fitch (1915 1985), British Labour Party politician * Albert Fitch Bellows (1829 1883), American landscape painter * Alfred Fitch, American Olympian *… …   Wikipedia

  • Frederic Brenton Fitch — (1908 1987) was an American logician, and was the inventor of Fitch style calculus. He was a professor at Yale University. Related Stanford University has produced an application called [http://www csli.stanford.edu/LPL/ Fitch] .An online Java… …   Wikipedia

  • Natural deduction — In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the natural way of reasoning. This contrasts with the axiomatic systems which instead use… …   Wikipedia

  • List of mathematics articles (F) — NOTOC F F₄ F algebra F coalgebra F distribution F divergence Fσ set F space F test F theory F. and M. Riesz theorem F1 Score Faà di Bruno s formula Face (geometry) Face configuration Face diagonal Facet (mathematics) Facetting… …   Wikipedia

  • Well-formed formula — In mathematical logic, a well formed formula (often abbreviated WFF, pronounced wiff or wuff ) is a symbol or string of symbols (a formula) that is generated by the formal grammar of a formal language. To say that a string S is a WFF with respect …   Wikipedia

  • Relevance logic — Relevance logic, also called relevant logic, is a kind of non classical logic requiring the antecedent and consequent of implications be relevantly related. They may be viewed as a family of substructural or modal logics. (It is generally, but… …   Wikipedia

  • United States Academic Decathlon — Infobox generic style0 = style= border: 1px solid #779FD5; float:right; font size:90%; margin: 0 0 1em 1em; padding: 0.25em; width: 275px; color = #356AB3 name = United States Academic Decathlon| img1 = Usadlogo fairuse.png width1 = 220px cap1 =… …   Wikipedia

  • logic, history of — Introduction       the history of the discipline from its origins among the ancient Greeks to the present time. Origins of logic in the West Precursors of ancient logic       There was a medieval tradition according to which the Greek philosopher …   Universalium

  • List of philosophy topics (D-H) — DDaDai Zhen Pierre d Ailly Jean Le Rond d Alembert John Damascene Damascius John of Damascus Peter Damian Danish philosophy Dante Alighieri Arthur Danto Arthur C. Danto Arthur Coleman Danto dao Daodejing Daoism Daoist philosophy Charles Darwin… …   Wikipedia

  • Kimball Union Academy — Coordinates: 43°32′46″N 72°15′31″W / 43.54611°N 72.25861°W / 43.54611; 72.25861 …   Wikipedia

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”