Оглавление
Введение 4
Актуальность.................................................... 4
Обзор) литературы............................................... 6
Цели работы..................................................... 9
Методы исследования............................................. 9
Положения, выносимые на защиту, и научная новизна............... 9
Апробация ..................................................... 10
Публикации..................................................... 11
Структура работы............................................... 11
1 Определения 13
1.1 Согласованные со сложением функции ....................... 13
1.2 Разрешимые теории и сложность разрешающих процедур . . 15
2 Свойства иерархий функций 18
2.1 Поведение функций /*...................................... 18
2.2 Термы .................................................... 22
3 Теория Т/ 26
3.1 Элиминация кванторов в теории 7/.......................... 26
3.2 Разрешимость теории Т/.................................... 40
3.3 Периодичность /\.......................................... 41
4 Время работы алгоритма 45
4.1 Верхняя оценка времени алгоритма.......................... 45
4.2 Нижняя оценка времени задачи ............................. 70
2
Заключение Список литературы
Введение
Актуальность
Исследование разрешимости арифметических теорий — одна из центральных задач математической логики. Этим вопросом стали заниматься примерно с середины двадцатых годов 20 века. В начале и середине тридцатых годов были получены знаменитые теоремы Гёделя о неполноте и результат Чёрча о неразрешимости. Эти результаты открыли перспективу изучения разрешимости и индуцировали массу иследований о разрешимости и неразрешимости различных математических теорий.
Основными методами доказательства разрешимости являются:
1. Эффективная элиминация кванторов — это алгоритмический процесс, порождающий по заданной логической формуле другую, эквивалентную ей формулу, свободную от вхождений кванторов. Элиминация кванторов далеко не всегда возможна, но когда это так, алгоритм элиминации кванторов приносит исключительную пользу для исследователя, так как вскрывает структуру теории и её моделей. При использовании метода элиминация кванторов часто требуется расширение сигнатуры, что показывает выразительную силу таких теорий.
Самыми известными теориями, разрешимость которых была доказана при помощи элиминации кванторов, являются аддитивная арифметика целых чисел (арифметика Пресбургера) и теория вещественно замкнутых полей (действительных чисел со сложением и умножением).
Также известны следующие теории, разрешимость которых установлена методом элиминации кванторов: теория рациональных чисел с порядком, теория алгебраически замкнутых полей, теория булевых алгебр.
4
2. Метод интерпретаций: если известно, что теория Т\ разрешима, а все отношения в теории То интерпретируются в теории Т\, то теория То также разрешима.
Например, Тарским было показано, что геометрия разрешима, так как интерпретируется в действительные числа.
3. Метод использования свойств формальных языков: Теория является разрешимой, если все отношения в этой теории могут быть закодированными с помощью какого-нибудь алфавита, и получившийся класс языков обладает свойством разрешимости, а также свойствами замкнутости, относительно операций пересечения, дополнения и некоторых других.
Одно из направлений исследований — поиск разрешимых обогащений арифметики Пресбургера. Один из наиболее значительных результатов был получен А.Л.Семеновым. Он ввёл понятие функций, согласованных со сложением, и рассматривал расширение арифметики Пресбургера такой функцией, а также доказал, что такая теория является разрешимой. Кроме того, А.Л.Семёновым было введено понятие класса редких предикатов и доказано, что теория, полученная расширением арифметики Пресбургера такими предикатами, является разрешимой. Также было доказано, что теория, полученная расширением арифметики Пресбургера порядком и умножением на одно произвольное число, разрешима. Теория, полученная расширением арифметики Пресбургера поразрядными операциями, также разрешима.
Примерно с шестидесятых годов 20 века начались исследования вычислительной сложности разрешимых проблем. На сложность разрешения теории можно смотреть как на меру её выразительных возможностей. В настоящее время вопрос об эффективности алгоритмов также приобретает всё большее практическое значение в связи с расширением применения вычислительной техники. Для решения задач с помощью вычислительной техники необходимо, чтобы они были алгоритмически разрешимыми и допускали разрешение с использованием ограниченного числоа ресурсов, поэтому важной теоретической и практической проблемой является установление
вычислительной сложности логических задач, разрешимость которых известна.
Работы Фишера, Мейера и Рабина показывают, что многие теории, хотя они и являются разрешимыми, с практитечкой точки зрения таковыми не являются, потому что любой разрешающий алгоритм требовал бы практически невозможного числа вычислительных шагов. Так для арифметики сложения натуральных чисел, разрешимость которой доказана Пресбур-гером, было показано, что для каждого разрешающего алгоритма ЛЬ существует предложение А размера п такое, что для ЛЬ требуется 2Т‘ вычислительных шагов для ответа на вопрос по поводу А. Также этими же авторами показано, что разрешающая процедура для теории вещественно замкнутых полей обладает сложностью по меньшей мере 2п. Было показано, что для арифметики Пресбургера существует разрешающий алгоритм, который работает 2“ шагов. Из других известных результатов отметим, что для доказательства разрешимости слабой мопадической теории следования второго порядка, требуется не меньше гинерэкспоиенты шагов.
Обзор литературы
В работах ряда авторов найдены неразрешимые проблемы и созданы общие методы доказательства неразрешимости теорий. Многие методы доказательства неразрешимости теорий изложены в известной монографии Тарского, Робинсона и Мостовского [45]. Первые неразрешимые теории были найдены Черчем (см. [29], |30|, (2|), который доказал неразрешимость узкого исчисления предикатов, и Россером (см. [42]), который доказал неразрешимость арифметики натуральных чисел. После доказательства неразрешимости формальной арифметики появилось множество результатов, касающихся разрешимости различных математических теорий.
Разрешимость многих теорий была доказана с помощью метода элиминации кванторов. В 1929 году М.Пресбургер показал, что арифметика натуральных чисел с одним сложением разрешима (см. [2], [37]). Ряд классических результатов о разрешимости получены Тарским: теория вещественно замкнутых полей разрешима (см. [4], [44]), евклидова геометрия
б
- Київ+380960830922