Натуральное исчисление

исчисление естественного вывода, натуральная дедукция, общее название логических исчислений, введённых и изученных в 1934 немецким логиком Г. Генценом (и независимо польским логиком С. Яськовским) с целью формализации процесса логического вывода, как можно более точно воспроизводящей структуру обычных содержательных рассуждений, а также для решения ряда важных задач метаматематики (См. Метаматематика) (в том числе для доказательства непротиворечивости (См. Непротиворечивость) арифметики натуральных чисел). Основным объектом Н. И. Можно считать отношение (формальной) выводимости, обозначаемое символом ⊢, обладающее, по определению, свойством А (разрешение усилить посылки), (разрешение опускать одну из совпадающих посылок), (разрешение переставлять посылки).

В различных формулировках Н. И. Вид и число структурных правил различны. Например, понимая под Д и Г не последовательности, а просто конечные множества (неупорядоченные) формул, можно обойтись без правил перестановки посылок. Обычное соглашение, что каждый элемент входит в него лишь один раз, делает ненужным правило сокращения повторяющихся посылок, и т.п. Кроме того, в Н. И. Входят логические правила вывода, регламентирующие процедуру введения и удаления (устранения, исключения) символов логических операций и описывающие (как и аксиомы «обычных» логических исчислений. См., например, Логика высказываний) свойства этих операций. Вот правила классического Н. И. Высказываний. Введение (так называемая «теорема о дедукции», см.

Дедукция) (reductio ad absurdum, или приведение к нелепости, см. Доказательство от противного) Удаление (так называемое доказательство разбором случаев) (modus ponens, или схема заключения) (так называемый закон снятия двойного отрицания). (В скобках указана Интерпретация некоторых правил в терминах традиционной логики. Интерпретация остальных правил — та же, что у соответствующих аксиом обычного исчисления высказываний, перефразировками которых они являются.) Добавление к этому списку соответствующих правил введения и удаления для Кванторов приводит к Н. И. Предикатов. Замена правила .