Натуральный вывод

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

Впервые такие исчисления созданы в 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 {\begin{aligned}A\\\vdots \;\\{\cfrac {\quad B}{A\Rightarrow B}}\end{aligned}}}$;

• исключение импликации (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.