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

---

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

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

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

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

---