Разрешимость теорий иерархий согласованных со сложением функций

• Автор: Снятков, Алексей Сергеевич
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 2012
• Место защиты: Тверь
• Количество страниц: 84 с.

Оглавление
Введение

Актуальность

Обзор литературы

Цели работы

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

Положения, выносимые на защиту, и научная новизна

Апробация
Публикации

Структура работы

1 Определения

1.1 Согласованные со сложением функции
1.2 Разрешимые теории и сложность разрешающих процедур
2 Свойства иерархий функций
2.1 Поведение функций /*
2.2 Термы tji
3 Теория Т
3.1 Элиминация кванторов в теории Т
3.2 Разрешимость теории Т
3.3 Периодичность /1
4 Время работы алгоритма
4.1 Верхняя оценка времени алгоритма
4.2 Нижняя оценка времени задачи

Заключение Список литературы
Введение
Актуальность
Исследование разрешимости арифметических теорий — одна из центральных задач математической логики. Этим вопросом стали заниматься примерно с середины двадцатых годов 20 века. В начале и середине тридцатых годов были получены знаменитые теоремы Гёделя о неполноте и результат Чёрча о неразрешимости. Эти результаты открыли перспективу изучения разрешимости и индуцировали массу иследований о разрешимости и неразрешимости различных математических теорий.
Основными методами доказательства разрешимости являются:
1. Эффективная элиминация кванторов —- это алгоритмический процесс, порождающий по заданной логической формуле другую, эквивалентную ей формулу, свободную от вхождений кванторов. Элиминация кванторов далеко не всегда возможна, но когда это так, алгоритм элиминации кванторов приносит исключительную пользу для исследователя, так как вскрывает структуру теории и её моделей. При использовании метода элиминация кванторов часто требуется расширение сигнатуры, что показывает выразительную силу таких теорий.
Самыми известными теориями, разрешимость которых была доказана при помощи элиминации кванторов, являются аддитивная арифметика целых чисел (арифметика Пресбургера) и теория вещественно замкнутых полей (действительных чисел со сложением и умножением).
Также известны следующие теории, разрешимость которых установлена методом элиминации кванторов: теория рациональных чисел с порядком, теория алгебраически замкнутых полей, теория булевых алгебр.

Если в каком-то в? содержится член 2о(жг, д“, о"'
120(Ж»; Од *?,2) 1 ’ ' ' ' ’ ]2' : 0 ! > ’ 1 ' > 2'
5(ж4, До, Д;
и, согласно сделанному в начале доказательства замечанию (2), х% не превосходит некоторую константу. Если же ни в каком бу не содержится член 2о(ж», Др', д"'
(a) 13о{х%, До - £?,, й1, > %) > ао ~ 5, аД * > аД)- Получаем:
1о(х)с, др — 1 1) , ал) 13о{хг, До — 55,, 01
< 5, (ж,, а0, ар , дД < сЯ'Дж*,, аД аД
< ипо(хк, До + ,дД
(b) Д0(ж„ До - 55,, аь
20(, Оо 55,, , Од) До 31? " Д/1) <''
< ЗД(ж*,До,аД...1а'1) 5;(жг)а0,аь
< До(жг, Ду ~Ь (Д;,, Д1, . , дг).
Оба случая рассматриваются аналогично, рассмотрим случай (а). Имеем:
ло(%к, До — 5,5' ’ 1> ‘ ‘ ‘ ) Дл) До(Дг> До > Д1, 1 Д)
< йло(жй, Ду 4- 6, аД
то есть
/о%Ахк, До - аД , дД)) < /о_1(о(жг, до - 55,, Д1, , аД) <
< /о_1(1о(, До + 5, аД , аД)). Далее, применяя лемму 5, получаем:
Д1, а2) ) Дд) + До — 5'х Д 1 (Дг, д 15 Д2, ДД + До ~ 5, <
< 1оо(хк, а'0 + 5 а',)) + с).