Pravidlo závěru - Rule of inference
| Pravidla transformace |
|---|
| Výrokový počet |
| Pravidla odvození |
| Pravidla výměny |
| Predikátová logika |
A pravidlo závěru, pravidlo odvození nebo pravidlo transformace je logická forma skládající se z funkce, která bere prostor, analyzuje jejich syntax, a vrátí závěr (nebo závěry ). Například se nazývá pravidlo odvození modus ponens vezme dvě premisy, jednu ve tvaru „Pokud p pak q“ a druhou ve tvaru „p“, a vrátí závěr „q“. Pravidlo je platné s ohledem na sémantiku klasická logika (stejně jako sémantika mnoha dalších neklasická logika ), v tom smyslu, že pokud jsou předpoklady pravdivé (pod výkladem), pak je to také závěr.
Pravidlo závěru obvykle zachovává pravdu, sémantickou vlastnost. v mnohocenná logika, zachovává obecné označení. Akce pravidla odvození je však čistě syntaktická a nemusí zachovávat žádnou sémantickou vlastnost: jakákoli funkce od sad vzorců po vzorce se počítá jako pravidlo odvození. Obvykle pouze pravidla, která jsou rekurzivní jsou důležité; tj. pravidla taková, že existuje efektivní postup pro určení, zda je daný vzorec závěrem dané sady vzorců podle pravidla. Příkladem pravidla, které v tomto smyslu není účinné, je infinitura ω-pravidlo.[1]
Populární pravidla odvození v výroková logika zahrnout modus ponens, modus tollens, a kontrapozice. První objednávka predikátová logika používá pravidla závěru k řešení logické kvantifikátory.
Standardní forma pravidel odvození
v formální logika (a mnoho souvisejících oblastí), pravidla odvození jsou obvykle uvedena v následující standardní formě:
Předpoklad # 1
Předpoklad # 2
...
Předpoklad č
Závěr
Tento výraz uvádí, že kdykoli v průběhu nějaké logické derivace byly získány dané premisy, lze daný závěr považovat za samozřejmost. Přesný formální jazyk, který se používá k popisu premisy i závěrů, závisí na skutečném kontextu odvozenin. V jednoduchém případě lze použít logické vzorce, například v:
To je modus ponens pravidlo výroková logika. Pravidla závěru jsou často formulována jako schémata zaměstnává metavariable.[2] Ve výše uvedeném pravidle (schématu) lze metavariable A a B vytvořit instanci pro libovolný prvek vesmíru (nebo někdy podle konvence omezenou podmnožinu, jako je propozice ) k vytvoření nekonečná sada odvozovacích pravidel.
Důkazový systém je tvořen ze sady pravidel, které jsou spojeny dohromady a tvoří důkazy, nazývané také derivace. Jakákoli derivace má pouze jeden konečný závěr, kterým je tvrzení prokázané nebo odvozené. Pokud v derivaci nejsou uspokojeni prostory, je derivace důkazem a hypotetický prohlášení: "-li areál drží, pak závěr platí. “
Příklad: Hilbertovy systémy pro dvě výrokové logiky
V Hilbertův systém, premisou a závěrem odvozovacích pravidel jsou jednoduše vzorce nějakého jazyka, obvykle využívající metavariable. Tato část používá grafickou kompaktnost prezentace a zdůraznění rozdílu mezi axiomy a pravidly odvození následující notace () místo vertikální prezentace pravidel.
Formální jazyk pro klasiku výroková logika lze vyjádřit pomocí pouze negace (¬), implikace (→) a výrokových symbolů. Známá axiomatizace, skládající se ze tří schémat axiomu a jednoho odvozovacího pravidla (modus ponens), je:
(CA1) ⊢ A → (B → A)
(CA2) ⊢ (A → (B → C)) → ((A → B) → (A → C))
(CA3) ⊢ (¬A → ¬B) → (B → A)
(MP) A, A → B ⊢ B
Může se zdát nadbytečné mít v tomto případě dva pojmy odvození, ⊢ a →. V klasické výrokové logice se skutečně shodují; the teorém o dedukci tvrdí, že A ⊢ B právě když if A → B. I v tomto případě však existuje rozdíl, který stojí za zdůraznění: první notace popisuje a dedukce, to je činnost přechodu od vět k větám, zatímco A → B je jednoduše vzorec vyrobený s logické pojivo, implikace v tomto případě. Bez pravidla odvození (jako modus ponens v tomto případě), neexistuje žádný odpočet ani závěr. Tento bod je znázorněn na Lewis Carroll dialog s názvem „Co želva řekla Achillesovi " [3], stejně jako pozdější pokusy o Bertrand Russell a Peter Winch vyřešit paradox zavedený v dialogu.
Pro některé neklasické logiky věta o dedukci neplatí. Například tříhodnotová logika z Łukasiewicz lze axiomatizovat jako:[4]
(CA1) ⊢ A → (B → A)
(LA2) ⊢ (A → B) → ((B → C) → (A → C))
(CA3) ⊢ (¬A → ¬B) → (B → A)
(LA4) ⊢ ((A → ¬A) → A) → A
(MP) A, A → B ⊢ B
Tato posloupnost se liší od klasické logiky změnou axiomu 2 a přidáním axiomu 4. Klasická věta o dedukci pro tuto logiku neplatí, nicméně platí modifikovaná forma, a to A ⊢ B právě když if A → (A → B).[5]
Přípustnost a odvoditelnost
V sadě pravidel může být pravidlo odvození nadbytečné v tom smyslu, že je přípustný nebo odvozitelné. Odvozitelné pravidlo je pravidlo, jehož závěr lze odvodit z jeho prostor pomocí ostatních pravidel. Přípustným pravidlem je pravidlo, jehož závěr platí, kdykoli se jedná o prostory. Všechna odvozitelná pravidla jsou přípustná. Chcete-li ocenit rozdíl, zvažte následující sadu pravidel pro definování přirozená čísla (dále jen rozsudek tvrdí, že je přirozené číslo):
První pravidlo to říká 0 je přirozené číslo a druhá to uvádí s (n) je přirozené číslo, pokud n je. V tomto důkazním systému lze odvodit následující pravidlo, které ukazuje, že i druhý následník přirozeného čísla je přirozeným číslem:
Jeho odvozením je složení dvou použití výše uvedeného pravidla nástupce. Následující pravidlo pro tvrzení existence předchůdce pro jakékoli nenulové číslo je pouze přípustné:
Toto je skutečný fakt přirozených čísel, což dokazuje indukce. (Chcete-li dokázat, že toto pravidlo je přípustné, předpokládejte derivaci premisy a indukujte na ní derivaci .) Nelze jej však odvodit, protože to závisí na struktuře odvození premisy. Z tohoto důvodu je derivovatelnost po přidání do systému důkazů stabilní, zatímco přípustnost nikoli. Chcete-li vidět rozdíl, předpokládejme, že do systému kontroly bylo přidáno následující nesmyslné pravidlo:
V tomto novém systému je pravidlo dvojitého nástupce stále odvozitelné. Pravidlo pro nalezení předchůdce však již není přípustné, protože neexistuje způsob, jak jej odvodit . Křehkost přípustnosti vychází ze způsobu, jakým je prokázána: protože důkaz může vyvolat strukturu odvození areálu, rozšíření systému přidávají k tomuto důkazu nové případy, které již nemusí platit.
Za přípustná pravidla lze považovat věty důkazního systému. Například v a následný počet kde eliminace řezu drží, střih pravidlo je přípustné.
Viz také
- Argumentační schéma
- Okamžitý závěr
- Odvozovací námitka
- Zákon myšlení
- Seznam pravidel odvození
- Logická pravda
- Strukturální pravidlo
Reference
- ^ Boolos, George; Burgess, John; Jeffrey, Richard C. (2007). Vyčíslitelnost a logika. Cambridge: Cambridge University Press. str.364. ISBN 0-521-87752-0.
- ^ John C. Reynolds (2009) [1998]. Teorie programovacích jazyků. Cambridge University Press. str. 12. ISBN 978-0-521-10697-9.
- ^ Kosta Dosen (1996). Msgstr "Logický důsledek: obrat ve stylu". v Maria Luisa Dalla Chiara; Kees Doets; Daniele Mundici; Johan van Benthem (eds.). Logické a vědecké metody: První díl desátého mezinárodního kongresu logiky, metodologie a filozofie vědy, Florencie, srpen 1995. Springer. str. 290. ISBN 978-0-7923-4383-7. předtisk (s různým stránkováním)
- ^ Bergmann, Merrie (2008). Úvod do mnohocenné a fuzzy logiky: sémantika, algebry a derivační systémy. Cambridge University Press. str.100. ISBN 978-0-521-88128-9.
- ^ Bergmann, Merrie (2008). Úvod do mnohocenné a fuzzy logiky: sémantika, algebry a derivační systémy. Cambridge University Press. str.114. ISBN 978-0-521-88128-9.