V logice je transformační pravidlo nebo pravidlo odvození syntaktické pravidlo nebo funkce, která bere premisy a vrací závěr (nebo v logice s vícenásobným závěrem závěry). Například pravidlo odvození modus ponens bere dvě premisy, jednu ve formě „If p then q“ a druhou ve formě „p“ a vrací závěr „q“. Pravidlo je platné s ohledem na sémantiku klasické logiky (stejně jako sémantika mnoha dalších neklasických logik), v tom smyslu, že pokud jsou premisy pravdivé (podle interpretace), pak je pravdivý i závěr.
Pravidlo odvození obvykle zachovává sémantickou vlastnost pravdy (nebo obecněji označení – viz mnohonásobně oceňovaná logika). Ale pokud to vezmeme čistě syntakticky, pravidlo odvození nemusí zachovávat žádnou sémantickou vlastnost: jako pravidlo odvození se počítá jakákoli funkce od množin vzorců po vzorce. Obvykle jsou důležitá pouze pravidla, která jsou rekurzivní; tj. pravidla taková, že existuje účinný postup pro určení, zda je daný vzorec závěrem dané množiny vzorců podle pravidla. Příkladem pravidla, které není v tomto smyslu účinné, je nekonečné pravidlo ω.
Populární pravidla odvozování zahrnují modus ponens, modus tollens z výrokové logiky a kontraindikace. Predikátová logika prvního řádu používá pravidla odvozování pro práci s logickými kvantifikátory. Viz Seznam pravidel odvozování pro příklady.
Ve formální logice (a mnoha souvisejících oblastech) jsou pravidla odvození obvykle uvedena v následující standardní formě:
Premise#1
Premise#2
…
Premise#n
Závěr
Tento výraz říká, že kdykoli byly v průběhu nějakého logického odvození dané předpoklady získány, může být daný závěr také považován za samozřejmý. Přesný formální jazyk, který se používá k popisu předpokladů i závěrů, závisí na skutečném kontextu odvození. V jednoduchém případě lze použít logické vzorce, například:
To je jen modus ponens pravidlo výrokové logiky. Pravidla odvození jsou obvykle formulována jako schémata pravidel pomocí univerzálních proměnných. Ve výše uvedeném pravidle (schématu) mohou být A a B instancovány k jakémukoli prvku vesmíru (nebo někdy konvencí k nějaké omezené podmnožině, jako jsou výroky) a tvořit tak nekonečný soubor pravidel odvození.
Důkazní systém je tvořen souborem pravidel spojených řetězem za účelem vytvoření dokladů, nebo odvozenin. Jakákoli odvozenina má pouze jeden konečný závěr, kterým je prokázané nebo odvozené tvrzení. Pokud jsou v odvozenině ponechány neuspokojené předpoklady, pak je odvození důkazem hypotetického tvrzení: „pokud předpoklady drží, pak platí závěr.“
Přípustnost a odvozitelnost
V souboru pravidel by odvozující pravidlo mohlo být nadbytečné v tom smyslu, že je přípustné nebo odvozitelné. Odvozené pravidlo je takové, jehož závěr lze odvodit z jeho premis pomocí ostatních pravidel. Přípustné pravidlo je takové, jehož závěr platí vždy, když dané premisy platí. Všechna odvozitelná pravidla jsou přípustná. Pro ocenění rozdílu zvažte následující soubor pravidel pro definování přirozených čísel (rozsudek potvrzuje skutečnost, že se jedná o přirozené číslo):
První pravidlo říká, že 0 je přirozené číslo, a druhé říká, že s(n) je přirozené číslo, pokud n je. V tomto důkazním systému je odvozitelné následující pravidlo ukazující, že druhý nástupce přirozeného čísla je také přirozené číslo:
Jeho odvození je pouze složením dvou použití výše uvedeného nástupnického pravidla. Následující pravidlo pro tvrzení existence předchůdce pro libovolné nenulové číslo je pouze přípustné:
To je pravdivý fakt přirozených čísel, jak může být prokázáno indukcí. (Chcete-li dokázat, že toto pravidlo je přípustný, předpokládejme odvození premisy a indukovat na to, aby se derivace .) Nicméně, to není derivovatelný, protože to závisí na struktuře odvození premisy. Vzhledem k tomu, derivovatelnost je stabilní podle dodatky k důkazu systému, zatímco přípustnost není. Chcete-li vidět rozdíl, předpokládejme, že následující nesmysl pravidlo byly přidány do důkazu systému:
V tomto novém systému je pravidlo dvojího nástupce stále odvozitelné. Nicméně pravidlo pro nalezení předchůdce již není přípustné, protože neexistuje způsob, jak odvodit . Křehkost přípustnosti vychází ze způsobu, jakým je prokázána: jelikož důkaz může navodit na strukturu odvození předpokladů, rozšíření systému přidávají k tomuto důkazu nové případy, které již nemusí platit.
Přípustná pravidla lze považovat za věty důkazního systému. Například v sekvenčním kalkulu, kde platí eliminace řezu, je přípustné pravidlo řezu.
Inferenční pravidla mohou být také uvedena v této formě: (1) některé (možná nulové) prostory, (2) symbol turniketu , což znamená „vyvozuje“, „dokazuje“ nebo „uzavírá“, (3) závěr. Ten obvykle ztělesňuje relační (na rozdíl od funkčního) pohledu na pravidlo vyvozování, kde turniket představuje dedukovatelnost vztahu držení mezi prostory a závěrem.
Pravidla odvození je třeba odlišit od axiomů teorie. Z hlediska sémantiky jsou axiomy platná tvrzení. Axiomy jsou obvykle považovány za východiska pro aplikaci pravidel odvození a generování souboru závěrů. Nebo, méně odborně řečeno:
Pravidla jsou příkazy O systému, axiomy jsou příkazy V systému. Například:
Pravidla inference hrají zásadní roli ve specifikaci logických kalkulů, jak jsou zvažovány v teorii důkazu, jako je sekvenční kalkul a přírodní dedukce.