Разрешимость теорий иерархий согласованных со сложением функций тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

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

Снятков Алексей Сергеевич

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

Специальность 01.01.06 — математическая логика, алгебра

и теория чисел

Автореферат диссертации на соискание учёной степени кандидата физико-математических наук

2 5 ОКТ 2012

Ярославль — 2012

005054004

Работа выполнена в Федеральном государственном бюджетном образовательном учреждении высшего профессионального образования «Тверской государственный университет».

Научный руководитель — доктор физико-математических наук,

доцент Дудаков Сергей Михайлович

Официальные оппоненты : Соколов Валерий Анатольевич, доктор

физико-математических наук, профессор, заведующий кафедрой теоретической информатики Ярославского государственного университета им. П. Г. Демидова

Чагров Александр Васильевич, доктор физико-математических наук, профессор кафедры функционального анализа и геометрии Тверского государственного университета

Ведущая организация — Московский государственный университет

им. М. В. Ломоносова Защита состоится 23 ноября 2012 г. в 1400 часов на заседании диссертационного совета Д 212.002.03 при Ярославском государственном университете им. П. Г. Демидова но адресу: Российская Федерация, 150008, Ярославль, ул. Союзная, 144, ауд. 426.

С диссертацией можно ознакомиться в библиотеке Ярославского государственного университета им. П. Г. Демидова.

Автореферат разослан « октября 2012 г.

Ученый секретарь диссертационного совета

Яблокова

Светлана Ивановна

Общая характеристика работы

Актуальность работы. Исследование разрешимости арифметических теорий — одна из центральных задач математической логики. Этим вопросом стали заниматься примерно с середины двадцатых годов 20 века. В начале н середине тридцатых годов были получены знаменитые теоремы Гсдсля о неполноте и результат Чёрча о неразрешимости. Эти результаты открыли перспективу изучения разрешимости и индуцировали массу иследований о разрешимости и неразрешимости различных математических теорий.

Одно из направлений исследований — поиск разрешимых обогащений арифметики Пресбургсра. Один из наиболее значительных результатов был получен Л.Л.Семеновым. Он рассматривал расширение арифметики Пресбургсра редкими предикатами1 и функциями, согласованных со сложением2, которые были введены также им. A.JI. Семёнов доказал, что оба варианта обогащения являются разрешимыми. Дудаковым С.М.3 было рассмотрено одновременное обогащение арифметики Пресбургсра одноместным функциональным и одноместным предикатным символами, и показано, что такая теория допускает элиминацию кванторов. Из других результатов, связанных с функцией экспонеты, можно выделить следующий: если гипотеза Шануэля для действительных чисел верна, то теория поля действительных чисел с экспонентой является разрешимой4.

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

1 Семёнов А.Л. О некоторых расширениях арифметики сложения натуральных чисел. > ' Изв. ЛН

СССР, 43(5), 1979. С.1173-1195.

2Семспоп Л.Л. Логические теории одпоМ(чтпых функций па натуральном ряде. [ I т. ЛН СССР,

■17(3), 1!Ш. С.«23-()5Х.

'Дудаков С.М. Трансляционная теорема п автоматные структуры Вестник ТвГУ сер. Прикл.

матем.. -1(211, 2006. С. 5-35.

4Macintyre A.J., Wilkie A.J. On the decidability of the real exponential field, Kreisel 70th Birthday

Volume, 20П5

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

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

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

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

'^Fischer, М. J-, and Rabin М.О., Super-Exponential Complexity of Presburger Arithmetic. / Proceedings of the SIAM-AMS Symposium in Applied Mathematics Vol. 7, 1974, 27-11

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

Цели работы. Данная работа посвящена исследованию свойств теорий вида:

Tf = Th(w, 0,1,<,+, /о, /!,...,/„),

образованных нз арифметики А.Л.Семенова Th(uj.+.f0) добавлением функций /¿, г > 0, которые в работе названы «гиперфункциями». Каждая из них получается итерацией предыдущей. В частности, показано, что такие теории при определённых условиях являются разрешимыми. Также в работе изучается сложность разрешающей процедуры для таких теорий.

Основные положения, выноснмые на защиту, и научная новизна. Все полученные результаты являются новыми. На защиту выносятся следующие основные результаты:

1. Доказано, что если все функции являются периодичными но любому натуральному модулю, то любая формула в теориях Tf эквивалентна экзистенциальной. Следовательно, эти теории являются модсльно полными. Показано, что преобразование каждой формулы к экзистенциальной может быть эффективным, если все гиперфункции являются эффективно периодичными по любому натуральному модулю. Установлено, что если обогатить теорию обратными для /j функциями, то получается теория с элиминацией кванторов. Элиминация будет эффективной при упомянутом выше условии. Таким образом, при выполнении условия эффективной периодичности гиперфункций, теории являются разрешимыми.

6Derek С. Oppen: А 22* Upper Bound on the Complexity of Presburger Arithmetic. J. Compvit. Syst.

Sei. 16(3): 323-332, 197S

2. Установлено, что если функция /о — периодичная по любому модулю р > 1 с периодом меньше р, то гиперфункция ОТ /о является эффективно периодичной по любому модулю р > 1с периодом 1. Также установлено, что если функция /о — периодичная по любому модулю р > 1с периодом меньше р, а функция fi{x) — периодичная функция, то гиперфункция от функции f(x) + f\(x) является периодичной по модулю р для любого р > 1. Следовательно, теории, для которых выполняется одно из двух условий, являются разрешимыми.

3. Показано, что представленный в работе разрешающий алгоритм для любой формулы длины п для определения сё истинности В ту требует памяти не больше чем • Следовательно, разрешающий алгоритм

0{тг) раз

работает не более ^^ шагов.

0(п) раз

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

работы алгоритма, определяющего истиность формулы в X/, будет не 2

меньше чем ^^ • Таким образом, задача разрешения указанных тео-

0(п) раз

рий является полной в классе сложности TIME I

^О(п) раз/

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

Апробация работы. Начиная с 2006 года содержание глав дайной диссертации неоднократно докладывалось па семинаре «Теоретические основы информатики» в ТвГУ.

Доклад по теме диссертации был сделан в 2008 году в Санкт-Петербургском отделении Математического института им.В.А.Стсклова РАН на семинаре по математической логике под руководством академика РАН Ю.В.Матиясевича.

•(C)-

„„-У

Также доклад по теме диссертации был сделан в 2011 году на международной конференции «Актуальные проблемы прикладной математики, информатики и механики» (Воронеж).

Исследования по теме работы были поддержаны РФФИ, проект № 08-01-002 11-а.

Публикации. Список публикаций по теме диссертации включает 5 работ. Работы [1], [2], [3] опубликованы в изданиях, входящих в список рекомендованных ВАК ведущих рецензируемых изданий.

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

Объем и структура работы. Диссертация состоит из титульного листа, оглавления, четырёх глав основной части, заключения и списка литературы. Общим объем диссертации составляет 83 страницы. Библиография включает 46 наименований.

Содержание работы

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

В первой главе даются основные определения, которые используются в диссертации. В параграфе 1.1 приводятся определения согласованной со сложением функции и иерархии таких функций(см. ссылку1). Функция / является эффективно периодичной, если для любого натурального р функция / периодична по модулю р с периодом, который определяется эффективно но р. Если для функции / выполняются следующие условия:

(1) / периодична по модулю п для всех п € п > 2;

(2) для всякой неограниченной конечной суммы

i

существует такое 5 G и, что либо S(x + 5) > f(x) для всех х G ш, либо S(x + S) < —f(x) для всех х € ш;

(3) / монотонно возрастает,

то она называется согласованной со сложением. Если константы в пунктах (1) и (2) находятся эффективно, то / называется эффективно согласованной со сложением.

Последовательности функций /¿, где i € и называется иерархией функций fi, если fi является гиперфункцией от fi-1, то есть определяется так, что fi+i(x + 1) = fi(fi+i{x)).

В параграфе 1.2 приводятся основные определения, связанные с вычислительной сложностью. В работе рассматривается класс сложности TIME i ) • В этот класс входят задачи, для которых найдется

^О(п) paj

алгоритм, решающий задачу за время не больше ^^ шагов, где п —

0(п) ра^

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

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

В параграфе 2.2 определяются термы, которые будут в дальнейшем использоваться:

tji(v, сц, oi+i,..., а,-) = fi(fi+1(.. - (fj-i(fj(v + а,-) + a,-_i)...) + oi+1) + а,),

где г < j, все — константы. Затем доказываются для них ряд важных в дальнейшем свойств (леммы 7-10).

В третьей главе исследуются свойства теории 7/. В параграфе

з.1 доказывается следующая основная теорема:

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

0 + х 4-----Н х ¿¡о{.V, о0, оь .... о,-) + с„V)

V

где все аьЬг,с, 0 — константы, V — переменные из формулы.

Для доказательства теоремы демонстрируется, что формула вида ->(3x1,. • • ,х{)ф

■эквивалентна экзистенциальной, если ф — бескванторная формула, причем при этом преобразовании, матрица формулы не теряет нужного нам вида. Для этого модифицируется метод А.Л. Семёнова. Отмечается, что (^¿^¡^(и, ао, 01,..., а;)) + а) эквивалентна булевой комбинации формул вида Як{и + Ь) для некоторых к II Ь и некоторых линейных неравенств для

и. В лемме 11 доказывается, почему можно ограничиться рассмотрением термов вида Ь<,-ц(г1, Оо, 01.....О;) и су. Далее каждое неравенство из ф

приводится к виду

П < «к < Мк,

где суммы 5к содержат только слагаемые с неременными х,-, а суммы г^ и таких слагаемых не содержат. Далее термы по каждой переменной группируются в суммы, вида

5(х) = ^ ач/(х + РЧ). я

Среди всех таких сумм выбирается а — максимальная по величине. Пусть — остаток суммы Би (без а). Возможны две ситуации:

1. а по модулю превосходит каждое в'к не менее чем в два раза,

2. а по модулю меньше для некоторого к.

Используя леммы 1-10, показывается, что в первом случае количество элиминируемых кванторов можно уменьшить, добавляя новые кванторы существования перед отрицанием, а во втором — сократить их количество, используя вместо кванторов дизъюнкцию.

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

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

Следствие 1. Если функция /о согласована со сложением и все функции /г периодичны по .модулю р для любого р > 1, то теория Т/ является моделъно полной.

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

Теорема 2. Пусть /о — согласованная со сложением функция и все функции /,• периодичны по модулю р для любого натурального р. Тогда если теорию Ту обогатить предикатами де.аимости и обратными функциями для /о, /ь /2, • • •, 1п, то в "ей любая формула эквивалентна бескванторной формуле.

Для доказательства демонстрируется, что экзистенциальная формула вида

(Зхь .. .,хп)ф 10

эквивалентна бескванторной. Это доказательство почти в точности повторяет доказательство теоремы 1, но вместо новых кванторов мы применяем обратные функции для получения требуемых значений.

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

В параграфе 3.3 устанавливаются некоторые достаточные условия для /о, при которых функции fi будут эффективно периодичными по любому натуральному модулю.

Теорема 3. Пусть для любого р > 1 функция f(x) периодична по модулю р с периодом меньше р. Тогда гиперфункция F(x) от функции f{x) является эффективно периодичной по модулю р > 1с периодом 1 для любого р.

Доказательство проводится индукцией по модулю р, используя методы теории чисел.

Теорема 4. Пусть f — функция, согласованная со сложением, и для любого р > 1 функция J(x) периодична по модулю р с периодом меньше р. Пусть fi(x) периодичъшя функция. Тогда гиперфункция F(x) от функции f(x) + fi(x) является периодичной по модулю р для любого р > 1.

Для доказательства показывается, что существует последовательность г/о, <7i,.... qk такая, что qk < qk~i < • ■ • < 9о- и f(x) периодична по модулю qo с периодом gi, по модулю q\ — с периодом дг, • • ■, по модулю 1 — с периодом qk, 110 модулю qk с периодом 1, где qo — период fi(x). Далее показывается, что если доказать периодичность F(x) по модулям <7о. ■••, 9ь то будет доказана периодичность F(x) по модулю р, начиная с некоторого х. И, наконец, доказывается периодичность F(x) 110 модулям 91, • • •, 9кВ четвёртой главе исследуется вычислительная сложность задачи разрешения теории Tj. В параграфе 4.1 оценивается время работы алгоритма из параграфа 3.2. Доказывается ряд лемм( 12-27), при помощи

которых оцениваются константы, используемые в разрешающем алгоритме из параграфа 3.2. В лемме 28 устанавливается, что формула длины п после одной итерации алгоритма из теоремы 1 в первом случае будет иметь длину не больше п20 для достаточно больших п. Далее в лемме 29 устанавливается, что формула длины п после одной итерации алгоритма из теоремы 1 во втором случае будет иметь длину не больше п° для достаточно больших п. Затем доказывается, что время работы разрешающего алгоритма для любой формулы из теории Ту не больше, чем > ссли

0(п) рал

исходная формула была длиной п:

Теорема 5. Пусть ф это формула ->(Э:Г1... хд)ф'. Пусть длина ф равна п. Тогда после одной итерации алгоритма из теоремы 1 длина ф для достаточно больших п не превосходит где М — некоторая кон-

М раз

станта.

Доказательство этой теоремы сводится к рассмотрению всех случаев из теоремы 1 и оценки длины формулы на каждом этапе, используя леммы 12-29.

Из этой теоремы получается следующее следствие.

Следствие 2. Если формулу ф длины п привести к экзистенциальному виду по алгоритму, представленному в теореме 1, то её длина для

2...2п

достаточно больших п не будет превосходить •

0(п) раз

Из теоремы 2 и следствия 2 получаем следующие результаты:

1. Если формулу ф длины п привести к бескванторной по алгоритму из теоремы 2, то её длина для достаточно больших п не будет превосходить ■

О(п) раз

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

О(п) раз

3. Задача разрешения теории 'Г/ принадлежит классу ТТМЕ ( ,2^

0(п) раз

В параграфе 4.2 Доказано, что для любого разрешающего алгоритма существует формула длины п из теории Tj, для которой вре-

2 Г мя работы алгоритма будет не меньше чем . Фишером и Рабином5

0(п) ри

был продемонстрирован следующий метод для установления нижней границы времени для разрешения теорий со сложением. Пусть для функции д, которая растёт не медленнее экспоненты, в теории со сложением Т существует константа с > 0 такая, что для любого числа п 6 N и для любого двоичного слова w длины п существуют формулы I„(b), Jn(b), S(a,i), Hw(x) длины, не превосходящей сп. 1п{Ь) означает, что b < у(п)2, Jn(b) означает, что Ъ = д(п), S(a,i) означает, что в а на гом месте стоит 1, Hw{x) означает, что первые д{п) элементов последовательности х имеют вид ti/'Os'"'-". Тогда для любого алгоритма, разрешающего Т, время его работы занимает больше, чем g(qn) шагов, где q — некоторая константа. Фактически доказано, что задача разрешения теории Т

является трудной в классе TIME(g(0(n))).

2

Пусть д(п) — это функция Доказывается следующая теорема:

п раз

Теорема 6. Пусть в произвольной теории со сложением Т существует формула логики первого порядка, которая любую пару натуральных чисел (w, v) взаимно однозначно кодирует натуральным числом. Тогда для теории Т существует константа с > 0 такая, что для каждого п существует формула фп(а,у,х), которая кодирует любую последовательность натуральных чисел ац,.. . а9(п+1)_1; то есть для любой такой последовательности существует а и для любого

2/ = 0,1,..., g(n + 1) — 1 :

Фп{а,У,х) у < д(п + 1) Л х = ау.

Также длина 1рп(а,у,х) не превосходит сп.

Формула фп(а,у,х) строится по индукции. Для п = 0, она получается из условия теоремы. Чтобы построить ф„+1 (а.у.х), сначала через

фп(а, у, х) определяются упомянутые выше формулы Sn(x, у), J „(у), 1п(у). Формула Hw(x) строится, используя формулу Sn{x,y).

Пусть s{x,y) — это код пары (х.у). Представим последовательность произвольных чисел Хо, ■ ■ ■ Хд(к+2)-\ в виде полного бинарного дерева Dh{xQ, xi...., x2h-i), где h = д(к + 1) — высота дерева, Xq.Xi, ... .X2h-\ — элементы в листьях дерева, а любая внутренняя вершина содержит код пары своих сыновей:

ф^о,:^), 5(2:2-ж3)) S(X0,X!) s(x 2,Х3)

xq XI Х2 х3 ...

Кодом дерева (и всей последовательности) будет число, стоящее в корне. Чтобы закодировать путь от корня к листу с номером у, нам достаточно для каждого j знать, к какому сыну: левому или правому — следует идти от вершины па глубине j. Следовательно, весь путь можно закодировать последовательностью нулей и единиц длины h. Используя у, х), можно эту последовательность закодировать, благодаря чему, имеем возможность построить ipn+i(a,y,x). Благодаря тождественным преобразованиям и свойствам фп(а. у, х), длина ijjn+i(a, у. х) возрастает не более чем на некоторую константу.

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

Теорема 7. Если в теории системы ТЬ(ол 0,1, <, +. /) выполняется условие f(x + 1) > f(x) для любого х, то в ней существует формула, которая взаимно однозначно кодирует два натуральных числа.

При выполнении условия из теоремы, получается:

f(x + у + 2) > f(x + у + 1) + f{x).

Пара чисел (х, у) кодируются следующим образом:

а = /(х) + f(x + у + 1).

Далее, показывется, что по а можно однозначно востановить х и у. Поэтому формула, которая взаимно однозначно кодирует два натуральных числа, будет выгледить так:

ф(а,у,х) (у = О Л (3u)(a = /(х) + f(x + it + 1)))V

V (у = 1 A (3u){a = f{u) + f(x + u+ 1))).

Как следствие получаем:

1. Если в теории системы Th(w, 0.1, <,+,/о,/i,.../т) выполняется условие /0(х + 1) > 1+^f0{x) для любого х, то задача разрешения для неё будет полной в классе TIME ( ) •

О(п) раз

2. Задачи разрешения для теорий Th(u>. 0,1, <, +, 2х) и Th(w,0,1. < , +, х!) будут полными в классе Т1Ме( Q^s ) •

Ю(п) раз'

В заключении ещё раз перечисляются полученные результаты и формулируются открытые вопросы, которые могут служить направлением дальнейших исследований. Также в заключении выражается благодарность участникам семинара по математической логике ПОМИ РАН и лично академику Ю.В.Матиясевичу, участникам семинара «Теоретические основы информатики* в ТвГУ за ценные советы и замечания.

Публикации в рецензируемых научных журналах

[1] Снятков A.C. Разрешимость теории Tj = ТЬ(ол 0.1, < , +, /(х), F(x)). / Вестник ТвГУ сер. Прикл. матем., 14(34), 2008. С. 67-77

[2] Снятков A.C. Разрешимость теории Tf = Th(w, 0,1,< ,+,/(х),...,/п). Модел. и анализ информ. систем., 17:3, 2010, С. 72-90

[3] Снятков A.C. Нижняя граница времени для разрешения теории с функцией экспоненты ' Вестник ТвГУ, сер. Прикл. матем., 17. Выпуск 2 (25), 2012. С. 5-10.

Другие публикации

[4] Снятков A.C. Разрешимость теории Тс = Th(cj, 0,1, <. сг, £х).

Вестник ТвГУ сер. Прикл. матем., 5(35), 2007. С. 113-121

[5] Снятков A.C. Разрешимость теории Tf = Th(a), 0. 1, <

, +, f(x),..., /„). / Актуальные проблемы прикладной математики, информатики и механики. Сборник трудов международной конференции, 2011, С. 362-365.

Технический редактор A.B. Жильцов Подписано в печать 15.10.2012. Формат 60x84 Vie-Усл. печ. л. 1,0. Тираж 100 экз. Заказ №510 Тверской государственный университет Редакционно-издательское управление Адрес: 170100, г. Тверь, ул. Желябова, 33. Тел. РИУ: (4822) 35-60-63

Введение

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

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

Цели работы.

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

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

Апробация

Публикации.

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

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

1.1 Согласованные со сложением функции

1.2 Разрешимые теории и сложность разрешающих процедур

2 Свойства иерархий функций

2.1 Поведение функций

2.2 Термы ^

3 Теория 7>

3.1 Элиминация кванторов в теории 7/.

3.2 Разрешимость теории Т/.

3.3 Периодичность /1.

4 Время работы алгоритма

4.1 Верхняя оценка времени алгоритма.

4.2 Нижняя оценка времени задачи

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

Исследование разрешимости арифметических теорий — одна из центральных задач математической логики. Этим вопросом стали заниматься примерно с середины двадцатых годов 20 века. В начале и середине тридцатых годов были получены знаменитые теоремы Гёделя о неполноте и результат Чёрча о неразрешимости. Эти результаты открыли перспективу изучения разрешимости и индуцировали массу иследований о разрешимости и неразрешимости различных математических теорий.

Основными методами доказательства разрешимости являются:

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

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

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

2. Метод интерпретаций: если известно, что теория Т\ разрешима, а все отношения в теории интерпретируются в теории Т\, то теория То также разрешима.

Например, Тарским было показано, что геометрия разрешима, так как интерпретируется в действительные числа.

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

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

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

Работы Фишера, Мейера и Рабина показывают, что многие теории, хотя они и являются разрешимыми, с практитечкой точки зрения таковыми не являются, потому что любой разрешающий алгоритм требовал бы практически невозможного числа вычислительных шагов. Так для арифметики сложения натуральных чисел, разрешимость которой доказана Пресбур-гером, было показано, что для каждого разрешающего алгоритма АЬ существует предложение А размера п такое, что для АЬ требуется 22" вычислительных шагов для ответа на вопрос по поводу А. Также этими же авторами показано, что разрешающая процедура для теории вещественно замкнутых полей обладает сложностью по меньшей мере 2п. Было показано, что для арифметики Пресбургера существует разрешающий алгоритм, который работает 222 шагов. Из других известных результатов отметим, что для доказательства разрешимости слабой монадической теории следования второго порядка, требуется не меньше гиперэкспоненты шагов.

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

В работах ряда авторов найдены неразрешимые проблемы и созданы общие методы доказательства неразрешимости теорий. Многие методы доказательства неразрешимости теорий изложены в известной монографии Тарского, Робинсона и Мостовского [45]. Первые неразрешимые теории были найдены Черчем (см. [29], [30], [2]), который доказал неразрешимость узкого исчисления предикатов, и Россером (см. [42]), который доказал неразрешимость арифметики натуральных чисел. После доказательства неразрешимости формальной арифметики появилось множество результатов, касающихся разрешимости различных математических теорий.

Разрешимость многих теорий была доказана с помощью метода элиминации кванторов. В 1929 году М.Пресбургер показал, что арифметика натуральных чисел с одним сложением разрешима (см. [2], [37]). Ряд классических результатов о разрешимости получены Тарским: теория вещественно замкнутых полей разрешима (см. [4], [44]), евклидова геометрия разрешима (см. [44]), теория булевых алгебр разрешима (см. [43]). Более простое доказательство последнего найдено Ершовым (см. [7], [8]). Аксом и Коченом (см. [23], [24], [25]) было доказано, что теория поля р-адических чисел разрешима. Также Аксом было доказано, что теория класса всех конечных полей разрешима. Эренфойхт в [32] показал, что теория линейно упорядоченных множеств разрешима. Первое полное доказательство этого результата было опубликовано Лёйхли и Леонардом в [36]. Позже этот результат стал простым следствием метода статьи Рабина (см. [41]). В [1] описаны результаты, посвящённые вопросу разрешимости и неразрешимости теорий, принадлежащие отечественным математикам.

В работах [13] и [14] А.Л.Семёновым были рассмотрены расширения арифметики Пресбургера функциями, согласованными со сложением и редкими предикатами. А.Л.Семёнов доказал, что оба варианта обогащения являются разрешимыми. В работе [12] И.В.Поповым было введено понятие периодичных по любому модулю, неубывающих функций, было рассмотрено расширение арифметики Пресбургера такой функцией, и показано, что такая теория является разрешимой. В работе [6] Дудаковым С.М. было рассмотрено одновременное обогащение арифметики Пресбургера одноместными функциональными и еще более редкими одноместными предикатными символами, и показано, что такая теория допускает элиминацию кванторов. В работе [10] Ю. Г. Пеизин доказал, что теория, полученная расширением арифметики Пресбургера порядком и умножением на одно произвольное число, разрешима. В [38] доказано, что если гипотеза Шануэля (см. [35]) для действительных чисел верна, то теория поля действительных чисел с экспонентой является разрешимой.

Одним из способов доказательства разрешимости теорий является метод использования свойств формальных языков. В статье [28] рассматриваются конечные автоматы для доказательства разрешимости теорий, вводится понятие автоматной системы. В [28] также доказано, что если система является автоматной, то по любой формуле этой системы можно эффективно построить конечный автомат, который проверяет её истинность, то есть теория такой системы является разрешимой. Например, системы (и;,+), ш, <), (¿2, <) (см. [3]) являются автоматными. В свою очередь, система (<0>,+) (см. [46]) не является автоматной, хотя ее теория допускает элиминацию кванторов и разрешима. В статье [И] понятие конечного автомата дополнятся рекурсивным оракулом и с помощью такой структуры доказывается разрешимость некоторых теорий автоматных систем, обогащенных одноместным предикатом вида С/ С {2х : х 6 ш}. Также в [11] приводится пример неавтоматной системы, теория которой не допускает элиминацию кванторов в исходной сигнатуре, но которая разрешима.

Значительное число работ посвящено исследованию вычислительной сложности. М. Блюмом в [27] дано формальное понятие аксиоматической меры сложности. При изучении сложности алгоритма нужно остановиться на каком-нибудь определённом уточнении понятия алгоритма. В качестве разрешающих процедур обычно выбирают алгоритмы, представленные в виде машины Тьюринга (см. [34]). В [21] показано, что все известные естественные формализации алгоритма по сложности эквивалентны машине Тьюринга (с точностью до полинома). Рабином в [40] была доказана теорема о сложности, а Блюмом в [27] — теорема об ускорении. Фишер и Ра-бин (см. [33]) нашли достаточные условия для доказательства трудности задач разрешения теорий в различных классах сложности. В частности, ими показано, что разрешающая процедура для арифметики Пресбургера обладает сложностью по меньшей мере 22". Там же установлено, что разрешающая процедура для теории вещественно замкнутых полей обладает сложностью по меньшей мере 2п. Однако, эту оценку точной назвать пока нельзя: Оппенен показал (см. [31]), что для арифметики Пресбургера существует разрешающий алгоритм, который работает 2" шагов и вопрос о том какая оценка точнее пока открыт. Мейер в [39] показал, что для доказательства разрешимости слабой монадической теории следования второго порядка требуется не меньше шагов.

0(п) раз

Цели работы

Данная работа посвящена исследованию свойств теорий

Т/ = ТЬ(а;, 0,1, <, 4-, /о, /ь - • •, /«), образованных из арифметики А.Л.Семенова +, /о) добавлением функций > 0, которые в работе названы «гиперфункциями». Каждая из них получается итерацией предыдущей. В частности, показано, что такие теории при определённых условиях являются разрешимыми. Также в работе изучается сложность разрешающей процедуры для таких теорий.

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

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

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

Все полученные результаты являются новыми. На защиту выносятся следующие основные результаты.

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

2. Установлено, что если функция /о — периодичная по любому модулю р > 1с периодом меньше р, то гиперфункция от /о является эффективно периодичной по любому модулю р > 1 с периодом 1. Также установлено, что если функция /о — периодичная по любому модулю р > 1с периодом меньше р, а функция fi(x) — периодичная функция, то гиперфункция от функции f(x) fi(x) является периодичной по модулю р для любого р > 1. Следовательно, теории, для которых выполняется одно из двух условий, являются разрешимыми.

3. Показано, что представленный в работе разрешающий алгоритм для любой формулы длины п для определения её истинности в Т/ требует па

2 п мяти не больше чем • Следовательно, разрешающий алгоритм ра

0(п) раз 2" ботает не более ^^ шагов.

0{п) раз

4. Предложен метод кодирования последовательности с помощью бинарного дерева. Используя этот метод, доказано, что для любого разрешающего алгоритма существует формула длины п, для которой время работы алгоритма, определяющего истиность формулы в Т/, будет не меньше 2 чем ,2^, . Таким образом, задача разрешения указанных теорий являем (п) раз ется полной в классе сложности TIME | ) •

Ю(п) раз

Апробация

Начиная с 2006 года содержание глав данной диссертации неоднократно докладывалось на семинаре «Теоретические основы информатики» в ТвГУ.

Доклад по теме диссертации был сделан в 2008 году в Санкт-Петербургском отделении Математического института им.В.А.Стеклова РАН на семинаре по математической логике под руководством академика РАН Ю.В.Матиясевича.

Также доклад по теме диссертации был сделан в 2011 году на международной конференции «Актуальные проблемы прикладной математики, информатики и механики» (Воронеж).

Исследования по теме работы были поддержаны РФФИ, проект № 08-01-00241-а.

Публикации

Список публикаций по теме диссертации включает 5 работ [15], [16], [17], [18], [19]. Работы [16], [17], [19] опубликованы в изданиях, входящих в список рекомендованных ВАК ведущих рецензируемых изданий.

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

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

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

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

В параграфе 2.2 мы определяем термы, с которыми будем в дальнейшем работать:

Ыу, а*, сц+1,., а,) = /г(/ш(- • • (/.ы(/> + + а^-х).) + ат) + аг), где г ^ у, все а^ — константы, после чего, доказываем для них ряд важных для нас свойств.

В параграфе 3.1 мы даем определение теории, образованной из арифметики А.Л.Семенова добавлением функций /¿,г > 0, полученных итерацией согласованной со сложением функции /о, которую мы называем Ту. После чего мы доказываем, что если все гиперфункции являются периодичными по любому натуральному модулю, то любая формула в этой теории эквивалентна экзистенциальной. Далее показано, что преобразование каждой формулы к экзистенциальной может быть эффективным при условии, что все гиперфункции являются эффективно периодичными по любому натуральному модулю.

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

В параграфе 3.3 мы доказываем теоремы, в которых находятся условия на функцию /о, при которых функции /г- будут эффективно периодичными по любому натуральному модулю.

В параграфе 4.1 мы доказываем ряд лемм, при помощи которых оцениваем константы, используемые в разрешающем алгоритме, который приведён в параграфе 3.2. Затем показываем, что время работы разрешающего о.2" алгоритма для любой формулы из теории Т/ не больше, чем , если

0(п) раз формула была длиной п.

В параграфе 4.2 продемонстрирован метод кодирования последовательности с помощью бинарного дерева. Используя этот метод, доказано, что для любого разрешающего алгоритма существует формула длины п из тео2 рии Т/, для которой время работы алгоритма будет не меньше чем •

О(п) раз

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

Список литературы состоит из 46 наименований.

Заключение

В диссертации получены следующие основные результаты:

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

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

3. Если обогатить систему теории Ту обратными функциями для /;, то получится система с элиминацией кванторов, которая также может быть эффективной при упомянутом выше условии.

4. При выполнении условия эффективной периодичности гиперфункций теории являются разрешимыми.

5. Если функция /о — периодичная по любому модулю р > 1с периодом меньше р, то гиперфункция от /о является эффективно периодичной по модулю р > 1с периодом 1.

6. Если функция /о — периодичная по любому модулю р > 1 с периодом меньше р, а функция /1(2) — периодичная функция, тогда гиперфункция от функции /(ж) + является периодичной по модулю р, для любого р > 1.

7. Теория системы ТЬ(о;, 0,1, <, +, /о, /1,. • /т) требует для разрешения не больше чем 2~ времени.

Г/ = ТЬ(а;,0,1)<,+|/о,/ь.>/п)

0{п) раз

8. Теория системы Th(w, 0,1, <, +, /о, /1,. /т), если в ней существует формула, которая взаимно однозначно кодирует два натуральных числа, о.2 требует для разрешения не меньше чем ' гДе # — некоторая кон

0(п) раз станта. Таким образом задача разрешения указанных теорий является полной в классе сложности TIME ( ,2^, J.

Ю(п) раз

Дальнейшие иследования в данной области могут в себя включать:

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

2. Исследования теорий, полученных из арифметики Пресбургера, добавлением функции Аккермана, при фиксировании второго аргумента.

Мы хотим выразить благодарность участникам семинара по математической логике ПОМИ РАН и лично академику Ю.В.Матиясевичу, участникам семинара «Теоретические основы информатики» в ТвГУ за ценные советы и замечания.

1. Адян С.И. Алгоритмические проблемы для групп и полугрупп /С.И. Адян, В.Г. Дурнев//УМЫ. - 2000. - 55:2(332). - С. 3-94.

2. Булос Дж. Вычислимость и логика/Дж. Булос, Р.Джеффри. М.: Мир, 1994. - 396 с.

3. Васылкина Л.В. Структура ((¿,<) является автоматной/Л.В. Васыл-кина//Вестник ТвГУ. Серия: Прикладная математика. 2006. - № 3. - С. 42-45.

4. Верещагин Н.К. Языки и исчисления/Н.К. Верещагин, А. Шепь. М.: МЦНМО, 2002. - 291 с.

5. Гери М. Вычислительные машины и труднорешаемые задачи/М. Гери, Д. Джонсон. М.: Мир, 1982. - 416 с.

6. Дудаков С.М. Трансляционная теорема и автоматные структуры/С.М. Дудаков// Вестник ТвГУ. Серия Прикл. матем. 2006. - 4(21). - С. 5-35.

7. Ершов Ю.Л. Разрешимость элементарной теории дистрибутивных структур с относительными дополнениями и теории фильтров/Ю.Л. Ершов//Алгебра и логика. 1964. - № 3, С. 17-38

8. Ершов Ю.Л. Проблемы разрешимочти и конструктивные моде-ли/Ю.Л. Ершов. М.: Наука, 1980. - 415 с

9. Кейслер Г. Теория моделей /Г. Кейслер, Ч. Чен. М.: Мир, 1977. - 614 с.

10. Пензин Ю. Г. Разрешимость теории целых чисел со сложением, порядком и умножением на произвольное число/Ю. Г. Пензин//Матем. заметки. 1973. - 13:5. - С. 667-675

11. Петров А.Е. Разрешимость теорий обобщений автоматных систем/А.Е. Петров// Вестник ТвГУ. Сер. Прикл. матем. 2010. - №17. С. 21-40

12. Попов И.В. Элиминация кванторов в некоторых обогащениях арифметики Пресбургера/И.В. Попов// Сложные системы: обработка информации, моделирование и оптимизация, Тверь. 2002. - С. 38-47.

13. Семёнов A.JI. Логические теории одноместных функций на натуральном ряде/A.JI. Семёнов//Изв. АН СССР. 1983. - 47(3). - С. 623-658.

14. Семёнов А.Л. О некоторых расширениях арифметики сложения натуральных чисел/А.Л. Семёнов//Изв. АН СССР. 1979. - 43(5). - С. 1175-1195.

15. Снятков A.C. Разрешимость теории Тс = Th(a;, 0,1, <, 4-, СХ)/А.С. Снятков// Вестник ТвГУ. Сер. Прикл. матем. 2007. - 5(35). - С. 113-121

16. Снятков A.C. Разрешимость теории Tj — Th(w,0,1, < , +, f(x), F(x))/A.C. Снятков// Вестник ТвГУ. Сер. Прикл. матем. 2008. - 14(34). - С. 67-77

17. Снятков A.C. Разрешимость теории Tf = Th(a;, 0,1, < 5 +> f(x),., fn)/A.C. Снятков// Модел. и анализ информ. систем. -2010. 17:3. - С. 72-90

18. Снятков A.C. Разрешимость теории Tf — Th(o;,0,1,< , +, f{x),., fn)./A.C. Снятков//Актуальные проблемы прикладной математики, информатики и механики. Сборник трудов международной конференции. 2011. - С. 362-365.

19. Снятков A.C. Нижняя граница времени для разрешения теории с функцией экспоненты/А.С. Снятков// Вестник ТвГУ. Сер. Прикл. матем. 2012. - №17. - Выпуск 2 (25). - С. 5-10.

20. Столбоушкин А.П. Математические основы информатики/А.П. Стол-боушкин, М.А. Тайцлин

21. Трахтенброт Б.А. Сложность алгоритмов и вычислений/Б.А. Трах-тенброт. Новосибирск: изд-во НГУ, 1967. - 247 с.

22. Ackermann W. Zum Hilbertschen Aufbau der reellen Zahlen/W. Ackermann// Mathematische Annalen. 1928. - 99. P. 118-133.

23. Ax J. Diophantine problems over local fields, I/J. Ax, S. Kochen//Amer. J. Math. 1965. - 87. - P. 605-630.

24. Ax J. Diophantine problems over local fields, II. A complete set of axioms for p-adic number theory/J. Ax, S. Kochen//Amer. J. Math.- 1965. 87. - P. 631-648.

25. Ax J. Diophantine problems over local fields, III. Decidable fields/J. Ax, S. Kochen//Ann. Math. 1966. - 83. - P. 437-456

26. Ax J. The elementary theory of finite fields/J. Ax//Ann. Math. 1968. -88. - P. 239-271.

27. Blum M. A Machine-Independent Theory of the Complexity of Recursive Functions/M. Blum//Journal of the ACM. 1967. - 14 (2). - P. 322-336.

28. Blumensath A. Automatic structures/A. Blumensath, E.Graedel//Proc. 15th IEEE Symp. on Logic in Computer Science-Cambridge, 2000. P. 51-62.

29. Church A. A note on the Entscheidungs problem/A. Church//Journal of Symbolic Logic. 1936. - № 1. - P. 40-41

30. Church A. An unsolvable problem of elementary number theory/A. Church//Amer. Journ. of Math. 1936. - 58. - P. 345-363.

31. Oppen D. C. A 22 Upper Bound on the Complexity of Presburger Arithmetic/D. C. Oppen//J. Comput. Syst. Sei. 1978. - 16(3). - P. 323332

32. Ehrenfeucht A. Decidability of the theory of linear ordering relation. -Notices Amer. Math. Soc., 1959, 6, P. 268-269

33. Fischer. M. J. Super-Exponential Complexity of Presburger Arithmetic/M. J. Fischer, M.O. Rabin//Proceedings of the SIAM-AMS Symposium in Applied Mathematics Vol. 7. New York, 1974. - P. 27-41.

34. Garey M.R. Computers and Intractability. A Guide to the Theory of NP-Completeness/M.R. Garey, D.S. Johnson. San Francisco, W.H.Freeman and Company, 1979,- 338 p.

35. Lang S. Introduction to Transcendental Numbers/S. Lang//Addison-Wesley. 1966. - P. 30-31.

36. Lauchli H. On the elementary theory of linear order/H. Lauchli, J. Leonard//Fundam. math. 1966. - 59. - P. 109-116.

37. Macintyre A.J. On the decidability of the real exponential field/A.J. Macintyre, A.J. Wilkie//Kreisel 70th Birthday Volume. 2005. - P. 441467.

38. Meyer A.R. The inherent complexity of theories of ordered sets/A.R. Meyer//Proceedings of the International Congress of Mathematics. -Vancouver, 1974. P. 477-482.

39. Rabin M. O. Speed of Computation of Functions and Classification of Recursive Sets/M. O. Rabin//Bull. Res. Council Israel 8F. 1959. - P. 69-70.

40. Rabin M. O. A simple method for undecidability proofs and some applications/M. O. Rabin//Logic, Methodology and Philosophy of Science, Ii/Ed. Y. Bar-Hillel. Amsterdam: North-Holland. 1969. - P. 92-101

41. Rosser J. B. Extensions of some theorems of Godel and Church/J. B. Rosser//JSL, 1. Chandler's Ford, 1936. - P. 87-91.

42. Tarski A. Arithmetical classes and types of Boolean algebras: Preliminary report/A. Tarski//Bull. Amer. Math. Sos. 1949. - 55. - 64 p.

43. Tarski A. A Decision Method for Elementary Algebra and Geometry/A. Tarski. Los Angeles, Berkeley, 1951. - 63 p.

44. Tarski A. Undecidable theory/A. Tarski,R. Robinson,A. Mostowski. -Amsterdam, North-Holland, 1953. 116 p.

45. Tsankov T. The additive group of the rationals does not have an automatic presentation/T. Tsankov// The Journal of Symbolic Logic.-2011.-76(4).-P. 1341-1351.