Предисловие
В настоящей работе приводятся решения некоторых проблем математической логики и теории алгоритмов, использующие связь вопроса об истинности утверждений с определенными математическими играми. Для иллюстрации рассмотрим известный пример. Пусть, дана замкнутая формула исчисления предикатов, и её предикатные символы проинтерпретированы в некоторой структуре. Нас интересует, истинна ли данная формула в данной структуре. А. Эреыфойхт заметил, что с этим вопросом естественно связать игру. Для этого формула приводится к префиксному виду. Игроку, стремящемуся доказать истинность формулы, соответствуют кванторы существования; а игроку, стремящемуся доказать ложность формулы, соответствуют кванторы общности. Ходы в игре делаются в том порядке, в котором расположены кванторы формулы. Ход игрока состоит в указании какого-либо элемента структуры. В конце игры в бескванторную часть формулы вместо каждой переменной подставляется значение, которое определяется так. Если переменная х была связана квантором С? (ф = 3 или С] = V), то вместо х подставляется тот элемент структуры, который был выбран игроком на ходе, соответствующем квантору (}. Если после подстановки бескванторная часть формулы становится истинной, то выиграл первый игрок; а если бескванторная часть формулы становится ложной, то выиграл второй игрок. Очевидно, что если исходная формула истинна, то у первого игрока есть выигрывающая стратегия; а если исходная формула ложна, то выигрывающая стратегия есть у второго игрока.
Заметим, что в отличие от примера из предыдущего абзаца мы будем рассматривать и игры в которых количество ходов бесконечно. Если для конечных игр просто доказать, что у одного из двух противников есть выигрывающая стратегия, то для бесконечных игр это очень нетривиальное свойство, называемое детерминированностью.
Обратимся к первой главе работы. Как известно, структура натуральных чисел со сложением и умножением имеет неразрешимую теорию первого порядка. Это обстоятельство делает особенно важным нахождение достаточно сильных разрешимых теорий. Одной из таких теорий является монадическая теория бинарного дерева. Бинарное дерево задаётся множеством всех двоичных слов и двумя операциями на нем: приписывание к слову нуля справа и приписывание к слову единицы справа. Монадическая теория состоит из формул, построенных с помощью этих двух операций, переменных
2
по словам и по множествам слов, предиката принадлежности, пропозициональных связок и кванторов по переменным обоих типов. Наличие в языке переменных по множествам делает эту теорию очень выразительной. К ней сводятся многие интересные вопросы математической логики и теории автоматов. Один из последних примеров такого сведения недавно предложен В. Л. Селивановым в докладе, представленном в [7]. Там изучается круг вопросов следующего типа: “можно ли по монадической формуле (со свободными переменными) эффективно узнать, выражает ли она предикат, выразимый элементарной формулой в той же сигнатуре?”.
Доказательство разрешимости монадической теории бинарного дерева было найдено М. Рабином в 1969 году [И]. Каждой формуле рассматриваемого языка эффективно сопоставляется конечный автомат, работающий на бинарном дереве, вершины которого размечены подходящим конечным алфавитом. Ключевым оказывается переход от автомата, распознающего какое-то множество разметок дерева, к автомату, распознающему дополнение до зтого множества. Доказательство Рабина было очень сложным и, в частности, оно использовало трансфинитную индукцию по всем счётным ординалам. В докладе на международном математическом конгрессе в Пицце Рабин поставил проблему нахождения болсс простого доказательства, которое не использовало бы трапсфинитной индукции 15].1 В теореме 1.1 мы предлагаем такое доказательство, основанное на играх. Оно было изложено в курсе лекций «Разрешимые теории», который был прочитан А. Л. Семёновым на кафедре математической логики Московского государственного университета в 1979/1980 учебном году. В 1981 году на той же кафедре автор защитил дипломную работу, содержащую этот результат. Соответствующая публикация автора в российском журнале “Семиотика и информатика” [3] была переведена международным журналом “Bulletin of the European Association for Theoretical Computer Science" [6].
Автор признателен Сергею Ивановичу Адяну, который посоветовал более формально выразить различие между доказательством из (14 и нашим доказательством, изложенным в § 2. Точные утверждения для выявления указанного различия вероятно связаны с проблемой аксиоматизации, поставленной 11. С. Новиковым. Эта проблема была решена для одной функции следования в 17]. План решения этой проблемы для двух функций следования обсуждается в § 3.
1 Иерпд* из постлятсиных а атом докладе пройдем гласила: А. Упростить доказательство теоремы 2(ti), возможно, за счёт устранения тралефижпном индукции, использояаикой в [2)«. Здесь теорема 2(и) — это ключевое утверждение из рассуждения Рябина. (2) — статья [1*1. из нашего списка литературы.
3
Во второй главе работы рассматривается общая теория алгоритмов, то есть теория изучающая свойства алгоритмов, не зависящие от конкретных моделей вычислений. С точки зрения математической логики значительная часть этой теории может рассматриваться как теория некоторой структуры, введённой X. Фридманом в [10]. Мы показываем, что для обширного класса формул истинность в этой структуре выражается посредством некоторой игры, которая не использует понятия вычислимости ([4]). Предлагаемая интерпретация позволяет прояснить известный в общей теории алгоритмов феномен релятивизуемости. Под релятивизацией понимается замена вычислимости на вычислимость относительно какого-то оракула. Построить истинную формулу общей теории алгоритмов, которая становится ложной при релятивизации любым невычислимым оракулом. — это просто. Тем не менее, как покалывает математическая практика, релятивизации всех “естественных” истинных утверждений тоже истинны.
Третья глава работы посвящена вопросу, которым интересовались математики еще в XVIII веке. Л именно, математическому уточнению понятия случайной двоичной бесконечной последовательности. А. II. Колмогоров в [1] сравнивает два способа такого уточнения. В первом способе используется введённое Колмогоровым понятие энтропии конечной двоичной последовательности. Для бесконечной двоичной последовательности а функция К (а ? п) сопоставляет натуральному числу п энтропию начала о- длины п. Неформально говоря, последовательность тем более случайна, чем больше значения функции К. Второй способ уточнения понятия случайности исходит из классического закона больших чисел. То есть частота нулей и единиц должна стремиться к 1/2. Но последовательность 010101... явно неслучайна! Может быть потребовать, чтобы закон больших чисел выполнялся для всякой подпоследовательности? Так тоже не получится, потому что можно рассмотреть подпоследовательность, состоящую как раз из тех членов начальной последовательности, которые равны нулю. Разумным компромиссом оказывается требование выполнения закона больших чисел для подпоследовательностей из достаточно широкого класса. Колмогоров в [1 рассмотрел класс всех подпоследовательностей, номера членов которых задаются вычислимыми монотонно возрастающими функциями. Колмогоров доказал, что для этого класса последовательности случайные в смысле второго способа уточнения бывают “максимально неслучайными” в смысле первого способа уточнения. А именно, он построил случайную в смысле закона больших чисел
•1
последовательность <*, у которой К(а(п) = О(к^п). То есть энтропия начала а длины п почти так же мала, как длина двоичной записи числа п. В той же статье Колмогоров выдвинул гипотезу, что его результат можно усилить, расширив класс подпоследовательностей, для которых требуется выполнение закона больших чисел. Расширенный класс подпоследовательностей, который предложил рассмотреть А. Н. Колмогоров, полностью описан в абзаце перед определением 111.1. В [5] автор опроверг гипотезу Колмогорова, доказав, что если 3$ < 1 Зс Уп К (а ; та) < еп Л- с, то последовательность а неслучайна в смысле закона больших чисел. При этом используются игры с переменными ставками (как в казино).
Для удобства читателя основные понятия из теории конечных автоматов на бесконечных деревьях приведены в § 1 главы I. Что касается использования основных понятий обшей теории алгоритмов (в главе И) и теории колмогоровскои энтропии (в главе III), то мы следуем книге В. А. Успенского и А. Л. Семёноза |8 .
Автор очень благодарен своему научному руководи телю Алексею Львовичу Семёнову за большую поддержку в работе.
5
ГЛАВА I
Упрощённое доказательство теоремы Рабина о разрешимости монадической теории дерева
Изложенный в первой главе результат используется для доказательства разрешимости монадической теории дерева с двумя функциями следования. Расскажем об обшем строении этого доказательства. Во-первых, язык теории удобно модифицировать так. чтобы заменить индивидные переменные на предикатные. Для этого следует вместо вершин дерева говорить об одноэлементных множествах. эти вершины содержащих. Во-вторых, набор одноместных предикатов будет отождествляться с разметкой дерева наборами значений характеристических функций. В-третьих, каждой формуле со с вободными переменными эффективно сопоставляется конечный автомат. Этот автомат распознаёт в точности разметки, соответствующие тем интерпретациям свободных переменных, при которых формула становится истинной. Сопоставление автомата происходит индукцией по построению формулы. Таким образом, разрешимость теории вытек;1ет из следующих пяти .алгоритмических фактов:
(1) можно построить автомат для распознавания области истинности атомарной формулы;
(2) по двум автоматам, распознающим какие-то множества, можно построить автомат для распознавания объединения этих множеств;
(3) по автомату, распознающему множество («+1)-элементных наборов разметок, можно построить автомат для распознавания проекции этого множества на первые п координат;
(4) но автомату, распознающему какое-то множество, можно построить автомат для распознавания дополнения этого множества;
(5) по автомату можно выяснить, распознаёт ли он пустое множество.
Первые три факта устанавливаются очень просто. При этом в доказательствах фактов (2) и (3) существенно используется недетерминированность автоматов. Но именно недетерминированность оказывается основной проблемой при установлении (4). Факт (о)
б
- Київ+380960830922