Натуральный вывод (естественный вывод) — тип логических исчислений, использующий для доказательства утверждений правила вывода, близкие к обычным содержательным методам рассуждений.
Впервые такие исчисления созданы в 1934 году независимо Генценом и Яськовским. Наряду с исчислением секвенций относятся генценовскому типу, поскольку отталкиваются от безаксиоматического подхода (в противоположность , использующим развитые наборы аксиом и минимум правил вывода). Наиболее известные системы натурального вывода — разработанные Генценом (для классического варианта исчисления предикатов) и (для интуиционистского исчисления предикатов).
Правила вывода в исчислении : введение конъюнкции: («если верно и , то можно заключить »); исключение конъюнкции: и ; введение дизъюнкции: и ; исключение дизъюнкции: («если верно , из выводится и из выводится , то можно заключить »); введение квантора всеобщности: ; исключение квантора всеобщности: ; введение квантора существования: ; исключение квантора существования: ; введение импликации: ; исключение импликации (modus ponens): ; введение отрицания: ; исключение отрицания: ; выведение из ложного высказывания: . Классическая система получается присоединением к этим правилам вывода аксиомы или добавлением правила двойного отрицания .
Литература
Категория:Теория доказательств