Игошин Математическая логика и теория алгоритмов (1019110), страница 61

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 61)

Программа формализации была выдвинута Д. Гильбертом с целью доказательства непротиворечивости математики точными математическими методами. Она предусматривала уточнение понятия локазательства, чтобы эти доказательства могли стать объектами точной математической теории — теории доказательств.

Чтобы сделать 247 такое возможным, доказательствам придается единая, точная и вполне определенная форма в рамках формальной аксиоматической теории, или формальной системы. Процесс формализации доказательства состоит в том, что утверждения теории заменяются конечными последовательностями определенных знаков, а логические способы заключения — формальными правилами образования новых формально представленных высказываний из уже доказанных. В 5 28 — 30 рассмотрены вопросы, связанные с формальными аксиоматическими теориями, или формальными системами. Этот раздел будет центральным для понимания роли математической логики в математических теориях.

Фундаментальная теорема Геделя о существовании модели у всякого синтаксически непротиворечивого множества формул узкого исчисления предикатов, доказываемая во втором параграфе, устанавливает исключительно важную взаимосвязь между свойствами формальной выводимости и содержательной истинности: непротиворечивый формальный вывод не может противоречить содержанию неформальной теории. Следствия из этой теоремы (теоремы полноты, компактности, Левенгейма— Сколема) углубляют понимание взаимосвязей между формальным и содержательным. В 5 30 с разной степенью подробности рассматриваются подходы к формализации тех математических теорий, которые лежат в основаниях школьного курса математики — теории равенств, теории множеств, числовых сметем, математического анализа„геометрии.

Неотъемлемой частью данной главы мог бы стать и 5 37, содержащий доказательство теоремы Геделя о неполноте формальной арифметики. Но он помещен в гл. Ч11 после изучения вопросов, связанных створней алгоритмов, поскольку методы этой теории существенно используются в ходе доказательства. Многие математики, а также представители других наук высказывают серьезные сомнения в том, стоит ли формализовать (даже если это в принципе и возможно) математические (и иные) теории, считая, что плоды формализации не оправдывают усилий, ценой которых она достигается. С помощью материала настоящей главы хотелось бы показать такие подходы к математическим теориям, истоки которых находятся в школьном курсе математики„которые осуществляет современная математическая наука с помощью математической логики. В настоящее время только формализованный подход к математическим теориям позволяет так формулировать многие важные проблемы о них, что попытки решения этих проблем можно рассматривать всерьез.

5 28. О формальных аксиоматических теориях Аксиоматический метод, рассмотренный в гл. Ч, является как бы формой организации математической науки, способом исследования тех или иных математических объектов. Неформальные 248 аксиоматические теории наполнены теоретико-множественным содержанием, понятие выводимости в них довольно расплывчато и в значительной мере опирается на здравый смысл. Дальнейший шаг на пути изучения аксиоматических теорий состоит в отходе этих теорий от содержательности, в строгой формализации понятия правила вывода и в превращении самих теорий в объекты математического исследования.

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

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

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

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

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

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

Появились работы Дедекинда и Кантора, которые сводили всю математику к теории множеств, работы Буля, Пеано, Пирса, Шредера, которые вводили начало математической символики для законов мышления, работа Фреге, пытавшегося свести всю математику к логике. Эти работы внушили безграничную веру в мощь формализации. Высокой степени точности формализация математического языка в рамках современных логических исчислений достигла в работах первоклассных математиков ХХ в. Рассела, Уайтхеда, Гильберта, Барнайса, Геделя, Черча, А.А.Маркова, А.

И. Мальцева и др. Поэтому сегодня уже можно говорить о математическом языке как о части математики, о языке как об одном из предметов, исследуемых математикой, и спорить о реализуемости мечты Лейбница. Мощное развитие логики и логического языка привело к созданию новой области математики — оснований математики, предметом изучения которой стало строение математических утверждений и математических теорий и которая поставила своей целью ответить на вопросы типа: «Как должна быть построена теория, чтобы в ней не возникло противоречий?», «Какими качествами должны обладать методы доказательства, чтобы считаться достаточно строгими?» и т.д. Одной из фундаментальных идей, на которые опираются исследования по основаниям мате- 250 матики, является идея формализации математических теорий, т.е.

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

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

Конечные последовательности символов алфавита теории Т называются словами или выражениями теории Т; 2) имеется подмножество выражений теории Т, называемых формулами теории Т (обычно имеется эффективная процедура, позволяющая по данному выражению определить, является ли оно формулой); 3) выделено некоторое множество формул, называемых аксиомами теории Т(обычно имеется эффективная процедура, позволяющая по данной формуле определить, является ли она аксиомой); 4) имеется конечное множество А„..., А„отношений между формулами, называемых правилами вывода. При этом для каждого А, (1 <! < и) существует целое положительное ) такое, что для каждого множества, состоящего изб формул, и для каждой формулы Рэффективно решается вопрос о том, находятся ли данные 1 формул в отношении А; с формулой Г, и если да, то Гназывается непосредственным следствием данных 1формул по правилу А, Построенное в 5 15 формализованное исчисление высказываний может служить примером формальной аксиоматической теории.

Характеристики

Список файлов книги