1.1.Натуральный вывод как тип логического вывода
Моментом появления натурального вывода (НВ) как одного из типов логического вывода традиционно считается выход в 1934 году статьи Г. Генцена «Исследования логических выводов» [Генцен] и статьи С.
Яськовского «Правила введения посылок в формальной логике» [Jaskowski].В англоязычной литературе системы НВ называются «natural deduction». В отечественной литературе системы НВ иногда называются «естественным выводом».
Название таких систем указывает на ту черту, которая отличает НВ от других типов логического вывода: исчислений гильбертовского типа (аксиоматик) и исчислений секвенций. Системы НВ создавались с целью (насколько это возможно) имитировать рассуждения, которые характерны для человеческого мышления, решающего (прежде всего) математическую задачу.
Г. Генцен писал: «Я хотел прежде всего построить такой формализм, который был бы как можно ближе к применяющимся в действительности рассуждениям» [Генцен, с. 10]. Далее он определяет свою задачу более точно: «Мы хотим построить формализм, по возможности точно передающий логические заключения, которые в действительности встречаются в математических доказательствах» [Генцен, с. 17].
Созданию С. Яськовским систем НВ способствовало замечание Я. Лукасевича, что «математики строят свои доказательства, используя не аксиоматический метод, а иные способы рассуждения; главным образом, математики берут «произвольные посылки» и смотрят, что из этих посылок можно вывести» [Pelletier, с. 4].
Данная черта отличает НВ как от аксиоматического метода (вывод в гильбертовских исчислениях страдает громоздкостью и определенной искусственностью, не характерной для естественных рассуждений), так и от исчисления секвенций и непосредственно идущих от метода секвенций методов семантических и аналитических таблиц (для последних двух методов характерен поиск опровержения, а не доказательства).
Приведем цитаты, показывающие достоинства НВ перед другими типами логического вывода.
«Естественный вывод гораздо более тонкий инструмент, чем семантические таблицы, обладающий большой аналитической силой и легкомодифицируемый» [Непейвода, с. 297]. «Наиболее удобным способом ее (логики предикатов - В.Ш.) задания является система натурального вывода» [Ивлев, с. 95]. «Для применения в качестве логического аппарата наиболее удобными (системами исчисления предикатов - В.Ш.) являются натуральные системы (системы натурального вывода)» [Войшвилло, с. 85].
Размышляя о преимуществах натурального вывода перед методом резолюции, Д. Пеллетье пишет: «Я предположил, что представление вывода в виде натурального на самом деле обладает значительными преимуществами с познавательной точкой зрения: такое максимально обобщенное представление позволяет студентам глубже проникнуть в структуру логических проблем» [Pelletier, с. 6].
Характеризуя гильбертовские исчисления, авторы [Смирнов и др., с. 21] пишут: «Сами способы построения и выводов в этих системах в значительной степени не соответствуют естественным способам рассуждений». Характеризуя секвенциальные и аналитико-табличные исчисления, эти же авторы пишут: «Сам стиль осуществления этих процедур во многом перестает носить «естественный» характер, т.е. перестает соответствовать обычным способам рассуждений» [Смирнов и др., с. 21].
«Логическая система может быть задана различными способами: аксиоматически, в виде табличного исчисления и т. д. Не все из них одинаково удобны для анализа выводов. Самые широкие возможности в этом плане открывают секвенциальные исчисления и системы натурального вывода» [Быстров, с. 139].
«Во всех этих приемах (секвенциальные исчисления и метод резолюции - В.Ш.) процедура выведения одних положений из других или вообще не представлена, или осуществляется в таком виде, который весьма далек от того, что понималось под выводом в истории логики. И секвенции, и метод резолюции - это скорее алгоритмы проверки общезначимости утверждений, чем вывод. Все они строятся на основе чисто аналитических процедур, в то время как традиционное понятие вывода представляет собой метод синтеза доказуемого утверждения из имеющихся посылок» [Болотов и др., с.
172].Из перечисленного можно сделать вывод, что НВ обладает определенными преимуществами перед другими типами логического вывода: удобство и простота, конгениальность естественным рассуждениям и др.
Что касается дедуктивной силы НВ, то, представляя НВ, Г. Генцен конструктивно показал, что в классической логике предикатов НВ дедуктивно эквивалентен исчислению секвенций и гильбертовскому исчислению, т.е. вывод некоторой формулы в одном исчислении можно перестроить в вывод этой же формулы в другом исчислении [Генцен].
Также отметим, что в нашем исследовании используются только системы НВ для классической логики. Поэтому рассмотрение НВ для неклассических логик выходит за рамки нашего исследования. Подробнее о системах НВ для неклассических логик см. [Basin et al].
Возможны различные классификации систем НВ [Pelletier], [Смирнов].
Например, Д. Пеллетье выделяет девять основных пунктов («nine choice points»), по которым можно классифицировать системы НВ. В то же время он признает, что «многообразие систем НВ делает весьма затруднительным выделение необходимых и достаточных признаков, которые позволили бы однозначно назвать некоторую логическую систему натуральным выводом» [Pelletier, с. 11].
Поскольку Д. Пеллетье не упоминает системы НВ, предложенные отечественными учеными, мы будем добавлять их в качестве примеров в соответствующие разделы классификации.
Первым основным пунктом является тип представления натурального вывода:
1) в виде дерева (Г. Генцен, Н.А. Шанин, Н.Н. Непейвода);
2) в виде линейного вывода (С. Яськовский, Ф. Фитч, В.А. Бочаров и В.И. Маркин), где подвыводы обозначаются некоторыми графическими объектами (скобками, квадратными скобками, линиями и др.);
3) в виде линейного вывода (С. Яськовский, У. Куайн), где подвыводы обозначаются различными (числовыми) префиксами;
4) в виде линейного вывода с множеством зависимостей (П. Суппес, Е.К. Войшвилло).
Вторым основным пунктом является присутствие (Г. Генцен, У. Куайн, Е.К.
Войшвилло) или отсутствие (С. Яськовский) в системе НВ некоторых аксиом наряду с правилами вывода.Назовем систему НВ симметричной, если в ней для любого логического символа (связки или квантора) содержатся хотя бы одно правило введения и хотя бы
одно правило удаления (исключения). Тогда наличие (Г. Генцен, Н.Н. Непейвода, В. А. Бочаров и В.И. Маркин) или отсутствие (Д. Пеллетье, Е.К. Войшвилло, Дж. Поллок, А.М. Анисов) симметричности в системе НВ - это третий основной пункт.
Четвертый основной пункт (для пропозиционального исчисления) - количество непрямых правил вывода в системе НВ, где непрямое правило - это правило, требующее построения подвывода.
Обычным непрямым правилом является ⊃b:если из посылки С выводима формула В, значит, можно построить вывод формулы С ⊃В.
Например, Г. Генцен предложил следующее непрямое правило vu:из формулы А V В, подвывода С из посылки А и подвывода С из посылки В выводима формула С. Однако можно предложить прямое правило vu:из А V В, А ⊃С, В ⊃С выводима формула С, или из А V В, —А выводима формула В.
Д. Пеллетье также отмечает, что прямые и непрямые правила можно вводить для других пропозициональных связок (например, —, ?).
Следующие основные пункты 5-9 касаются работы с переменными в системах НВ. Д. Пеллетье отмечает нетривиальность проблемы работы с переменными в системах НВ в сравнении с другими типами логического вывода.
Количество кванторов, которые используются в системах НВ, - это пятый основной пункт. Подавляющее большинство авторов используют и квантор общности, и квантор существования при формулировке своих систем НВ. Исключение составляет, например, С. Яськовский.
Шестой основной пункт - наличие прямого (У. Куайн, В.А. Бочаров и В.И. Маркин) или непрямого (Г. Генцен, Н.Н. Непейвода) правила удаления квантора существования.
Важнейшей характеристикой систем НВ с прямым правилом удаления 3 является тот факт, что в общем случае заключение такого натурального вывода логически не следует из посылок этого вывода.
В таких системах НВ появляется наряду с понятием вывода понятие завершенного вывода, т. е. вывода, в котором заключение логически следует из всех неисключенных посылок этого вывода. Далее мы подробнее остановимся именно на данном основном пункте.
В системах НВ формулировка правила Vbпредполагает наличие произвольной или новой, ранее не встречающейся в выводе переменной. Седьмой основной пункт - это различные способы, которые гарантируют, что переменная в формулировке правила Vbявляется произвольной.
Например, в системе НВ, предложенной Н.Н. Непейводой, переменная считается произвольной только в том подвыводе, в котором к ней применено Vb,и в этом подвыводе запрещено пользоваться формулами из других подвыводов, в которые данная переменная входит свободно.
В то же время, в системе НВ, предложенной В. А. Бочаровым и В.И. Маркиным, наличие произвольной переменной в формулировке правила Vb задается неявным образом.
С одной стороны, данная переменная не обязательно новая, ранее не встречающаяся в выводе, с другой стороны, согласно понятию вывода в этой системе НВ, ни к одной переменной правило Vbне может быть применено более одного раза, а значит, формулировка Vbпредполагает новую переменную.
Восьмым основным пунктом является разделение всех систем НВ на те, которые допускают вхождение свободных переменных в посылки и заключение выводов (У. Куайн, В.А. Бочаров и В.И. Маркин), и на те, которые не допускают посылок и заключений такого вида, т.е. посылки и заключения в таких системах могут быть только предложениями (В. А. Смирнов).
Дополнительно отметим, что возможна условная (В. А. Бочаров и В. И. Маркин) и универсальная (Д. Пеллетье) интерпретация свободных переменных.
Наконец, девятым основным пунктом является наличие (Дж. Поллок, В. А. Смирнов) или отсутствие (У. Куайн, В. А. Бочаров, В.И. Маркин) особых термов в формулировках кванторных правил.
Например, В. А. Смирнов формулирует кванторные правила Vb,Зи с помощью ε-термов, содержательно трактующихся как неопределенные дескрипции.
Особое внимание мы обратим на деление всех систем НВ в зависимости от того, принимается ли в них прямое или непрямое правило удаления (исключения) квантора существования, и отметим классификацию систем НВ, предложенную В.А. Смирновым.
В данной классификации система НВ, названная 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ι,..., zn) выводима формула A(y, zι,..., zn), при этом переменная у становится абсолютно ограниченной в выводе переменной, а все переменные z1,..., zn- относительно ограниченными в выводе переменными (z1,..., znсуть все свободные переменные из 3xA(x)).
При этом требуется, чтобы ни одна переменная не была абсолютно ограничена в выводе более одного раза и чтобы ни одна переменная не ограничивала сама себя (непосредственно, т.е. у не входит в z1,..., zn, или по транзитивности, т.е. если 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)). Данная формула ложна, если в качестве А взять отношение равенства на множестве натуральных чисел.
Еще по теме 1.1.Натуральный вывод как тип логического вывода:
- ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004, 2004
- Михайлов Кирилл Авенирович. Логические идеи И. Канта. Диссертация на соискание ученой степени кандидата философских наук. Москва, 2003год, 2003
- 2.3. Порфирий как комментатор Платона.
- 2.4. Раннепифагорейский космос как целостность
- Акусмы как мыслительный феномен
- Самопознание как начало философского познания.
- Открытие несоизмеримости как мыслительный феномен
- Ранние пифагорейцы как часть досократической философии
- Бугай Дмитрий Владимирович. Прокл Диадох как комментатор Платона. Диссертация на соискание учёной степени кандидата философских наук. Москва - 2001, 2001
- Источник генезиса логики
- Заключение
- Терминологические и методологические проблемы
- Другие примеры прото-упорядочивания
- Проблема интерпретации учения ранних пифагорейцев
- Введение
- Специфика доксографии и краткий обзор академического изучения раннего пифагореизма
- Библиография