Přirozený závěr

Přirozená inference ( natural inference ) je typ logického kalkulu , který používá inferenční pravidla k prokázání tvrzení , která jsou blízká obvyklým smysluplným metodám uvažování.

Poprvé takové výpočty vytvořili v roce 1934 nezávisle Gentsen a Yaskovsky . Spolu se sekvenčním kalkulem patří do Gentzenova typu , protože jsou založeny na neaxiomatickém přístupu (na rozdíl od Hilbertova kalkulu , který používá rozvinuté sady axiomů a minimum odvozovacích pravidel). Nejznámější přirozené inferenční systémy jsou ty, které vyvinul Gentzen (pro klasickou verzi predikátového počtu ) a (pro intuicionistický predikátový počet). $\mathbf {NK}$ $\mathbf {NJ}$

Odvozovací pravidla v počtu : $\mathbf {NJ}$

úvod spojení : ${\cfrac {A\quad B}{A\wedge B}}$ („pokud je pravda a , pak můžeme dojít k závěru “); $A$ $B$ $A\klín B$
výjimka spojení: ${\cfrac {A\wedge B}{A}}$ a ; ${\cfrac {A\wedge B}{B}}$
úvod disjunkce : ${\cfrac {A}{A\vee B}}$ a ; ${\cfrac {B}{A\vee B}}$
výjimka disjunkce: ${\begin{aligned}A\quad B\\\vdots \;\quad \vdots \;\\{\cfrac {A\vee B\quad C\quad C}{C))\end{aligned }}$ („pokud je to pravda , z je vyvozeno a z je vyvozeno , pak můžeme dojít k závěru “); $A\vee B$ $A$ $C$ $B$ $C$ $C$
zavedení univerzálního kvantifikátoru : ${\cfrac {Fa}{\forall {x}Fx))$ ;
výjimka univerzálního kvantifikátoru: ${\cfrac {\forall {x}Fx}{Fa))$ ;
zavedení existenčního kvantifikátoru : ${\cfrac {Fa}{\exists {x}Fx))$ ;
vyloučení existenčního kvantifikátoru: ${\begin{aligned}Fa\\\vdots \;\\{\cfrac {\exists {x}Fx\quad C}{C))\end{aligned))$ ;
implikační úvod : ${\cfrac {B}{A\Rightarrow B}}$ ;
vyloučení implikace ( modus ponens ): ${\cfrac {A\quad A\Rightarrow B}{B}}$ ;
úvod negace : ${\begin{aligned}A\\\vdots \;\\{\cfrac {\quad \bot }{\neg A))\end{aligned))$ ;
výjimka negace: ${\cfrac {A\quad \neg A}{\bot }}$ ;
odvození z nepravdivého tvrzení : ${\cfrac {\bot }{A}}$ .

Klasický systém se získá přidáním axiomu k těmto pravidlům odvození nebo přidáním pravidla dvojité negace . $\mathbf {NK}$ $A\vee\neg A$ ${\cfrac {\neg \neg A}{A))$

Literatura

Gentzen G. Inference Studies = Untersuchungen über das logische Schließen // Mathematische Zeitschrift, Bd. 39 (1934–1935), S. 405–431 // Idelson A. V., Mints G. E. Mathematical theory of inference / přeložil A. V. Idelson. - M .: Nauka, 1967. - S. 9-76 .
Getmanová A. D. Logic. - Dům knihy "Univerzita", 1998. - 480 s.
Zinoviev A. A. Výroková logika a teorie odvození. - Petr, 2015. - 937 s.
Pravits D. přirozený závěr. Výzkum založený na důkazech / překlad P. Bystrova. - Laurie, 1997.

Logika

Filosofie • Sémantika • Syntaxe • Historie

Logické skupiny

klasická logika	Aristotelská logika výroková logika Logika prvního řádu Logika druhého řádu logika vyššího řádu
matematická logika	teorie množin Teorie modelu Teorie vyčíslitelnosti Důkazová teorie a konstruktivní matematika Lineární logika formální systém přirozený závěr Sekvenční počet Algebra logiky Relevantní logika Deontická logika intuicionistická logika Lambekův počet
Neklasická logika	intuicionismus fuzzy logika Substrukturální logika logika Popisná logika Vícehodnotová logika Logická syntéza Závazná logika Temporální logika Modální logika ( Hybrid logic ) epistemická logika
Filosofická logika	Kritické myšlení neformální logika deduktivní uvažování

Komponenty

Seznam booleovských symbolů