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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  ${\begin{aligned}A\\\vdots \;\\{\cfrac {\quad B}{A\Rightarrow B}}\end{aligned}}$;

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

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

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

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

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

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

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

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

Классическая система $\mathbf {NK}$ получается присоединением к этим правилам вывода аксиомы $A\vee \neg A$ или добавлением правила двойного отрицания ${\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.