Fitch calculus

The Fitch calculus is a method for proving first-order predicate logic invented by the American logician Frederic Brenton Fitch . The proof is only given on the basis of syntactic rules, without taking into account the meaning of the content of the sentences, i.e. formally . The Fitch calculus is both correct and complete and therefore also suitable as an interactive proof system. In the Fitch calculus, in addition to the premises of the main proof, the introduction of any further assumptions is allowed, but only within sub-proofs. For a proof to be correct, all steps apart from the prerequisites and the initial assumptions of the sub-proofs must be substantiated by first-order logic rules. After an atomic statement has been proven, it can be used to justify a new statement until the proof has been provided.

regulate

The Fitch calculus uses the language of first-order predicate logic , i.e. its logical operators (for example AND, OR, IMPLIED, NOT etc.), applied to atomic statements (represented in the following by lowercase letters p, q, ...). The symbol is the derivative operator (eg read: “p proves q” or “q can be derived from p”). In the Fitch calculus there are the following derivation rules: ${\displaystyle \vdash }$ ${\displaystyle p\vdash q}$

Negations introduction

If p IMPLICATED q and p IMPLICATED NOT q are given, then also NOT p (see Reductio ad absurdum ). Example: ${\displaystyle p\rightarrow q,p\rightarrow \neg q\vdash \neg p}$

Elimination of negation

If p is NOT NOT given (or any other even number of negations), then p is also given (see law of double negation ). Example: ${\displaystyle \neg \neg p\vdash p}$

Conjunction introduction

If p, q, r… are given, then also p AND q AND r… . Example: ${\displaystyle p,q\vdash p\wedge q}$

Elimination of conjunctions

If p AND q AND r… are given, then also p, q, r… . Example: ${\displaystyle p\wedge q\vdash p}$

Disjunction Introduction

If p is given, then also p OR q OR r… . Example: ${\displaystyle p\vdash p\lor q}$

Disjunction Elimination

If p OR q OR r… is given and p IMPLIED z, q IMPLIED z, r IMPLIED z… , then also z . Example: ${\displaystyle p\lor q,p\to z,q\to z\vdash z}$

Equivalence introduction

If p IMPLIED q and q IMPLIED p are given, then p EQUIVALENT q . Example: ${\displaystyle p\to q,q\to p\vdash p\leftrightarrow q}$

Elimination of equivalence

If p EQUIVALENT q is given, then also p IMPLIED q and q IMPLIED p . Example: ${\displaystyle p\leftrightarrow q\vdash p\to q}$

Subjunction introduction

If it has been shown that q can be proved from p by Fitch derivation rules (notation: p q), then p IMPLIED q also holds . By introducing subjunctions one ends a sub-evidence. Example: ${\displaystyle \vdash }$ ${\displaystyle (p\vdash q)\vdash (p\to q)}$

Subjunction Elimination

If p is given and p IMPLIED q , then also q . Example: ${\displaystyle p,p\to q\vdash q}$

If the language contains quantifiers , there are four additional rules:

Allquantor introduction

If a sentence with free variables is given, the fact that these can take on any value of the basic set can be written as universal quantification. Example: ${\displaystyle x=ungerade\vdash \forall x.(x=ungerade)}$

Universal quantifier elimination

If an all-quantified proposition is given, one can infer any individual case from this general case; the variable bound by the universal quantifier can thus be replaced by any element of the basic set. Example: ${\displaystyle \forall x.(x=ungerade)\vdash 3=ungerade}$

Existential quantifier introduction

If there is a specific individual case, this can be formalized as an existence statement. Example: “Rome is the capital of Italy” implies three existential statements: 1. There is something that is the capital of Italy, 2. There is something of which Rome is the capital, 3. There is something that is the capital of something .

Existential quantifier elimination

From an all-quantified implication (for example ∀xr (x) → y, "For all x the following applies: if x has the property r, then y") and the knowledge of the existence of such an x ​​(in the example: ∃xr (x) , "There is an x ​​with the predicate r") one can conclude from the succession (here: y). Example: From the two premises 1. ∀x. (X receives the majority of the votes cast → x is elected) and 2. ∃x. (X received the majority of the votes) it can be concluded: x is elected.

Examples

The following example demonstrates the chain conclusion : . It follows from this . The arrow → means IMPLICATED, IE is short for Implication Elimination, II for Implication Introduction. ${\displaystyle (p\to q),(q\to r)}$ ${\displaystyle (p\to r)}$

1 p → q [Premise] 2 q → r [Premise]    3 p [Assumption begins a sub-evidence]    4 q [IE in lines 3.1]    5 r [IE in lines 4.2; Sub-evidence completed] 6 p → r [II in lines 5.3; Proof completed]

Here is some evidence for the distribution of the implication : ${\displaystyle (p\to (q\to r))\to ((p\to q)\to (p\to r))}$

1 p → (q → r) [Premise]    2 p → q [Assumption 1, starts a sub-evidence]       3 p [Assumption 2, starts a sub-sub-evidence]       4 q [IE in lines 3.2]       5 q → r [IE in lines 3.1]       6 r [IE in lines 4,5; Sub-evidence completed]    7 p → r [II in lines 6.3; Sub-evidence completed] 8 (p → q) → (p → r) [II at lines 7.2; Proof completed]

From the premise ∃y.∀xr (x, y) - “There exists a y such that r (x, y) holds for all x” it should be shown that ∀x.∃yr (x, y) then also holds - "For every x there is a y such that r (x, y)" is true:

1 ∃y.∀xr (x, y) [Premise]    2 ∀xr (x, y) [Assumption begins a sub-evidence]    3 r (x, y) [UE in line 2]    4 ∃yr (x, y) [EI in line 3] 5 ∀xr (x, y) → ∃yr (x, y) [II in lines 2.4; Sub-evidence completed] 6 ∀y. (∀xr (x, y) → ∃yr (x, y)) [UI in line 5] 7 ∃yr (x, y) [EE in lines 1,6] 8 ∀x.∃yr (x, y) [UI in line 7]

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

Applications

In addition to philosophical purposes, the Fitch calculus can also be used in computer science. It is particularly important in theoretical computer science .

Web links

• Entry “Fitch Calculus” In: John Halleck's Logic Systems
• Exercises and evidence calculator for the Fitch calculus on the Stanford University website.
• Java application for Fitch evidence by Christian Gottschall (University of Vienna).

literature

• Jon Barwise and John Etchemendy : Language, Proof, and Logic , Volume 1: Propositional and Predicate Logic . Mentis 2005, ISBN 3-89785-440-6 , there. S. 59ff.117ff et passim ( Volume 2: Applications and Metatheorie. Mentis 2006, ISBN 3-89785-441-4 ); German translation of Language proof and logic , Seven Bridges Press and CSLI, 1999.
  • engl. Original as pdf