Большая Советская энциклопедия - натуральное исчисление

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