Генценовское исчисление естественных выводов как средство экспликации форм интуитивных умозаключений в трудах античных математиков тема диссертации и автореферата по ВАК РФ 09.00.07, кандидат философских наук Бирюков, Александр Викторович

• Бирюков, Александр Викторович
• кандидат философских наук
• 1999

Оглавление диссертации кандидат философских наук Бирюков, Александр Викторович

Оглавление

Введение

Глава 1. О выборе подходящей современной дедуктивной системы для экспликации евклидовых доказательств.

1.1. Взгляды Лейбница на природу математических доказательств

1.2. Необходимость расширения традиционной логики для возможности представления структуры математического доказательства

1.3. Неформализованный характер логической составляющей математического доказательства до начала XX века

1.4. Осознание необходимости уточнения способов заключения, фигурирующих в математическом рассуждении

1.5. Математическая модель естественного языка как одна из фундаментальных предпосылок анализа логических переходов

в математическом доказательстве

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

в античной математике

1.7. Генценовский вариант натурального вывода

Глава 2. Описание генценовского исчисления естественных выводов

(секвенциальный вариант)

2.0. Секвенциальный вариант генценовского исчисления естественных выводов

2.1. Замечания об используемых в настоящей работе логической символике и логико-предметном языке

2.2. Структура естественного вывода

2.3. Возможные начала процесса вывода в ИЕВ

2.4. Основные правила естественного вывода

2.5. Пропозициональная часть ИЕВ

2.6. Правила введения и исключения

пропозициональных связок

2.7. Структурные правила ИЕВ

2.8. Кванторные правила ИЕВ

2.9. Определение понятия «вывод в ИЕВ»

2.10. О семантической мотивировке ИЕВ

2.11. Недостаточность основных правил исчисления для представления фактических способов заключения

в математических доказательствах

2.12. Обоснование производного правила

исключения конъюнкции

2.13. Получение производных «правил опровержения»

2.14. Получение производного правила

«введения-исключения квантора существования»

2.15. Производное правило перехода от секвенций

к импликативным формулам

Глава третья. Вводные замечания о применении логико-предметных языков первой ступени для описания доказательств в первой книге «Начал» Евклида

3.1. Исторические "предшественники" «Начал»

3.2. Некоторые пояснения, относящиеся к базисным геометрическим представлениям Евклида

3.3. Об особенностях предлагаемой работы,

вытекающих из интуитивного характера представленных в книге Евклида математических доказательств

3.4. Выявление и точное описание фактически фигурирующих в «Началах» способов умозаключений - главная цель предлагаемой работы

3.5. Соображения о выборе первой книги «Начал»

в качестве предмета экспликации

3.6. О "переводе" евклидовых исходных формулировок в логико-предметные формулы

3.7. Анализ различных смыслов, в которых у Евклида употреблен термин «предложение»

3.8. Конкретные примеры "перевода" евклидовых исходных

формулировок в выражения логико-предметного языка

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

4.0. О "разделении" евклидовых «предложений»

первой книги «Начал» на две группы

4.1. О некоторых особенностях использования в предлагаемой работе чертежей

4.2. Невозможность экспликации евклидова доказательства предложения 4 первой книги «Начал»

4.3. Экспликация евклидова доказательства предложения 5

4.4. Экспликация евклидова доказательства предложения 6

4.5. Экспликация евклидова доказательства предложения 15

4.6. Экспликация евклидова доказательства предложения 18

4.7. Экспликация евклидова доказательства предложения 19

4.8. Экспликация евклидова доказательства предложения 24

4.9. Экспликация евклидова доказательства предложения 25

4.10. Экспликация евклидова доказательства предложения 26

4.11. Экспликация евклидова доказательства предложения 27

4.12. Экспликация евклидова доказательства предложения 28

4.13. Экспликация евклидова доказательства предложения 29

4.14. Экспликация евклидова доказательства предложения 30

4.15. Экспликация евклидова доказательства предложения 33

4.16. Экспликация евклидова доказательства предложения 34

4.17. Экспликация евклидова доказательства предложения 1

4.18. Экспликация евклидова доказательства предложения 9

4.19. Экспликация евклидова доказательства предложения 10

4.20. Экспликация евклидова доказательства предложения 11

Заключение

Библиографический список литературы

Введение диссертации (часть автореферата) на тему «Генценовское исчисление естественных выводов как средство экспликации форм интуитивных умозаключений в трудах античных математиков»

Введение.

Актуальность темы

Человеку, приступающему к изучению современной математической логики, может показаться, что последняя является "изобретением" последнего времени. Однако, соответствуя в главном действительности, этот взгляд требует некоторой, как представляется, вполне оправданной корректировки.

Такое представление о возникновении той или иной научной дисциплины, при котором идет речь об "изобретении" последней, превращает ее в своеобразное "deus ex machina", что в отношении логики менее всего применимо.

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

¿с ^

определенного рода параллелизм начальных шагов современной математической логики и современной алгебры - и та, и другая во многом "исходили" из чисто интуитивного оперирования со своими объектами, - в случае математической логики такими объектами являлись определенного рода "предложения", в случае же алгебры - некоторые алгебраические структуры.

Наконец, математиками была осознана настоятельная необходимость параллельного уточнения наряду с базисными

представлениями чисто математического характера также и свойств логических операций с этими представлениями.

«Если мы изобразим точками всю совокупность положений какой-либо математической дисциплины, например, элементарной геометрии, и точку А, отвечающую какому-нибудь положению, будем соединять прямыми с В, С, Б, ..., как с положениями, из которых А выводится, то получим сеть, которая начинается в точках, отвечающих начальным, т.е. очевидным, положениям. Можно сказать, что математика обычно интересуется не самой сетью, а только ее узлами. Для нее важно указать какой-нибудь путь, ведущий от очевидных положений А, В, С, Б,... к интересующему его положению О, существование которого почему-либо подозревается и, если этот путь найден, то математик со спокойной совестью может сказать, что положение О им доказано. Более же глубоким, но еще не успевшим внедриться во все области математики является взгляд, по которому исследование логической сети является не менее важным, чем исследование ее узлов. Нужно предполагать, что логический анализ в будущем будет приобретать все большее и большее значение и интеллектуальная совесть математика будущего времени будет гораздо чувствительнее, он будет искать не какой-нибудь путь от А, В, С, ... к О, а путь определенного типа, идущий от наперед заданной части аксиом через положения определенных типов» [Мордухай-Болтовской, стр. 28].

В 30-е гг. нынешнего столетия немецким математиком и логиком Г. Генценом была построена система логического вывода, называемая «исчислением естественных выводов», достаточно адекватно представляющая структуру математического рассуждения. Сам Генцен в своей работе «Непротиворечивость чистой теории чисел» приводит пример применения исчисления естественных выводов к одному из исторически существующих математических доказательств, а именно, к евклидову доказательству теоремы о бесконечности простых чисел.

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

Поэтому оказывается оправданной попытка, учитывая все особенности представления математических структур в античности (первым из дошедших до нас и наиболее известным представителем этого античного восприятия математических объектов являются «Начала» Евклида) и придерживаясь точности и строгости, достигнутых в современной математической логике, показать, что интуитивные математические доказательства в евклидовых «Началах» возможно проинтерпретировать посредством схем правил, нашедших свое выражение в современных логико-математических исчислениях.

Степень разработанности темы.

Следует отметить тот факт, что другие примеры, кроме упомянутого примера, приводимого Генценом в работе «Непротиворечивость чистой теории чисел» и иллюстрирующего возможность применения исчисления естественных выводов к фактическим математическим доказательствам, проводимым в античности, - пример "расчлененного" доказательства теоремы Евклида: «Существует бесконечно много простых чисел», автору предлагаемого диссертационного исследования неизвестны.

Цели и задачи исследования.

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

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

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

2) Показать, что логика математического рассуждения до своего фактического закрепления в работах по математической логике в первой половине XX века развивалась как интуитивная система логических заключений в доказательствах математических предложений.

3) Продемонстрировать тот факт, что одним из оснований построения в 30-е гг. XX столетия Г. Генценом исчисления

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

Научная новизна результатов исследования.

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

- выявлен интуитивный характер возникновения и формирования одного из бурно развивающихся в настоящее время разделов современной математической логики;

- на конкретном примере показана непосредственная связь современных теоретических концепций математической логики с интуитивным оперированием с логическими структурами в математическом доказательстве;

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

Методология исследования.

Специфика темы и попытка найти "золотую середину" между, с одной стороны, необходимостью оставаться верным исторической "правде", а с другой, - соответствовать точности и строгости, являющихся характерной особенностью современных логико-математических языков, предопределили выбор основного метода предлагаемого исследования. Этим методом предлагаемой диссертационной работы служит метод историко-логической реконструкции.

Настоящая работа посвящена анализу тех способов рассуждений, которые уже в шестом веке до нашей эры систематически применялись античными математиками в процессах математических доказательств. Инструментом такого анализа будет служить исчисление естественных выводов (в секвенциальном варианте), созданное в 30-е годы XX столетия выдающимся математиком и логиком Герхардом Генценом и опубликованное в [Gentzen,1934-1935]. Исследование данной темы было предложено автору Шаниным H.A., и некоторые из результатов, нашедших свое выражение в этой работе, получены благодаря его советам и рекомендациям. Однако эта пока ещё слишком общая формулировка цели предстоящего исследования требует некоторых необходимых комментариев.

Во-первых, наш анализ способов рассуждений, нашедших свое выражение в античной математике, отправляется от конкретного произведения того времени - речь идет об известном произведении античной математики, о «Началах» Евклида.

Во-вторых, и данное обстоятельство нужно выделить особо, указанный анализ не затрагивает базисных представлений чисто геометрического характера, принимаемых в книге Евклида, но целиком относится к прояснению только логической структуры умозаключений с помощью математических моделей естественного языка, получивших своё развитие в конце XIX - начале XX веков. Таким образом, данное исследование относится не к истории математики, но к истории логики, и в нем почти не затрагивается генезис концепций античной математики.

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

"обобщённой" формулировки можно обосновать следующим обстоятельством.

Как указывает Н. Бурбаки,

«<...> Оригинальность греков (в сравнении, скажем, с древними египтянами и вавилонянами - А.Б.) заключается именно в их сознательных попытках расположить цепь математических доказательств в такую последовательность, чтобы переход от одного звена к следующему не оставлял бы места сомнению и завоевал общее признание» [Бурбаки, 1963 ,стр. 10].

Иначе говоря, эта констатированная Бурбаки «оригинальность» древнегреческих математиков проявляется прежде всего в их стремлении к строго логическому построению всего здания математической науки, а то, что дело обстояло именно так, лишний раз подтверждает знакомство с «Началами» Евклида. Хотя многие из достигнутых в античности математических результатов историки математики могут связать с тем или иным конкретным именем, однако вклад какого-либо отдельного математика в "логический фундамент" этого здания не удается специфицировать из-за отсутствия достоверных данных по этому вопросу. Этим в конечном счёте объясняется и то, что некоторые историки математики придерживаются той точки зрения, что способы умозаключений, служащие инструментами доказательств в «Началах» Евклида, приобрели определённого рода "устоявшийся" характер их интуитивного употребления в математических доказательствах уже во времена, более ранние, чем эпоха самого Евклида.

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

интуитивного употребления. Здесь мы основываемся на работах математика Б.Л. ван дер Вардена, математика и историка математики Д.Я. Стройка, а также историка математики Жмудь Л. Я.

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

СС ^

логических переходов в математических доказательствах к первой в истории логики отчетливо построенной системе схем умозаключений, согласно которым, по мнению автора этой системы, и должно строится любое корректное рассуждение. Речь идет о силлогистической системе Аристотеля. Согласно цитированному уже выше Бурбаки, заслуга Аристотеля

«<...> Состоит в том, что ему впервые удалось систематизировать и кодифицировать приёмы рассуждения, которые у его предшественников оставались неясными и несформулированными. Нам здесь следует особо выделить главный тезис этого труда (речь идет о «Первой аналитике» Аристотеля - А.Б.), а именно, что каждое корректное рассуждение можно свести к систематическому применению очень небольшого числа неизменных правил, независимых от частной природы объектов, о которых идет речь (независимость ясно обнаруживается обозначением понятий или высказываний с помощью букв, что, возможно, было заимствовано Аристотелем у математиков)» [Бурбаки,1963,стр.12].

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

Античные математики фактически не использовали правил, сформулированных Аристотелем в силлогистической форме, в качестве формальных инструментов своих доказательств. (Правда, некоторые силлогизмы, преобразованные в "современную форму", можно обнаружить у античных математиков в качестве иногда встречающихся

видов умозаключений, однако говорить о систематическом употреблении таких форм умозаключений, которые можно эксплицировать с помощью силлогистической системы Аристотеля, не приходиться). Дело в том, что Аристотель сформулировал схемы умозаключений лишь для весьма "узких" типов суждений. Именно поэтому (как убедительно показано в [Лукасевич,1959]) для обоснования некоторых силлогизмов, обозначенных Аристотелем как «несовершенные», последний интуитивно применяет такие формы умозаключений, которые выходят за рамки его системы.

С точки зрения математиков, силлогистическая система Аристотеля имеет тот существенный недостаток, что в языке, используемом при построении этой системы, не встречаются многоместные предикаты (см. [Hilbert, Ackermann, 1972,s.65-73], [Новиков, 1959,стр. 128]). В то же время в математических рассуждениях многоместные предикаты и многоместные предметные операции пронизывают всю структуру математики. Отметим, что в [Hilbert, Ackermann, 1972,s.43-63] для изложения аристотелевской системы в современном виде вводится специальное исчисление -«исчисление классов» («der Klassenkalkul»).

«<.. .> Введение в рассмотрение предикатов от нескольких переменных, способных выражать отношения между предметами, приносит существенно новое по сравнению с логикой предикатов от одного переменного. Оказывается, что во всех системах аксиом математических дисциплин существуют аксиомы, не выразимые посредством предикатов от одного переменного» [Новиков, 1959,стр. 129].

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

языке посредством двухместного предиката, трехместное отношение между точками «не лежать на одной прямой» и т.п.

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

Использование современного логико-предметного языка 1-й ступени дает возможность в полной мере отразить фактическую роль многоместных предикатов и многоместных операций в «Началах» Евклида, а генценовское исчисление естественных выводов оказывается подходящим средством для адекватной экспликации форм интуитивных умозаключений в упомянутом произведении. Обоснование этих

и с* и

утверждении является основной целью настоящей работы.

Глава первая.

О выборе подходящей современной дедуктивной системы для экспликации евклидовых доказательств.

1.1. Одним из первых, кто явно выразил мысль, что способы умозаключений, применяемые математиками в своих доказательствах, в некоторых случаях имеют несиллогистическую форму, был, по всей видимости, Г.-В. Лейбниц.

«И евклидовы доказательства чаще всего представляют аргументацию по форме; хотя он пользуется, по-видимому, энтимемами, но устраненное предложение, которое как будто отсутствует, дополняется ссылкой на полях, дающей возможность найти его уже заранее доказанным; это значительно сокращает ход доказательства, нисколько не ослабляя силы его. Все эти обращения, сложения и разделения доводов, которыми он пользуется, - всего лишь особенные, свойственные математике и ее предмету разновидности форм аргументации, и математики доказывают эти формы с помощью всеобщих форм логики. Кроме того, следует помнить, что существуют правильные асиллогистические выводы, которые нельзя доказать строгим образом при помощи каких бы то ни было силлогизмов, не изменяя несколько терминов их. И само это изменение терминов представляет асиллогистический вывод» [Лейбниц,1983,стр.493].

1.2. До конца XIX и начала XX века среди философов считалось, что та «логика», которой пользуются в математическом исследовании, является традиционной логикой, которая в те времена связывалась только с именем Аристотеля и с силлогистической системой, по существу бывшей в те времена единственной формально выраженной системой логического вывода. Однако уже Лейбниц указывает на то, что наряду с этой силлогистической системой Аристотеля в античной геометрии

существовали способы рассуждений, которые можно обозначить как расширение методов «общей логики» на геометрические объекты.

«В самом деле, логика столь же доступна демонстративному познанию, как и геометрия, и можно сказать, что логика геометров, или методы доказательства, выясненные и установленные Евклидом применительно к теоремам, являются распространением или частным случаем общей логики» [Лейбниц, 1983,стр.377].

1.3. Кроме того, как явно выразил это обстоятельство тот же Лейбниц, математики по существу считали логическую составляющую своей науки неотъемлемой частью своих исследований, предпочитая либо оставить ее в неформализованном виде как присущую базисным представлениям математического характера, либо использовать для своих доказательств в готовом виде уже известную на то время систему логического вывода, которую представляла собой силлогистическая система Аристотеля (что было крайне редко, ибо носило несколько искусственный характер). Например, Лейбниц в своей работе «Новые опыты о человеческом разумении» упоминает про некоторые из попыток, которые предпринимались в XVI и XVII веках, чтобы изложить математические рассуждения, пользуясь силлогизмами (см. [Лейбниц, 1983,стр.368]). Сложившуюся ситуацию американский математик Роберт Р. Столл описывает следующим образом.

«В математической практике аксиоматические теории обычно описываются в виде неформальных теорий, что же касается предполагаемой при этом логики, то обычно считается, что это та интуитивная логика, которая усваивается в ходе изучения математики» [Столл, 1968,стр. 145].

1.4. Наконец, после работ Дж. Буля, А. де Моргана, Г. Фреге, Б. Рассела и А. Уайтхеда, Дж. Пеано, после получения Г. Кантором основных результатов теории множеств и после одновременного с этим открытия знаменитых теоретико-множественных парадоксов, математиками была

осознана настоятельная необходимость параллельного уточнения, наряду с базисными представлениями математического характера, тех способов умозаключений, которые применяются в математических доказательствах. Уже в 1904 году Д. Гильберт формулирует следующий тезис:

«Обычно считают арифметику частью логики и при обосновании арифметики большей частью предполагают традиционные основные идеи логики известными. Однако, внимательно присматриваясь, мы замечаем, что при обычном изложении законов логики применяются уже некоторые основные понятия арифметики, как-то: понятие множества, частично понятие числа, особенно в смысле количества. Мы попадаем, таким образом, в порочный круг, а потому для избежания парадоксов необходимо в некоторой части одновременное развитие и законов логики, и законов арифметики» [Гильберт, 1948,стр.325].

1.5. Одной из фундаментальных предпосылок такого осознания стало построение в начале XX века математических моделей "сравнительно обширных" фрагментов естественных языков, - таких моделей, которые, отвлекаясь от некоторых особенностей этих языков, делают вполне обозримой (благодаря «деревьям синтаксического разбора») смысловую структуру языковых конструкций, предоставляя, таким образом, возможность отчетливого описания форм умозаключений, фактически осуществляемых в математических доказательствах. В настоящей работе привлекается тот логико-предметный язык, который используется в исчислении предикатов 1 -й ступени с предикатными и функциональными константами (исчислении, называемого в

[Hilbert,Ackermann] также «узким исчислением предикатов»).

1.6. При выборе подходящего формализма для экспликации форм интуитивных умозаключений в доказательствах античных математиков мы руководствовались следующими соображениями.

Как указывает Д. Правиц, Лукасевич на своих семинарах в 1926 году «привлек внимание к тому факту, что в процессе неформального

математического рассуждения никто не следует логическим системам Фреге, Рассела и Гильберта, т.е. не строит выводы из аксиом (или теорем) с помощью (прямых) правил заключения. Вместо этого чаще всего применяется метод выведения заключений из допущений»[Правиц,1997, стр.90].

Знакомство с текстом первой книги евклидовых «Начал», которая является предметом нашего анализа, показывает, что между формализмом гильбертовского типа и интуитивным, неформальным выводом геометрических предложений в данной книги нет видимого сходства. Характерным свойством логических систем гильбертова типа является использование большого числа логических аксиом и небольшого числа правил заключения, с помощью которых происходит переход от одного выражения к другому. Гораздо более "естественной" для экспликации форм интуитивных умозаключений, осуществляемых в математических доказательствах, оказывается логическая система, которая формализует «введение допущений» и одновременно с этим предоставляет в наше распоряжение большое число правил заключения, которые разрешают переход от одних языковых конструкций к другим. Именно упоминаемый Правицем «метод выведения заключений из допущений» использован Евклидом в доказательствах геометрических предложений первой книги «Начал».

1.7. Систему правил вывода, которая основывается на систематическом использовании метода «введения допущений», построили в тридцатые годы XX века независимо друг от друга польский математик Ст. Яськовский и немецкий математик Г. Генцен. Как отмечает уже цитированный выше Правиц, «генценовский вариант натурального вывода является <...> более естественным» [Правиц, 1997,стр.ХУП], то есть, более адекватно описывающим структуру математического рассуждения. Надо отметить то обстоятельство, что Генцен построил свое исчисление в двух различных вариантах, а именно, первый и более ранний

вариант этого исчисления - в форме так называемого «древовидного вывода» (в работе «Untersuchungen über das logische Schließen»,1934-1935), и второй, по времени более поздний вариант - в форме так называемого «секвенциального исчисления» (в работе «Die Widerspruchsfreiheit der reinen Zahlentheorie», 1936,§5).

1.8. Немецкий термин «natürlichen Schließen» допускает двойной перевод на русский язык: как «натуральный вывод», так и «естественный вывод». Именно второй вариант перевода указанного немецкого термина на русский язык использовался в лекциях H.A. Шанина, слушателем которых был и автор настоящей работы, и под таким названием -«исчисление естественных выводов» - система Генцена фигурирует в этой работе.

1.9. Кроме того, следует отметить тот факт, что сам Генцен в работе «Непротиворечивость чистой теории чисел» дал пример расчлененного доказательства теоремы Евклида: «Существует бесконечно много простых

9

чисел», - пример, иллюстрирующий сформулированные им правила «естественного вывода». Это "расчленение" касается только одной евклидовой теоремы, относящейся к арифметике, и более современного, чем у Евклида, доказательства этой теоремы.

Иные примеры такого рода, касающиеся анализа применявшихся Евклидом форм умозаключений средствами современного аппарата логического вывода, автору настоящего исследования неизвестны.

Глава вторая.

Описание генценовского исчисления естественных выводов (секвенциальный вариант).

2.0. Поскольку в качестве средства экспликации интуитивных способов умозаключений, используемых Евклидом для доказательства геометрических предложений в первой книге «Начал», мы выбрали генценовское исчисление естественных выводов, необходимо в первую очередь точно описать подходящий для наших целей секвенциальный вариант этого исчисления.

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

=> применяется в качестве знака секвенции. (Заметим, что эта символика в некоторых пунктах отличается от принятой в [Генцен,1967]).

Далее, в отличие от Генцена (а также от Гильберта и Бернайса) мы будем использовать такой вариант логико-предметного языка, в котором не вводятся отдельно связанные и свободные предметные переменные, но вхождения предметных переменных в формулы классифицируются на связанные и свободные (см., например, [Клини,1973]). Тексты Евклида наиболее естественно "вкладываются" именно в такой вариант логико-предметного языка.

2.2. Рассмотрим структуру естественного вывода в его секвенциальной форме. Естественный вывод представляет собой некоторую последовательность выражений вида Рх, Р2Р„=><2 ,

называемых секвенциями, в которых формулы, стоящие слева от знака =>,

образуют антецедент секвенции. (Если рассматривать вывод в

целом, построенный из некоторой последовательной цепочки секвенции, антецеденты секвенций составляют, так сказать, "память" вывода, роль которой заключается в том, чтобы явно фиксировать те допущения, от которых зависит формула, стоящая справа от знака секвенции). Формула, расположенная справа от знака =>, называется сукцедентом секвенции и выполняет роль, так сказать, "рабочей части" вывода, в которой и происходит непосредственное преобразование тех или иных формул. Сам знак => называется знаком секвенции и служит для того, чтобы на каждом шаге вывода отделять "память" вывода от его "рабочей части". Секвенцией называется любое выражение вида

где Р1,Р2,...,Рп (п>0), являются формулами. В случае, если п=0, "память" вывода не содержит допущений, от которых зависит его "рабочая часть". Выражение «=> С>» также является секвенцией и имеет следующий смысл: «без каких-либо допущений имеет место С>».

2.3. Допустим, что мы располагаем некоторым списком специфических аксиом, определяющих те или иные связи, существующие между базисными объектами рассматриваемой теории, - к примеру, в нашем случае такими специфическими аксиомами будут выступать те аксиомы, которые сформулированы Евклидом под именем «общие понятия» в самом начале первой книги. Обозначим специфические аксиомы через А:, А2,..., Ап{п> 1), а их список - посредством А. Тогда возможными началами процесса логического вывода будут:

1. Упоминание одной из специфических исходных аксиом

=>А„ где \ <1<И,

2. Введение какого-либо допущения Р (в качестве Р может выступать любая формула нашего языка)

Р=>Р.

Выражение вида «Р => Р» называется тривиальной

исходной секвенцией (сокращенная запись: ТИС). Это выражение имеет следующий смысл:

(а) если формула Р является замкнутой формулой нашего языка, то секвенция вида «Р => Р» читается как: «допустим Р, тогда имеет место Р»;

(б) если формула Р имеет какие-либо параметры, то тривиальная исходная секвенция вида «Р => Р» имеет такой смысл: «пусть значения параметров а1,а2,...,ак (к > 1) таковы, что имеет место Р, тогда при тех же самых значениях параметров а1,а2,...,а1с имеет место Р»;

Любая дальнейшая секвенция вывода может иметь один из видов (1) - (2), либо представляет собой результат применения одного из постулируемых ниже правил исчисления естественных выводов к некоторым построенным ранее секвенциям.

2.4. Основные правша естественного вывода.

Различают три типа таких правил.

Правила введения и исключения пропозициональных связок: конъюнкции « & », дизъюнкции «V », импликации «->», эквивалентности «<->» и отрицания « -1».

Структурные правила (их роль заключается в чисто структурном преобразовании антецедента секвенции).

И, наконец, правила введения и исключения квантора общности «V» и квантора существования «3 ».

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

2.5. Если мы ограничиваемся набором специфических аксиом, правилами вывода для пропозициональных связок и структурными правилами, то получающаяся при этом часть исчисления естественных выводов называется пропозициональной частью исчисления над списком специфических аксиом А (сокращенное обозначение: ИЕВ~). При добавлении же кванторных правил получается исчисление над списком специфических аксиом А (сокращенное обозначение: ИЕВЛ). Часто, однако, список специфических аксиом пуст, и соответствующие обозначения исчисления естественных выводов имеют вид: ИЕВ" и ИЕВ.

2.6. Правила введения и исключения пропозициональных связок. В следующих ниже правилах заглавные греческие буквы Г,Е,П...

символизируют какие-либо списки формул (возможно, пустые), а заглавные латинские буквы Р, <3, Я, 8 - какие-либо формулы. (1) Правило введения конъюнкции. Г =>Р

Пр+& *=>()

Г,Е=>(Р&0)

(2) Правила исключения конъюнкции.

Г=>(Р&д)

Пр&{а) ПР&{6)

Г =>Р Г => (Р & 0

Г=>0

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

(3) Два правила введения дизъюнкции.

ПрЦа) Пр+Лб)

Г => (Р V 0

Г => (Р V 0 (4) Правило исключения дизъюнкции.

r=>(ivß) ПР: T1,Q=*R

Г,2,П=>Д

Это правило называется также правилом «разбора возможных случаев».

(5) Правило введения импликации (называемое также правилом «освобождения от допущения»).

Г ,P=>Q

Пр\ --—-

Г =>(P^Q)

(6) Правило исключения импликации (обобщенное правило modus ponens).

Г =>Р

Пр" £=>(Р-»0

Г,

(7) Правило введения эквивалентности.

Г=>(Р->0

(8) Два правила исключения эквивалентности. Лр0( а)

Пр'^б)

Г => (-Р -> 0 Г=>(Р^0

(9) Правило «опровержения».

Пр; Е, Р => -i <2

Г, Е ^ -п Р

(10) Правило «удаления двойного отрицания». Пр

2.7. Структурные правила исчисления естественных выводов.

Правило перестановки допущений в антецеденте

(данное правило выражает интуитивно очевидную возможность размещения допущений в "памяти" в любом порядке).

Пр.стр. 1 -

Правило устранения повторений допущения. Пр.стр.2

Правило утончения в антецеденте.

Г^Р

Пр.стр. 3

2.8. Кванторные правила.

Несколько предварительных соображений относительно использования данных правил в описываемом варианте исчисления естественных выводов. В формулировках правил «исключение квантора общности» и «введение квантора существования» фигурирует условие «формула Р, переменная а и терм Т согласованны». В терминологии, принятой в [Клини,1973,стр.180] это условие получает следующее выражение: «терм г свободен для переменной х в формуле А(х)».

Ниже выражение \_Р I" ] обозначает результат подстановки в формулу Р терма Т вместо всех свободных вхождений переменной а.

Итак, кванторные правила исчисления естественных выводов.

Правило введения квантора общности «V ».

а- переменная,

а не входит свободно в Г

Г^УаР

Правило исключения квантора общности «V ».

Яр*

Г^УаР

а - переменная,

Т - однотипный с переменной а,

формула Р, переменная а и терм Т - согласованы

г=>[р1ат\

Правило введения квантора существования «3».

Г=>1Р±ат\

а - переменная,

Пр^ Т — терм, однотипный с переменной а,

формула Р, переменная а и терм Т - согласованы

Правило исключения квантора существования «Э ».

переменная а не входит свободно в "Ей Я

2.9. Далее определяется понятие «вывод в исчислении естественных выводов». Выводом в данном исчислении ИЕВА называется любой список секвенций ^,¿>2,..., , такой, что при любом) (] = 1,2,...,р) SJ является

либо специфической исходной секвенцией, либо тривиальной исходной секвенцией, либо получено из некоторых предшествующих ей в этом списке секвенций по одному из описанных правил вывода. Секвенция 50 называется выводимой в ИЕВ А, если можно построить такой вывод, в котором последний член графически совпадает с ^. Формула Р называется выводимой в ИЕВ А, если выводима секвенция => Р.

2.10. Исчисление естественных выводов имеет определенную семантическую мотивировку. Каждой секвенции Рх,Р2,...,Рп =><2 (п > 0) ставится в соответствие определенная формула Ф[Р1,Р2,...,Рп называемая формульным образом данной секвенции и определяемая следующим образом:

ф[Рх,Р2,...,Рп =>0] = е,еоши = 0;и

с1е/

Ф [р,, Р2Р„ => 0] = ((Р, &Р2 &...&Р„ )-»£>), еслип>0.

щ

Теорема о семантической корректности исчисления естественных выводов гласит:

если все специфические аксиомы тождественно-истинны, то формульный образ любой выводимой формулы будет также тождественно-истинной формулой.

Обоснование этой теоремы имеет финитный характер, если все предметные области, рассматриваемые в данной теории, конечны. Если же встречаются бесконечные области, то для обоснования привлекаются идеализации, используемые в теории множеств.

2.11. При экспликации интуитивных математических доказательств оказывается, что основных правил исчисления зачастую явно недостаточно для выражения тех форм интуитивных умозаключений, которые фактически использовались для вывода доказываемых положений. Однако имеется возможность формулировки разнообразных «производных» правил вывода (т.е. правил, не входящих в список «основных», но таких, что любое их применение заменимо некоторой последовательностью применений «основных» правил, - таким образом, производные правила играют роль определенного рода удобных «сокращений» цепочек применения основных правил исчисления). В теории логического вывода накоплен обширный набор таких правил и некоторые из них оказываются уместными при экспликации форм интуитивных умозаключений в «Началах» Евклида. Поэтому для упомянутой экспликации необходимо располагать подходящим для этой цели набором производных правил вывода.

Поскольку в настоящей работе в качестве предмета анализа форм интуитивных умозаключений в математических доказательствах с позиции

исчисления естественных выводов генценовского типа

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

2.12. Вышеописанные правила исключения конъюнкции исчисления естественных выводов имеют такой вид:

ПрЦа) Г =>(Р&0 Т^Р

ПрЦб) Г =>(Р&0

Таким образом, указанные правила исключения конъюнкции

44 55 »•»

позволяют получать на выходе лишь первый и второй конъюнктивные члены, тогда как в первой книге евклидовых «Начал» имеется целый ряд таких предложений, для анализа логических переходов в доказательствах которых в исчислении естественных выводов привлекается обобщенное правило исключения конъюнкции, разрешающее из любой произвольной к-членной конъюнкции получать любой ьтый член последней. Это обобщенное правило получения любого произвольного конъюнктивного члена является в системе ИЕВ А производным, потому что может быть заменено цепочкой применения основных правил исключения конъюнкции.

Обоснование производности этого обобщенного правила исключения конъюнкции.

Поскольку конъюнкция ассоциативна, то формула

г =>0?, & р2 &... & р1 &... & рк_2 & рк_г & рк)

представляет собой определенного рода сокращение формулы

Итак, вывод в ИЕВ формулы р1.

[1] Г=>(((((((Р, &Р2)&...)&Р,)&...)&Рк_1)&Рк_1)&Рк)

[исходная секвенция]

[2] Г^((((((Р1&Р2)&...)&^)&...)&^-2)&Л-1) [1 ,Пр1(а)-\

[3] Г^(((((Р1&Р2)&...)&Р/)&...)&А-2) Р ,Пр-&(а)]

[1 + 1] Г =>(((/>&Р2)&...)&Р,) [иПрЦа)}

[/ + 2] Г^Р, [/ + 1 ,Пр1Ш Таким образом, можно сформулировать обобщенное правило исключения конъюнкции, являющееся в системе ИЕВ производным.

Г =»(/>&Р2 &...&/> &...&/»,) .

Пр.пр. 1 -, где (1<г<£) .

г => р;

2.13. Евклид в своих доказательствах некоторых геометрических предложений первой книги «Начал» очень часто применяет метод «доказательство от противного». Для того, чтобы адекватно эксплицировать формы интуитивных логических переходов, употребляемых Евклидом в этих случаях метода «доказательство от противного», нам потребуется ряд производных правил для отрицания. В упомянутой выше работе «Непротиворечивость чистой теории чисел» Генцен приводит список таких правил (см. [Генцен,1967,стр.101]). Но для экспликации интуитивных евклидовых логических переходов в доказательствах предложений первой книги «Начал» нам необходимы лишь два производных правила из этого списка. Это следующие правила:

и

Г,Е =>-|Р

пр:12] г ^р

Для обоснования первого из этих производных

правил покажем, что из данных посылок выводится искомое заключение.

[1] И,Р-=>() [данная посылка]

[2] 2 :=> (Р —» 0 [1 ,Пр1]

[3] => ((Р —> —> (—1 —> —: Р)) [выводимая в ИЕВ формула]

[4] [2,3, ад

[5] Г => -10, [данная посылка]

[6] Г, Е=>-1Р [5,4

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

[1] Г => Р [данная посылка]

[2] Г => (Р V 0 [1, Пр* ]

[3] => ((Р V 0 ->• (-1Р 0) [выводимая в ИЕВ формула]

[4] г => (-1 р -> 0 [2,з, ад

[5] 2 => -1Р [данная посылка]

[6] [5,4, ад

[7] [6, Пр.стр. 1]

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

заключение о том, что допущение, исходя из которого

постулируются возможные случаи, не может соответствовать действительности.

Для адекватной экспликации указанного логического перехода в доказательствах Евклида нам требуется производное правило исчисления естественных выводов, имеющее следующий вид:

Пр.пр.2 Г,S^(PvQ)

П^-иб

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

[1] Е -IР [данная посылка]

[2] П => -л () [данная посылка]

[3] 2,п=>(-,р&-,0 РА ад

[4] => ((-л Р & -I 0 -1 (Р V 0) [выводимая в ИЕВ формула]

[5] =>((-п?&пб)^(?у0) [4 ,Пр-„(а)]

[6] 2,П=>-,(Ру0 [3,5, Яр;]

[7] Г, 5 => (Р V 0 [данная посылка]

[8] 2,П,Г=>-,5 [6,7 ,Пр:т]

[9] [8,Пр.стрЛ]

2.14. В так называемых задачах на построение Евклид применяет и такие формы интуитивных умозаключений, адекватная интерпретация которых посредством предложенного Генценом секвенциального исчисления естественных выводов наряду с основным правилом исключения квантора существования требует введения в систему исчисления естественных выводов также и производного правила

исключения квантора существования. Основное

правило исключения квантора существования, как уже указывалось, имеет такой вид:

Г => ЗаР

2,Р=>Р

переменная а не входит свободно в £ и Р

Тогда как производное правило исключения квантора существования можно представить следующим образом.

Г=> ЗаР

Пр.пр~

Таким образом, это производное правило исключения квантора существования представляет собой по существу правило исключения -введения квантора существования. Поэтому в дальнейшем оно будет называться правилом «исключения-введения квантора существования».

Для обоснования «производности» данного правила «исключения-введения квантора существования» покажем, что при данных посылках и при использовании основных правил исчисления естественных выводов "на выходе" действительно получается требуемое заключение.

[1] Г За Р [данная посылка]

[2] 2, Р =><2 [данная посылка]

[3] [2,Пр+3]

[4] Г,£ => 3а <2 [1,3,Пр^, где ЗaQ выполняет роль Р

основного правила исключения 3 ]

В доказательствах некоторых из своих предложений там, где он применяет метод «доказательство от противного», Евклид использует следующий способ заключения: построив какой-либо геометрический объект (такому построению в «теоремах о существовании» сопоставляется суждение о существовании заданного геометрического объекта), он показывает, что высказывания об этом объекте ведут к противоречию; на

основании этого он делает заключение о том, что то

положение вещей, при допущении которого осуществлялось построение какого-либо геометрического объекта, в действительности не может иметь место. Для адекватной экспликации этого евклидова способа заключения употребляется следующее производное правило исчисления естественных выводов:

Г,Д=>3 аР

Пр.пр.Ъ П б

а не входит свободно в Е, П, Я Г, Е, П => -1Я

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

[1] Г, Я => 3 а Р [(данная посылка]

[2] Т,,Р =><2 [данная посылка]

[3] П, Р => -1 [данная посылка]

[4] Х,Р,П,Р=>^Я [2,3 ,ПР:[2]]

[5] Е,Р, [4,Пр.стр.2]

[6] Г, Я, Е, П => -1Я [1,5, Пр^, при условии, что а не входит свободно

вТ,Ъ,П,Я]

[7] Г,Е,П,Д=>^Д [6, Пр.стр. 1]

[8] Г,2,П=>(Д->-,Д) [1,Пр^]

[9] => ((Л —> —1 К) <-> —1 К) [выводимая в ИЕВ формула]

[10] [9, Пр^ (а)]

[11] [8,9,Пр~Л

2.15. Очень часто в своих доказательствах Евклид интуитивно употребляет следующий прием рассуждения, считая его вполне очевидным: при доказательстве суждений вида ((д, & Д2 &... & Р) в

конце процесса доказательства, введя допущения Дх, Д2,..., Дп, он просто

упоминает о том, что при данных допущениях ДХ,Д2,..., Д„ имеет место

искомое положение дел, описываемое формулой Р.

Данный чисто интуитивный ход евклидова рассуждения можно обосновать в качестве производного правила вывода в исчислении естественных выводов, употребляя для этого обоснования основные правила исчисления. Данное производное правило вывода в ИЕВ делает оправданным логический переход от секвенций вида Дх,Д2,...,Дп =>Р к секвенциям вида =*((Д1&Д2&...&Д„)->Р).

Дх,Д2,...,Дп => Р ПрлрА —т-,-,

Обоснование этого правила как производного правила исчисления естественных выводов.

[1] Д1,Д2,...,ДП=>Р [исходная секвенция ]

[2] (Д1&Д2&...8сД„)=>(Дх&Д2&...&Дп) [ТИС]

V

я

[3] Н^Д„ [2, Пр~& (б)]

[4] ДХ,Д2,,...,ДП_Х^(ДП->Р) [\,Пр^]

[5] Н,ДХ,Д2,...,ДП_Х => Р [ЗД Яр"]

[6] Я [2,Пр.пр.\]

[7] Н,ДХ,Д2,...,ДП_2^{ДП_Х^Р) [5 ,Др*]

[8] Н,Н,ДХ,Д2,...,ДП_2 =>Р [6,7,Др"]

[т] Я, Н,...Н, ^Р [т-2,т-\, Пр" ] [т +1] Я, Я,..., Н,_х Р [т, Пр.стр.2]

[т + 1] Н => Р [т + (1-1), Пр.стр.2]

[т + 1 +1] =>((Д1&Д2&...&Д„)^Р) [т + 1,Пр\]

Заключение диссертации по теме «Логика», Бирюков, Александр Викторович

Заключение.

Подведем некоторые итоги изложенному выше. Как мы видим, в своих доказательствах геометрических предложений в первой книге «Начал» Евклид на интуитивном уровне пользуется такими способами умозаключений, которые можно эксплицировать посредством современной теории логического вывода - исчисления естественных выводов, предложенного в 30-е гг. нынешнего века математиком и логиком Генценом.

Труды Аристотеля и его преемников, по-видимому, не оказали заметного влияния на математику. Греческие математики в своих исследованиях шли по пути, проложенному пифагорейцами и их последователями в IV в. (Теодором, Теэтетом, Евдоксом), и мало интересовались формальной логикой при изложении своих результатов. Это не должно вызывать удивления; достаточно сравнить гибкость и точность математических рассуждений, которое имело место начиная с этого периода, с весьма рудиментарным состоянием аристотелевой логики» [Бурбаки,1963,стр.14].

Это по выражению Бурбаки «весьма рудиментарное состояние аристотелевой логики» можно объяснить одним: Аристотель ограничивается лишь сравнительно частным случаем логических отношений, - отношений, существующих между понятиями, или терминами; он не анализирует в явной форме в своей силлогистической системе логические отношения между предложениями (или, как называет эти языковые конструкции Бурбаки, «полностью неопределенными высказываниями», - см. [Бурбаки, 1963,стр. 13])

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

АпВ = 0 (примечание Бурбаки: «соответствующие формулы Аристотеля "Всякое А есть В" и "Некоторое А есть В"», - А.Б.) и способ сцепления этих отношений или их отрицаний по схеме

АаВиВаС)^(А^С). Аристотель все же был достаточно знаком с математикой своей эпохи и не мог не заметить, что подобные схемы были недостаточными для описания всех логических операций математиков, ни тем более для других применений логики» [Бурбаки,1963,стр.12-13].

Сам Аристотель иногда пользуется такими способами интуитивных умозаключений, которые выходят за рамки его силлогистической системы. Некоторым примером может служить аристотелево обоснование положения: «из истинных [посылок] нельзя вывести ложное заключение». (Примем, что переменная без знака отрицания обозначает истинное высказывание, а со знаком отрицания - ложное высказывание).

Рассуждение Аристотеля:

Итак, что из истинных [посылок] нельзя вывести ложное заключение, явствует прежде всего из следующего. Если при наличии А необходимо есть Б, то, если нет Б, необходимо нет и А. Следовательно, если А истинно, то необходимо истинно и Б; иначе окажется, что одно и то же вместе есть и не есть, что невозможно» [Аристотель,Первая аналитика, 53в 10-15].

Детализируем это рассуждение Аристотеля, используя для этого генценовское исчисление естественных выводов в его секвенциальном варианте.

Пусть если есть А, имеет место и Б".

Это высказывание можно рассматривать в виде следующей секвенции: "при допущении А имеет место Б": А => Б.

Далее Аристотелем применяется метод «доказательство от противного»: "предположим, что при допущении А не имеет место Б".

Ниже для обозначения ситуации "X не имеет место" употребляется форма записи: -,х). а=>->б.

Два высказывания приводят к противоречию: а=> б и а=>->б. На основании этого Аристотель делает заключение: «если нет Б, необходимо нет и А». Если а=> б и Л =>-.£, то =>->а.

Следовательно, если А истинно, то необходимо истинно и Б <. .>» [Аристотель, Первая аналитика, 53Ы4].

Для экспликации интуитивного логического перехода, который имеет место у Аристотеля в данном фрагменте его рассуждения, можно привлечь еще одно «правило заключения для отрицания», упоминаемое Генценом в работе «Непротиворечивость чистой теории чисел» (см. [Генцен,1967,стр.101]). Это правило имеет вид: Г г=>(Р->0'

Вернемся к рассуждению Аристотеля. В виде секвенций последнее можно проинтерпретировать следующим образом.

Если нет А, то, следовательно, если А истинно, то необходимо истинно и Б".

-,а

Л->£).

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

Следовательно, прав был Лукасевич, утверждая в своей работе «Аристотелевская силлогистика с точки зрения современной формальной логики»:

Никто не может вполне понять аристотелевские доказательства, если не знает, что, кроме аристотелевской системы, существует еще другая система логики, более фундаментальная, чем теория силлогизма. Это -логика предложений» [Лукасевич, 1959,стр.92].

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

Однако на том основании, что А положено как один термин, нельзя полагать, что при наличии чего-то одного с необходимостью вытекает что-то [другое], ибо это невозможно. Ведь то, что вытекает с необходимостью, есть заключение, а для того, чтобы получилось заключение, требуется по меньшей мере три термина и два их сочетания, т.е. две посылки. Следовательно, если истинно, что всему тому, чему присуще Б, присуще А, и всему тому, чему присуще В, присуще Б, то чему присуще В, необходимо присуще А; и это не может быть ложно, ибо иначе одно и то же было бы вместе присуще и не присуще. Таким образом, А положено как одно, но охватывает две посылки» [Аристотель,Первая аналитика, 53в 15 -23].

Указанные трудности проистекают из недостаточности силлогистической системы.

Эта аристотелевская теория доказательства имеет существенный недостаток: она предполагает, что все проблемы могут быть выражены посредством четырех видов силлогистических посылок и что, следовательно, категорический силлогизм является единственным инструментом доказательства. Аристотель не осознает, что его же собственная теория силлогизма служит примером, свидетельствующим против этой концепции. Будучи импликациями, модусы силлогизма являются предложениями иного рода, чем посылки силлогизма, но тем не менее они являются истинными предложениями, и если какое-нибудь из них не самоочевидно и не доказано, то оно требует доказательства своей истинности. Это доказательство, однако, не может быть дано средствами категорического силлогизма, потому что импликация не имеет ни субъекта, ни предиката, и было бы бесполезно искать средний термин между несуществующими крайними» [Лукасевич,1959,стр.87].

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

Не обязательно всегда требовать, чтобы термины были выражены [одним только] словом, ибо часто встречаются сочетания слов, для которых нет [равнозначного им] имени. Поэтому силлогизм с такого рода терминами трудно бывает свести [к одной из фигур]. А иногда делают ошибку именно из-за такого рода попытки, как если бы предположили, что имеется силлогизм без средних терминов. Пусть А означает два прямых угла, Б - треугольник, а В - равнобедренный. А присуще В через Б; А же присуще Б не через что-то другое, ибо треугольник сам по себе имеет [в совокупности] два прямых угла. Так что для посылки АБ, которая хотя и может быть доказана, не будет среднего термина. Очевидно, таким образом, что средний термин не всегда следует брать как определенное нечто, но что иногда следует брать его как сочетание слов, как это имеет место и в только что приведенном примере» [Аристотель,Первая аналитика, 48а 29-39].

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

Список литературы диссертационного исследования кандидат философских наук Бирюков, Александр Викторович, 1999 год

Литература.

1. [Александров, 1987]: Александров А.Д. Основания геометрии, Москва, 1987.

2. [Аристотель, Первая аналитика] в: Аристотель, Сочинения в четырех томах, том 2, Москва, 1978.

3. [Бурбаки,1963]: Бурбаки Н. Очерки по истории математики, Москва, 1963.

4. [Ван дер Варден, 1959]: Ван дер Варден Б. Л. Пробуждающаяся наука, Москва, 1959.

5. [Waerden В. L.van der, 1978]: Waerden В. L., van der. Die Postulate und Konstruktionen in der frühgriechieschen Geometrie, in: AHES, 1978, bd. 18, s. 343-357.

6. [Евклид]: Начала Евклида, книги I - VI, Перевод с греческого и комментарии Д. Д. Мордухай-Болтовского, Москва - Ленинград, 1948.

7. Гильберт Д, Основания геометрии, Москва - Ленинград, 1948.

8. [Гильберт, Бернайс, 1982]: Д. Гильберт, П. Бернайс, Основания математики. Логические исчисления и формализация арифметики, Москва, 1982.

9. [Hilbert, Ackermann, 1972]: D. Hilbert und W. Ackermann, Grundzüge der theoretischen Logik, 6. Auflage, Berlin, Heidelberg, New York, 1972.

10.[Генцен, 1967]: Генцен Г. Непротиворечивость чистой теории чисел, в: Математическая теория логического вывода, Москва, 1967.

1 l.[Gentzen, 1934-1935]: Gentzen G., Untersuchungen über das logische Schließen, I-II, in: Karel Berka, Lothar Kreiser, Logik-Texte, Berlin, 1971.

12.[Жмудь, 1990, стр. 300-325]: Жмудь JI. Я. Пифагор как математик, в: Историко-математические исследования. Выпуск 32-33, Москва, 1990, стр. 300-325.

13.[Клини, 1973]: Клини С. К. Математическая логика, Москва, 1973.

14.[Лейбниц, 1983]: Лейбниц Г. В. Новые опыты о человеческом разумении, в: Сочинения в 4-х томах, том 2, Москва, 1983.

15.[Лукасевич, 1959]: ЛукасевичЯ. Аристотелевская силлогистика с точки зрения современной формальной логики, Москва, 1959.

16.[Мордухай-Болтовской, 1998]: Мордухай-Болтовской Д. Д. Философия, психология, математика, Москва, 1998.

17.[Новиков, 1959]: Новиков П. С. Элементы математической логики, Москва, 1959.

18. Patzig G. Die aristotelische Syllogistik. Logisch-philologische Untersuchungen über das Buch A der "Ersten Analytiken", Göttingen, 1959.

19.[Погорелов, 1979]: Погорел ob A.B. Основания геометрии, Москва, 1979.

20.[Правиц, 1997]: ДагПравиц. Натуральный вывод. Теоретико-доказательственное исследование, Санкт-Петербург, 1997.

21.[Столл, 1968]: Столл Р. Роберт. Множества. Логика. Аксиоматические теории. Москва, 1968.