Введение

Вид доказательного исчисления
В логике и теории доказательств, естественная дедукция — это вид доказательного исчисления, в котором логические рассуждения выражаются правилами вывода, тесно связанными с «естественным» способом рассуждения. Это противопоставляется системам в стиле Гильберта, которые вместо этого используют аксиомы в максимально возможной степени для выражения логических законов дедуктивного вывода.

История

Естественная дедукция возникла на фоне неудовлетворенности аксиоматизациями дедуктивного рассуждения, распространенными в системах Гильберта, Фреге и Рассела (см., например, систему Гильберта). Эти аксиоматизации наиболее известны по использованию Расселом и Уайтхедом в их математическом трактате Principia Mathematica. Подстегнутый серией семинаров в Польше в 1926 году, проведенных Лукасевичем, которые выступали за более естественное понимание логики, Яшковский предпринял первые попытки определения более естественной дедукции, сначала в 1929 году, используя диаграмматическую нотацию, а затем уточнил свое предложение в серии статей в 1934 и 1935 годах. Его предложения привели к различным обозначениям, таким как исчисление в стиле Фитча (или диаграммы Фитча) или метод Саппеса, для которого Леммон предложил вариант, названный системой L.

Естественная дедукция в ее современном виде была независимо предложена немецким математиком Герхардом Гентценом в 1933 году в диссертации, представленной на факультет математических наук Геттингенского университета. Термин «естественная дедукция» (или, скорее, его немецкий эквивалент natürliches Schließen) был введен в этой работе:

Гентцен был мотивирован желанием установить непротиворечивость теории чисел. Ему не удалось доказать основной результат, необходимый для доказательства непротиворечивости, – теорему об отбрасывании срезов (устранении обрыва) – Hauptsatz – непосредственно для естественной дедукции. По этой причине он ввел свою альтернативную систему – исчисление секвенций, для которой он доказал Hauptsatz как для классической, так и для интуиционистской логики. В серии семинаров в 1961 и 1962 годах Правиц дал всесторонний обзор исчислений естественной дедукции и перенес значительную часть работы Гентцена с исчислением секвенций в рамки естественной дедукции. Его монография 1965 года «Естественная дедукция: теоретическое исследование доказательств» стала фундаментальным трудом по естественной дедукции и включала приложения для модальной и логики второго порядка. В естественной дедукции предложение выводится из набора посылок путем многократного применения правил вывода. Система, представленная в этой статье, является незначительной вариацией формулировки Гентцена или Правица, но с более строгим следованием описанию логических суждений и связок, предложенному Мартином Лёфом.

История стилей нотации

Природный вывод имеет большое разнообразие стилей обозначений, указывающих на предшествующие зависимости по номерам строк в квадратных скобках, предвосхищая обозначение номерами строк, предложенное Суппесом в 1957 году. 1950: В учебнике был продемонстрирован метод использования одной или нескольких звездочек слева от каждой строки доказательства для указания зависимостей. Это эквивалентно вертикальным чертам Клине. (Не совсем ясно, появилась ли астерисковая нотация Куйна в оригинальном издании 1950 года или была добавлена в более позднем издании.) 1957: В учебнике было представлено введение в практическое доказательство теорем логики, где зависимости (т.е. предшествующие утверждения) указывались номерами строк слева от каждой строки. 1963: использует наборы номеров строк для указания предшествующих зависимостей строк последовательных логических аргументов, основанных на правилах естественного вывода. 1965: Весь учебник является введением в логические доказательства, использующим метод, основанный на методе Суппеса, который теперь известен как нотация Суппеса — Леммона. 1967: В учебнике кратко были продемонстрированы два вида практических логических доказательств: одна система использует явные цитаты предшествующих утверждений слева от каждой строки, а другая система использует вертикальные черты слева для указания зависимостей.