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

• Автор: Бирюков, Александр Викторович
• Шифр специальности: 09.00.07
• Научная степень: Кандидатская
• Год защиты: 1999
• Место защиты: Санкт-Петербург
• Количество страниц: 215 с.

Оглавление
Введение
Г лава 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. Экспликация евклидова доказательства предложения
4.4. Экспликация евклидова доказательства предложения
4.5. Экспликация евклидова доказательства предложения
4.6. Экспликация евклидова доказательства предложения
4.7. Экспликация евклидова доказательства предложения
4.8. Экспликация евклидова доказательства предложения
4.9. Экспликация евклидова доказательства предложения
4.10. Экспликация евклидова доказательства предложения
4.11. Экспликация евклидова доказательства предложения
4.12. Экспликация евклидова доказательства предложения
4.13. Экспликация евклидова доказательства предложения
4.14. Экспликация евклидова доказательства предложения
4.15. Экспликация евклидова доказательства предложения

искомое положение дел,
описываемое формулой Р.
Данный чисто интуитивный ход евклидова рассуждения можно обосновать в качестве производного правила вывода в исчислении естественных выводов, употребляя для этого обоснования основные правила исчисления. Данное производное правило вывода в ИЕВ делает оправданным логический переход от секвенций вида Д1,Д2
Обоснование этого правила как производного правила исчисления естественных выводов.
[1] Д1,Д2
=>((#, &Д2&...&Д„)->Р).
Прлр
Ді,Ді,-,Д„ =>Р =>((Д1&Д2&...&Д1|)->Р)
[2] (Д, &Д2 & ...& Д,)=»(Д, & Д2 &-& Д„) [ТИС]

[3] Н => Дп [2,Пр&(б)
[4] Др Д2
[5] Н,Дх,Дг
[6] Н => Ди_, [2, Пр.пр. 1]
[7] Я,Д,,Д2„..,Д„_2 =>(Д„_, н>Р) [5,Яр;]
[8] Я,Я,Д„Д2
[те] Я,Я
[те + /] Я => Р [те + (/ -1), ТІр.стр.2]
[те + / +1] ((Д1&Д2&...&Д„)Р) [те + /,Яр;]