Натуральный вывод ( естественный вывод ) — тип логических исчислений , использующий для доказательства утверждений правила вывода , близкие к обычным содержательным методам рассуждений.

Впервые такие исчисления созданы в 1934 году независимо Генценом и Яськовским . Наряду с исчислением секвенций относятся , поскольку отталкиваются от безаксиоматического подхода (в противоположность , использующим развитые наборы аксиом и минимум правил вывода). Наиболее известные системы натурального вывода — разработанные Генценом ${\displaystyle \mathbf {NK} }$ (для классического варианта исчисления предикатов ) и ${\displaystyle \mathbf {NJ} }$ (для интуиционистского исчисления предикатов).

Правила вывода в исчислении ${\displaystyle \mathbf {NJ} }$ :

• введение конъюнкции :

  ${\displaystyle {\cfrac {A\quad B}{A\wedge B}}}$ («если верно ${\displaystyle A}$ и ${\displaystyle B}$ , то можно заключить ${\displaystyle A\wedge B}$ »);

• исключение конъюнкции:

  ${\displaystyle {\cfrac {A\wedge B}{A}}}$ и ${\displaystyle {\cfrac {A\wedge B}{B}}}$ ;

• введение дизъюнкции :

  ${\displaystyle {\cfrac {A}{A\vee B}}}$ и ${\displaystyle {\cfrac {B}{A\vee B}}}$ ;

• исключение дизъюнкции:

  ${\displaystyle {\begin{aligned}A\quad B\\\vdots \;\quad \vdots \;\\{\cfrac {A\vee B\quad C\quad C}{C}}\end{aligned}}}$ («если верно ${\displaystyle A\vee B}$ , из ${\displaystyle A}$ выводится ${\displaystyle C}$ и из ${\displaystyle B}$ выводится ${\displaystyle C}$ , то можно заключить ${\displaystyle C}$ »);

• введение квантора всеобщности :

  ${\displaystyle {\cfrac {Fa}{\forall {x}Fx}}}$ ;

• исключение квантора всеобщности:

  ${\displaystyle {\cfrac {\forall {x}Fx}{Fa}}}$ ;

• введение квантора существования :

  ${\displaystyle {\cfrac {Fa}{\exists {x}Fx}}}$ ;

• исключение квантора существования:

  ${\displaystyle {\begin{aligned}Fa\\\vdots \;\\{\cfrac {\exists {x}Fx\quad C}{C}}\end{aligned}}}$ ;

• введение импликации :

  ${\displaystyle {\cfrac {B}{A\Rightarrow B}}}$ ;

• исключение импликации ( modus ponens ):

  ${\displaystyle {\cfrac {A\quad A\Rightarrow B}{B}}}$ ;

• введение отрицания :

  ${\displaystyle {\begin{aligned}A\\\vdots \;\\{\cfrac {\quad \bot }{\neg A}}\end{aligned}}}$ ;

• исключение отрицания:

  ${\displaystyle {\cfrac {A\quad \neg A}{\bot }}}$ ;

• выведение из ложного высказывания :

  ${\displaystyle {\cfrac {\bot }{A}}}$ .

Классическая система ${\displaystyle \mathbf {NK} }$ получается присоединением к этим правилам вывода аксиомы ${\displaystyle A\vee \neg A}$ или добавлением правила двойного отрицания ${\displaystyle {\cfrac {\neg \neg A}{A}}}$ .

Литература

• Генцен Г. Исследования логических выводов = Untersuchungen über das logische Schließen // Mathematische Zeitschrift, Bd. 39 (1934–1935), S. 405–431 // Идельсон А. В., Минц Г. Е. Математическая теория логического вывода / перевод А. В. Идельсона. — М. : Наука, 1967. — С. 9—76 .
• Гетманова А. Д. Логика. — Книжный дом «Университет», 1998. — 480 с.
• Зиновьев А. А. Логика высказываний и теория вывода. — Питер, 2015. — 937 с.
• . Натуральный вывод. Теоретико-доказательственное исследование / перевод П. Быстрова. — Лори, 1997.