<<
>>

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)). Данная формула ложна, если в качестве А взять отношение равенства на множестве натуральных чисел.

<< | >>
Источник: ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004. 2004

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

  1. ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004, 2004
  2. Михайлов Кирилл Авенирович. Логические идеи И. Канта. Диссертация на соискание ученой степени кандидата философских наук. Москва, 2003год, 2003
  3. 2.3. Порфирий как комментатор Платона.
  4. 2.4. Раннепифагорейский космос как целостность
  5. Акусмы как мыслительный феномен
  6. Самопознание как начало философского познания.
  7. Открытие несоизмеримости как мыслительный феномен
  8. Ранние пифагорейцы как часть досократической философии
  9. Бугай Дмитрий Владимирович. Прокл Диадох как комментатор Платона. Диссертация на соискание учёной степени кандидата философских наук. Москва - 2001, 2001
  10. Источник генезиса логики
  11. Заключение
  12. Терминологические и методологические проблемы
  13. Другие примеры прото-упорядочивания
  14. Проблема интерпретации учения ранних пифагорейцев
  15. Введение
  16. Специфика доксографии и краткий обзор академического изучения раннего пифагореизма
  17. Библиография