Verwijderingsregels

Verwijderingsregels zijn inference rules in formele logica die aangeven hoe uit een samengestelde uitspraak een of meer eenvoudige onderdelen of afgeleide resultaten kunnen worden afgeleid. Ze vormen de tegenhanger van de introductieregels, die juist aangeven hoe een complexere uitspraak kan worden opgebouwd. Verwijderingsregels komen voor in systemen van natuurlijk deductie en zijn aanwezig in zowel klassieke als intuïtionistische logica. Ze dienen om gestructureerd bewijs stap voor stap te kunnen afleiden.

De meest voorkomende verwijderingsregels zijn onder andere: conjunctie-eliminatie, uit P ∧ Q kun je P afleiden en ook Q; disjunctie-eliminatie, uit P ∨ Q en bewijzen dat P leidt tot R en Q leidt tot R kun je R afleiden (dit heet een gevalsstudie); implicatie-eliminatie, uit P → Q en P volg Q (modus ponens); universele eliminatie, uit ∀x φ(x) kun je φ(t) afleiden voor een specifieke term t; existentiële eliminatie, uit ∃x φ(x) en een afleidingsstructuur die φ(a) impliqueert ψ met een vers a, kun je ψ afleiden; en ex falso quodlibet, uit een contradictie volg je elke gewenste conclusie. Daarnaast zijn er regels voor quantifiers met voorzorgen zoals de eigenvariabele voor existentiële eliminatie.

Verwijderingsregels worden toegepast om logische connectieven stap voor stap te openen en om bewezenheden uit samengestelde uitspraken te herleiden. Ze zijn fundamenteel in formalisering van bewijsvoering en worden in diverse logische systemen en onderwijsonderwerpen behandeld. Historisch ontstonden ze in het kader van natural deduction, ontwikkeld door Gentzen en Jaśkowski, en zijn ze nog steeds essentieel in logische syllabi en verantwoorde redenering.