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

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

Впервые такие исчисления созданы в 1934 году независимо Генценом и Яськовским. Наряду с исчислением секвенций относятся генценовскому типу, поскольку отталкиваются от безаксиоматического подхода (в противоположность Шаблон:Iw, использующим развитые наборы аксиом и минимум правил вывода). Наиболее известные системы натурального вывода — разработанные Генценом $𝐍𝐊$ (для классического варианта исчисления предикатов) и $𝐍𝐉$ (для интуиционистского исчисления предикатов).

Правила вывода в исчислении $𝐍𝐉$:

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

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

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

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

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

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

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

  $\begin{array}{c}AB\\ ⋮⋮\\ \frac{A\vee BCC}{C}\end{array}$ («если верно $A\vee B$, из $A$ выводится $C$ и из $B$ выводится $C$, то можно заключить $C$»);

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

  $\frac{Fa}{\mathrm{\forall }xFx}$;

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

  $\frac{\mathrm{\forall }xFx}{Fa}$;

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

  $\frac{Fa}{\mathrm{\exists }xFx}$;

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

  $\begin{array}{c}Fa\\ ⋮\\ \frac{\mathrm{\exists }xFxC}{C}\end{array}$;

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

  $\begin{array}{c}A\\ ⋮\\ \frac{B}{A\Rightarrow B}\end{array}$;

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

  $\frac{AA\Rightarrow B}{B}$;

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

  $\begin{array}{c}A\\ ⋮\\ \frac{\mathrm{\perp }}{\mathrm{\neg }A}\end{array}$;

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

  $\frac{A\mathrm{\neg }A}{\mathrm{\perp }}$;

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

  $\frac{\mathrm{\perp }}{A}$.

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

Литература

• Шаблон:Статья
• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Книга