Systeem van Fitch

Het systeem van Fitch is een systeem om met natuurlijke deductie stellingen te bewijzen in de formele logica. Het systeem is bedacht door de Amerikaanse logicus Frederic Fitch. In het systeem worden premissen, lemmata en deelbewijzen gebruikt om stellingen te bewijzen.

Elke regel in het (niet uitgebreide) systeem van Fitch dient onderbouwd te worden door een regel uit de natuurlijke deductie, uitgezonderd de hypothesen (die kunnen op elk gewenst moment aangenomen worden). Aan de verticale strepen (soms slechts weergegeven als een verspringing) valt te zien hoelang een hypothese actief is. De horizontale strepen dienen om de hypothesen duidelijk weer te geven (onder elke hypothese staat een horizontale streep).

Het volgende is een eenvoudig voorbeeld uit de propositielogica waar de stelling $A\vdash B\to A$ wordt bewezen:

Er bestaat in deze stelling één premisse (nl. $A$), en deze wordt vanzelfsprekend als eerste hypothese gebruikt. Het enige wat vervolgens moet gebeuren, is onder deze aanname aantonen dat $B\to A$. Daartoe wordt in regel 2 een nieuwe hypothese $B$ aangenomen. Omdat de hypothese uit 1 nog steeds actief is, kan daarop reïteratie worden toegepast, zoals gedaan is in regel 3. Uit de regels 2 en 3 valt vervolgens de implicatie $B\to A$ te introduceren, zoals in regel 4 is gedaan. Daarmee is het bewijs van $A\vdash B\to A$ voltooid.