Fitch-style calculus

The Fitch - calculus is an invented by the American logician Frederic Brenton Fitch method for proofs in first-order logic. The proof is simply out of syntactic rules, without regard to the content, meanings of sentences occurring, so formal. The Fitch - calculus is therefore also suitable as interactive proof system both correct and complete. In Fitch - calculus is in addition to the assumptions of the main evidence, the introduction of any further assumptions allowed, but only within sub- proofs. For a proof is correct, all the steps except for the conditions and the initial assumptions of evidence must be supported by logic rules first order. After an atomic statement has been proved, it must be used to justify a new statement until evidence has been offered.

Regulate

The Fitch - calculus uses the language of first order predicate logic, so the logical operators (such as AND, OR, IMPLIES, NOT, etc. ) applied to atomic propositions (hereinafter represented by lower-case letters p, q, ...). The symbol is the derivative operator (for example, read " shows p q" or " Q can be derived from p "). In Fitch - calculus we have the following derivation rules:

Contains the language quantifiers, four more rules are added:

Examples

The following example demonstrates the chain end. It follows. The arrow → means IMPLIED, IE is short for Implication elimination ( Subjunktionsbeseitigung ), II for Implication Introduction ( Subjunktionseinführung ).

Here is a proof of the distribution of the implication:

From the premise ∃ Y ∀ x r (x, y) -. " There is a Y, so that r (x, y) is valid for all x " is to be shown that then ∀ x ∃ yr (x, y) is true. - " For every x there exists a y such that r ( x, y) " is true:

Abbreviations: AI: Universal elimination = universal quantifier elimination, UI: Universal Introduction = universal quantifier introduction, EI: Existential Introduction = existential - introduction, EE: Existential Eliminitation = existential quantifier elimination

Applications

The Fitch - calculus can be used in addition to philosophical purposes in computer science. It has meaning primarily in theoretical computer science.