1.1.Натуральный вывод как тип логического вывода

Моментом появления натурального вывода (НВ) как одного из типов логического вывода традиционно считается выход в 1934 году статьи Г. Генцена «Исследования логических выводов» [Генцен] и статьи С.

В англоязычной литературе системы НВ называются «natural deduction». В отечественной литературе системы НВ иногда называются «естественным выводом».

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

Г. Генцен писал: «Я хотел прежде всего построить такой формализм, который был бы как можно ближе к применяющимся в действительности рассуждениям» [Генцен, с. 10]. Далее он определяет свою задачу более точно: «Мы хотим построить формализм, по возможности точно передающий логические заключения, которые в действительности встречаются в математических доказательствах» [Генцен, с. 17].

Созданию С. Яськовским систем НВ способствовало замечание Я. Лукасевича, что «математики строят свои доказательства, используя не аксиоматический метод, а иные способы рассуждения; главным образом, математики берут «произвольные посылки» и смотрят, что из этих посылок можно вывести» [Pelletier, с. 4].

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

Приведем цитаты, показывающие достоинства НВ перед другими типами логического вывода.

модифицируемый» [Непейвода, с. 297]. «Наиболее удобным способом ее (логики предикатов - В.Ш.) задания является система натурального вывода» [Ивлев, с. 95]. «Для применения в качестве логического аппарата наиболее удобными (системами исчисления предикатов - В.Ш.) являются натуральные системы (системы натурального вывода)» [Войшвилло, с. 85].

Размышляя о преимуществах натурального вывода перед методом резолюции, Д. Пеллетье пишет: «Я предположил, что представление вывода в виде натурального на самом деле обладает значительными преимуществами с познавательной точкой зрения: такое максимально обобщенное представление позволяет студентам глубже проникнуть в структуру логических проблем» [Pelletier, с. 6].

Характеризуя гильбертовские исчисления, авторы [Смирнов и др., с. 21] пишут: «Сами способы построения и выводов в этих системах в значительной степени не соответствуют естественным способам рассуждений». Характеризуя секвенциальные и аналитико-табличные исчисления, эти же авторы пишут: «Сам стиль осуществления этих процедур во многом перестает носить «естественный» характер, т.е. перестает соответствовать обычным способам рассуждений» [Смирнов и др., с. 21].

«Логическая система может быть задана различными способами: аксиоматически, в виде табличного исчисления и т. д. Не все из них одинаково удобны для анализа выводов. Самые широкие возможности в этом плане открывают секвенциальные исчисления и системы натурального вывода» [Быстров, с. 139].

«Во всех этих приемах (секвенциальные исчисления и метод резолюции - В.Ш.) процедура выведения одних положений из других или вообще не представлена, или осуществляется в таком виде, который весьма далек от того, что понималось под выводом в истории логики. И секвенции, и метод резолюции - это скорее алгоритмы проверки общезначимости утверждений, чем вывод. Все они строятся на основе чисто аналитических процедур, в то время как традиционное понятие вывода представляет собой метод синтеза доказуемого утверждения из имеющихся посылок» [Болотов и др., с.

Из перечисленного можно сделать вывод, что НВ обладает определенными преимуществами перед другими типами логического вывода: удобство и простота, конгениальность естественным рассуждениям и др.

Что касается дедуктивной силы НВ, то, представляя НВ, Г. Генцен конструктивно показал, что в классической логике предикатов НВ дедуктивно эквивалентен исчислению секвенций и гильбертовскому исчислению, т.е. вывод некоторой формулы в одном исчислении можно перестроить в вывод этой же формулы в другом исчислении [Генцен].

Также отметим, что в нашем исследовании используются только системы НВ для классической логики. Поэтому рассмотрение НВ для неклассических логик выходит за рамки нашего исследования. Подробнее о системах НВ для неклассических логик см. [Basin et al].

Возможны различные классификации систем НВ [Pelletier], [Смирнов].

Например, Д. Пеллетье выделяет девять основных пунктов («nine choice points»), по которым можно классифицировать системы НВ. В то же время он признает, что «многообразие систем НВ делает весьма затруднительным выделение необходимых и достаточных признаков, которые позволили бы однозначно назвать некоторую логическую систему натуральным выводом» [Pelletier, с. 11].

Поскольку Д. Пеллетье не упоминает системы НВ, предложенные отечественными учеными, мы будем добавлять их в качестве примеров в соответствующие разделы классификации.

Первым основным пунктом является тип представления натурального вывода:

1) в виде дерева (Г. Генцен, Н.А. Шанин, Н.Н. Непейвода);

2) в виде линейного вывода (С. Яськовский, Ф. Фитч, В.А. Бочаров и В.И. Маркин), где подвыводы обозначаются некоторыми графическими объектами (скобками, квадратными скобками, линиями и др.);

3) в виде линейного вывода (С. Яськовский, У. Куайн), где подвыводы обозначаются различными (числовыми) префиксами;

4) в виде линейного вывода с множеством зависимостей (П. Суппес, Е.К. Войшвилло).

Вторым основным пунктом является присутствие (Г. Генцен, У. Куайн, Е.К.

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

одно правило удаления (исключения). Тогда наличие (Г. Генцен, Н.Н. Непейвода, В. А. Бочаров и В.И. Маркин) или отсутствие (Д. Пеллетье, Е.К. Войшвилло, Дж. Поллок, А.М. Анисов) симметричности в системе НВ - это третий основной пункт.

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

Обычным непрямым правилом является ⊃_b:если из посылки С выводима формула В, значит, можно построить вывод формулы С ⊃В.

Например, Г. Генцен предложил следующее непрямое правило v_u:из формулы А V В, подвывода С из посылки А и подвывода С из посылки В выводима формула С. Однако можно предложить прямое правило v_u:из А V В, А ⊃С, В ⊃С выводима формула С, или из А V В, —А выводима формула В.

Д. Пеллетье также отмечает, что прямые и непрямые правила можно вводить для других пропозициональных связок (например, —, ?).

Следующие основные пункты 5-9 касаются работы с переменными в системах НВ. Д. Пеллетье отмечает нетривиальность проблемы работы с переменными в системах НВ в сравнении с другими типами логического вывода.

Количество кванторов, которые используются в системах НВ, - это пятый основной пункт. Подавляющее большинство авторов используют и квантор общности, и квантор существования при формулировке своих систем НВ. Исключение составляет, например, С. Яськовский.

Шестой основной пункт - наличие прямого (У. Куайн, В.А. Бочаров и В.И. Маркин) или непрямого (Г. Генцен, Н.Н. Непейвода) правила удаления квантора существования.

Важнейшей характеристикой систем НВ с прямым правилом удаления 3 является тот факт, что в общем случае заключение такого натурального вывода логически не следует из посылок этого вывода.

В таких системах НВ появляется наряду с понятием вывода понятие завершенного вывода, т. е. вывода, в котором заключение логически следует из всех неисключенных посылок этого вывода. Далее мы подробнее остановимся именно на данном основном пункте.

В системах НВ формулировка правила V_bпредполагает наличие произвольной или новой, ранее не встречающейся в выводе переменной. Седьмой основной пункт - это различные способы, которые гарантируют, что переменная в формулировке правила V_bявляется произвольной.

Например, в системе НВ, предложенной Н.Н. Непейводой, переменная считается произвольной только в том подвыводе, в котором к ней применено V_b,и в этом подвыводе запрещено пользоваться формулами из других подвыводов, в которые данная переменная входит свободно.

В то же время, в системе НВ, предложенной В. А. Бочаровым и В.И. Маркиным, наличие произвольной переменной в формулировке правила V_b задается неявным образом.

С одной стороны, данная переменная не обязательно новая, ранее не встречающаяся в выводе, с другой стороны, согласно понятию вывода в этой системе НВ, ни к одной переменной правило V_bне может быть применено более одного раза, а значит, формулировка V_bпредполагает новую переменную.

Восьмым основным пунктом является разделение всех систем НВ на те, которые допускают вхождение свободных переменных в посылки и заключение выводов (У. Куайн, В.А. Бочаров и В.И. Маркин), и на те, которые не допускают посылок и заключений такого вида, т.е. посылки и заключения в таких системах могут быть только предложениями (В. А. Смирнов).

Дополнительно отметим, что возможна условная (В. А. Бочаров и В. И. Маркин) и универсальная (Д. Пеллетье) интерпретация свободных переменных.

Наконец, девятым основным пунктом является наличие (Дж. Поллок, В. А. Смирнов) или отсутствие (У. Куайн, В. А. Бочаров, В.И. Маркин) особых термов в формулировках кванторных правил.

Например, В. А. Смирнов формулирует кванторные правила V_b,З_и с помощью ε-термов, содержательно трактующихся как неопределенные дескрипции.

Особое внимание мы обратим на деление всех систем НВ в зависимости от того, принимается ли в них прямое или непрямое правило удаления (исключения) квантора существования, и отметим классификацию систем НВ, предложенную В.А. Смирновым.

В данной классификации система НВ, названная NC, с непрямым правилом удаления 3 называется системой НВ первого типа. Второй тип систем НВ (в качестве примера предлагается система NεC) содержит в множестве своих правил прямое правило удаления 3. Ниже мы подробно проанализируем систему NεC.

В оригинальной системе, предложенной Г. Генценом, имеется непрямое правило удаления 3: из формулы 3xA(x) выводима формула С, если формула С выводима из A(a), где a - новая, ранее не встречавшаяся в выводе константа. Таким образом, чтобы получить по такому правилу формулу С из формулы 3xA(x), необходимо построить вспомогательный вывод (он называется подвыводом) формулы С из формулы A(a). Только после построения такого подвывода можно утверждать, что из формулы 3xA(x) выводима формула С.

По-видимому, первым, кто обратил внимание на неудобство применения этого правила и кто предложил альтернативный вариант удаления 3, был У. Куайн [Quine]. В статье «On natural deduction» он сформулировал прямое правило удаления 3: из формулы 3xA(x) выводима формула A(y), где y - переменная, которая в алфавитном порядке не предшествует ни одной переменной, свободно входящей в 3xA(x).

Формулировка данного правила предполагает наличие некоторого упорядочения всех переменных из алфавита языка классической логики предикатов. Фактически речь идет о линейном порядке, заданном на множестве переменных языка. У. Куайн показывает, что именно такой порядок гарантирует непротиворечивость и полноту предложенной им системы НВ.

Однако подход У. Куайна не является единственным. Например, В. А. Смирнов в системе NεC предлагает следующую формулировку прямого правила удаления 3: из формулы 3xA(x) следует формула A(εxA(x)), где εxA(x) - это ε-терм, содержательно трактующийся как неопределенная дескрипция вида «некоторые х, обладающие свойством А» [Смирнов].

Поскольку ε-термы не являются термами классической логики предикатов, то система NεC не эквивалентна системе NC (системе НВ с непрямым правилом удаления 3, предложенной В. А. Смирновым там же): все, что доказуемо в NC, доказуемо в NεC, но обратное неверно.

Однако для NεC можно доказать теорему Гильберта об устранении ε-термов: если в NεC можно из (возможно, пустого) множества посылок Г вывести А и Г, А не содержат ε-термы, то А следует из Г в NC [Смирнов, с. 228], [Мендельсон, с. 111-112].

В. А. Бочаров и В. И. Маркин предлагают вводить абсолютно ограниченные и относительно ограниченные переменных в выводе. Тогда правило удаления 3 запишется следующим образом: из формулы 3xA(x, zι,..., z_n) выводима формула A(y, zι,..., z_n), при этом переменная у становится абсолютно ограниченной в выводе переменной, а все переменные z₁,..., z_n- относительно ограниченными в выводе переменными (z₁,..., z_nсуть все свободные переменные из 3xA(x)).

При этом требуется, чтобы ни одна переменная не была абсолютно ограничена в выводе более одного раза и чтобы ни одна переменная не ограничивала сама себя (непосредственно, т.е. у не входит в z₁,..., z_n, или по транзитивности, т.е. если x ограничивает y и y ограничивает x, то x ограничивает x). Во второй главе нашей работы показывается, что такой подход гарантирует непротиворечивость этой системы НВ.

Мы подробно останавливаемся на системах НВ с прямым правилом удаления 3, поскольку система BMV (Bocharov, Markin, Voishvillo), алгоритм поиска вывода в которой является предметом нашей работы, - система НВ именно такого типа.

С другой стороны, мы останавливаемся подробно на работе с переменными в системах НВ с непрямым правилом удаления 3, т.к. существуют примеры систем НВ, не корректно работающие с переменными.

В англоязычной литературе известна серия публикаций 60-70-х гг. XX века в «The Journal of Symbolic Logic» по поводу системы НВ, предложенной И. Копи (I. Copi). И. Копи публиковал не являющиеся семантически непротиворечивыми системы НВ с прямым правилом удаления 3 [Copi]. Семантическая противоречивость предлагаемых И. Копи систем НВ была установлена Д. Калишем (D. Kalish) [Kalish].

Не является семантически непротиворечивой система НВ, предложенная Е.К. Войшвилло [Войшвилло]. В этой системе доказывается, например, формула 3y(VxA(x, x) ⊃ VzA(y, z)). Данная формула ложна, если в качестве А взять отношение равенства на множестве натуральных чисел.