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

Текст диссертации на тему "Генценовское исчисление естественных выводов как средство экспликации форм интуитивных умозаключений в трудах античных математиков"

6/ 99-9/з 40

Санкт-Петербургский государственный университет Философский факультет Кафедра логики

На правах рукописи

Бирюков Александр Викторович

ГЕНЦЕНОВСКОЕ ИСЧИСЛЕНИЕ ЕСТЕСТВЕННЫХ ВЫВОДОВ

КАК СРЕДСТВО ЭКСПЛИКАЦИИ ФОРМ ИНТУИТИВНЫХ УМОЗАКЛЮЧЕНИЙ В ТРУДАХ АНТИЧНЫХ МАТЕМАТИКОВ.

Специальность 09.00.07 - Логика

Диссертация на соискание ученой степени кандидата философских наук

Научный руководитель:

доктор философских наук, профессор

Слинин Я. А.

ЬиЬоьй ^ (к

Санкт-Петербург 1999

Оглавление

Введение......................................................................1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Заключение....................................................................208

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

Введение.

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

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

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

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

¿с ^

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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