S2S (математика)

В математике S2S — это монадическая теория второго порядка с двумя преемниками. Это одна из самых выразительных известных естественных разрешимых теорий, со многими разрешимыми теориями, интерпретируемыми в S2S. Ее разрешимость была доказана Рабином в 1969 году. [1]

Основные свойства

Объекты первого порядка S2S — это конечные двоичные строки. Объекты второго порядка — это произвольные множества (или унарные предикаты) конечных двоичных строк. S2S имеет функции s → s 0 и s → s 1 на строках, а предикат s ∈ S (эквивалентно, S ( s )), означающий, что строка s принадлежит множеству S .

Некоторые свойства и соглашения:

  • По умолчанию строчные буквы относятся к объектам первого порядка, а заглавные — к объектам второго порядка.
  • Включение множеств делает S2S вторым порядком, при этом «монадический» указывает на отсутствие k -арных предикатных переменных для k >1.
  • Конкатенация строк s и t обозначается как st и не является обычно доступной в S2S, даже s →0 s . Префиксное отношение между строками определимо.
  • Равенство является примитивным, или его можно определить как s = t ⇔ ∀ S ( S ( s ) ⇔ S ( t )) и S = ​​T ⇔ ∀ s ( S ( s ) ⇔ T ( s )).
  • Вместо строк можно использовать (например) натуральные числа с n →2 n +1 и n →2 n +2, но никаких других операций.
  • Множество всех двоичных строк обозначается как {0,1} * , используя звезду Клини .
  • Произвольные подмножества {0,1} * иногда отождествляются с деревьями, в частности, с {0,1}-меченым деревом {0,1} * ; {0,1} * образует полное бесконечное двоичное дерево.
  • Для сложности формулы префиксное отношение в строках обычно рассматривается как отношение первого порядка. Без него не все формулы были бы эквивалентны формулам Δ 1 2. [2]
  • Для свойств, выражаемых в S2S (рассмотрение набора всех двоичных строк как дерева), для каждого узла только O (1) бит может быть передано между левым поддеревом и правым поддеревом и остальными (см. сложность связи ).
  • Для фиксированного k функция от строк до k (т. е. натуральных чисел ниже k ) может быть закодирована одним набором. Более того, s , t ⇒ s 01 t ′ , где t ′ удваивает каждый символ t, является инъективным, а s ⇒ { s 01 t ′ : t∈{0,1} * } является S2S-определимым. Напротив, по аргументу сложности связи, в S1S (ниже) пара наборов не кодируется одним набором.

Ослабления S2S: Слабое S2S (WS2S) требует, чтобы все множества были конечными (обратите внимание, что конечность выражается в S2S с помощью леммы Кёнига ). S1S можно получить, потребовав, чтобы «1» не появлялось в строках, и WS1S также требует конечности. Даже WS1S может интерпретировать арифметику Пресбургера с предикатом для степеней 2, поскольку множества могут использоваться для представления неограниченных двоичных чисел с определяемым сложением.

Сложность решения

S2S разрешима, и каждая из S2S, S1S, WS2S, WS1S имеет неэлементарную сложность принятия решения, соответствующую линейно растущему стеку экспонент. Для нижней границы достаточно рассмотреть предложения Σ 1 1 WS1S. Один квантификатор второго порядка может быть использован для предложения арифметического (или другого) вычисления, которое может быть проверено с использованием квантификаторов первого порядка, если мы можем проверить, какие числа равны. Для этого, если мы соответствующим образом закодируем числа 1.. m , мы можем закодировать число с двоичным представлением i 1 i 2 ... i m как i 1 1 i 2 2 ... i m m , которому предшествует охрана. Объединяя проверку охран и повторно используя имена переменных, число бит линейно зависит от числа экспонент. Для верхней границы, используя процедуру принятия решения (ниже), предложения с k -кратным чередованием квантификаторов могут быть решены за время, соответствующее k + O (1)-кратному возведению в степень длины предложения (с равномерными константами).

Аксиоматизация

WS2S можно аксиоматизировать с помощью определенных базовых свойств и индукционной схемы. [3]

S2S можно частично аксиоматизировать следующим образом:
(1) ∃! s ∀ t ( t 0≠ s ∧ t 1≠ s ) (пустая строка, обозначается ε; ∃! s означает «существует уникальный s »)
(2) ∀ s , t ∀ i ∈{0,1} ∀ j ∈{0,1} ( si = tj ⇒ s = t ∧ i = j ) (использование i и j является сокращением; для i = j , 0 не равно 1)
(3) ∀ S ( S (ε) ∧ ∀ s ( S ( s ) ⇒ S ( s 0) ∧ S ( s 1))⇒ ∀ s S (s)) ( индукция )
(4) ∃ S ∀ s ( S ( s ) ⇔ φ( s )) ( S не свободен в φ)

(4) — это схема понимания над формулами φ, которая всегда справедлива для логики второго порядка. Как обычно, если φ имеет свободные переменные, не показанные, мы берем универсальное замыкание аксиомы. Если равенство примитивно для предикатов, то также добавляется экстенсиональность S = T ⇔ ∀ s ( S ( s ) ⇔ T ( s )). Поскольку у нас есть понимание, индукция может быть одним утверждением, а не схемой.

Аналогичная аксиоматизация S1S является полной. [4] Однако для S2S полнота открыта (по состоянию на 2021 год). Хотя S1S имеет униформизацию, не существует определимой (даже допускающей параметры) функции выбора S2S , которая при заданном непустом множестве S возвращает элемент S , [5] и схемы понимания обычно дополняются различными формами аксиомы выбора . Однако (1)-(4) является полной при расширении схемой детерминации для некоторых игр четности . [6]

S2S также может быть аксиоматизирован предложениями Π 1 3 (используя префиксное отношение на строках в качестве примитива). Однако оно не является конечно аксиоматизируемым и не может быть аксиоматизировано предложениями Σ 1 3 , даже если мы добавим схему индукции и конечный набор других предложений (это следует из его связи с Π 1 2 -CA 0 ).

Для каждого конечного k монадическая теория второго порядка (MSO) счетных графов с древовидной шириной ≤ k (и соответствующая древовидная декомпозиция) интерпретируема в S2S (см. теорему Курселя ). Например, теория MSO деревьев (как графов) или последовательно-параллельных графов разрешима. Здесь (т. е. для ограниченной ширины дерева) мы также можем интерпретировать квантификатор конечности для набора вершин (или ребер), а также подсчитывать вершины (или ребра) в наборе по модулю фиксированного целого числа. Разрешение несчетных графов не меняет теорию. Также, для сравнения, S1S может интерпретировать связные графы ограниченной путевой ширины .

Напротив, для каждого набора графов неограниченной древовидной ширины его экзистенциальная (т.е. Σ 1 1 ) теория MSO неразрешима, если мы допускаем предикаты как на вершинах, так и на ребрах. Таким образом, в некотором смысле, разрешимость S2S является наилучшей возможной. Графы с неограниченной древовидной шириной имеют большие миноры сетки, которые можно использовать для моделирования машины Тьюринга .

При сведении к S2S теория MSO счетных порядков разрешима, как и теория MSO счетных деревьев с их порядками Клини–Брауэра . Однако теория MSO для ( , <) неразрешима. [7] [8] Теория MSO ординалов <ω 2 разрешима; разрешимость для ω 2 не зависит от ZFC (предполагая Con(ZFC + слабо компактный кардинал )). [9] Кроме того, ординал определим с помощью монадической логики второго порядка на ординалах тогда и только тогда, когда он может быть получен из определимых регулярных кардиналов сложением и умножением ординалов. [10] Р {\displaystyle \mathbb {R} }

S2S полезен для разрешимости некоторых модальных логик, при этом семантика Крипке естественным образом приводит к деревьям.

S2S+U (или просто S1S+U) неразрешимо, если U является неограниченным квантором — U X Φ( X ) тогда и только тогда, когда Φ( X ) выполняется для некоторого произвольно большого конечного X . [11] Однако WS2S+U, даже с квантификацией по бесконечным путям, разрешимо, даже с подформулами S2S, которые не содержат U. [12]

Сложность формулы

Множество двоичных строк определимо в S2S тогда и только тогда, когда оно регулярно (т.е. образует регулярный язык ). В S1S (унарный) предикат на множествах (без параметров) определим тогда и только тогда, когда оно является ω-регулярным языком . Для S2S для формул, которые используют свои свободные переменные только на строках, не содержащих 1, выразительность такая же, как и для S1S.

Для каждой формулы S2S φ( S 1 ,..., S k ), (с k свободными переменными) и конечным деревом двоичных строк T , φ( S 1 ∩ T,..., S k ∩ T) может быть вычислено за время, линейное по | T | (см. теорему Курселя ), но, как отмечено выше, накладные расходы могут быть итерированы экспоненциально по размеру формулы (точнее, время равно ). О ( | Т | к ) + 2 О ( | ϕ | ) 2 {\displaystyle O(|T|k)+2_{O(|\phi |)}^{2}}

Для S1S каждая формула эквивалентна формуле Δ 1 1 и булевой комбинации арифметических формул Π 0 2. Более того, каждая формула S1S эквивалентна принятию соответствующим ω-автоматом параметров формулы. Автомат может быть детерминированным автоматом четности: автомат четности имеет целочисленный приоритет для каждого состояния и принимает тогда и только тогда, когда наивысший приоритет, встречающийся бесконечно часто, является нечетным (или четным).

Для S2S, используя древовидные автоматы (ниже), каждая формула эквивалентна формуле Δ 1 2. Более того, каждая формула S2S эквивалентна формуле всего с четырьмя кванторами, ∃ S ∀ T ∃ s ∀ t ... (предполагая, что наша формализация имеет как префиксное отношение, так и функции преемника). Для S1S достаточно трех кванторов (∃ S ∀ s ∃ t ), а для WS2S и WS1S достаточно двух кванторов (∃ S ∀ t ); префиксное отношение здесь не нужно для WS2S и WS1S.

Однако со свободными переменными второго порядка не каждая формула S2S может быть выражена в арифметике второго порядка только через трансфинитную рекурсию Π 1 1 (см. обратную математику ). RCA 0 + (схема) {τ: τ является истинным предложением S2S} эквивалентна (схеме) {τ: τ является предложением Π 1 3, доказуемым в Π 1 2 -CA 0 }. [13] [14] Над базовой теорией схемы эквивалентны (схеме над k ) ∀ S ⊆ω ∃α 1 <...<α k L α 1 ( S ) ≺ Σ 1 ... ≺ Σ 1 L α k (S), где L является конструируемой вселенной (см. также большой счетный ординал ). Из-за ограниченной индукции Π 1 2 -CA 0 не доказывает, что все истинные (в рамках стандартной процедуры принятия решения) утверждения Π 1 3 S2S на самом деле истинны, даже если каждое такое предложение доказуемо Π 1 2 -CA 0 .

Более того, для заданных наборов двоичных строк S и T следующие условия эквивалентны:
(1) T можно определить с помощью S2S из некоторого набора двоичных строк, вычислимого за полиномиальное время из S. (
2) T можно вычислить из набора выигрышных позиций для некоторой игры, выигрышем которой является конечная булева комбинация наборов Π 0 2 ( S ).
(3) T можно определить из S в арифметическом μ-исчислении (арифметические формулы + наименьшая логика с фиксированной точкой ).
(4) T находится в наименьшей β-модели (т. е. ω-модели, теоретико-множественный аналог которой транзитивен ), содержащей S и удовлетворяющей всем Π 1 3 следствиям из Π 1 2 -CA 0 .

Эскиз доказательства:
См . [13] и [15] , но вкратце доказательство выглядит следующим образом. (1)⇒(2) следует из нижеприведенного доказательства разрешимости с использованием древесных автоматов. (2)⇒(1) следует путем преобразования игры, связанной с двоичной строкой s, в игру с четностью дерева с фиксированным числом приоритетов, а затем слияния этих деревьев в одно дерево (двоичные деревья можно объединить здесь с помощью s , t ⇒ s 01 t ′ , где t ′ удваивает каждый символ t ). Нижеприведенное доказательство определенности (в разделе разрешимости) также приводит к (2)⇒(3). Π 1 2 -CA 0 доказывает монотонную индукцию Δ 1 2 , поэтому (3)⇒(4).

Для (3)⇒(2) определите игру, в которой игрок 1 пытается показать, что желаемый элемент s находится внутри наименьшей неподвижной точки. Игрок 1 постепенно маркирует элементы, включая s , рациональными числами, предназначенными для соответствия порядковым этапам монотонной индукции (любой счетный порядковый номер вкладывается в ). Игрок 2 играет элементами со строго убывающими метками (и он может пасовать) и выигрывает, если последовательность бесконечна или игрок 2 выигрывает последнюю вспомогательную игру. Во вспомогательной игре игрок 1 пытается показать, что последний элемент, выбранный игроком 2, является допустимым индуктивным шагом, использующим элементы с меньшими метками. Теперь, если s не находится в наименьшей неподвижной точке, то набор меток необоснован, или индуктивный шаг неверен, и (используя монотонность) это может быть выбрано игроком 2. (Если игрок 1 играет меньшей меткой вне наименьшей неподвижной точки, игрок 2 может использовать ее (отказываясь от вспомогательной игры), в противном случае (используя монотонность) игрок 2 может использовать стратегию вспомогательной игры, которая предполагает, что набор меньших меток в исходной игре будет равен наименьшей неподвижной точке.) В {\displaystyle \mathbb {Q} }

Для (4)⇒(3) мы используем монотонную индукцию для построения начального сегмента конструируемой иерархии выше заданного действительного числа r . Это работает до тех пор, пока каждый ординал α идентифицируется некоторым соответствующим образом выражаемым свойством α, так что мы можем закодировать α натуральным числом и продолжить. Теперь предположим, что мы построили L α (r), и индуктивный шаг (который использует L α (r) в качестве параметра) позволяет исследовать L β (r). Если новый факт Σ 1 (L(r),∈,r) появляется между α и β, мы можем использовать его для маркировки α и продолжить. В противном случае мы получаем указанные выше Σ 1 элементарные цепи, длина которых соответствует глубине вложенности монотонных индуктивных определений.

Для эквивалентности RCA 0 +S2S с {Π 1 3 φ: Π 1 2 -CA 0 ⊢φ}, для каждого k позиционная определенность с k приоритетами доказуема в Π 1 2 -CA 0 , в то время как остальное (в терминах доказательства предложений S2S) может быть сделано в слабой базовой теории. Наоборот, RCA 0 +S2S дает нам схему определенности, которая дает существование наименьших неподвижных точек (с помощью модификации вышеприведенного (3)⇒(2) и даже без требования позиционности; см. ссылку). В свою очередь, их существование (с использованием (4)⇒(3)) дает искомые Σ 1 элементарные цепи.

Модели S1S и S2S

Помимо стандартной модели (которая является уникальной моделью MSO для S1S и S2S), существуют и другие модели для S1S и S2S, которые используют некоторые, а не все подмножества домена (см. семантику Хенкина ).

Для каждого S ⊆ω множества, рекурсивные в S, образуют элементарную подмодель стандартной модели S1S, и то же самое для каждого непустого набора подмножеств ω, замкнутого относительно объединения по Тьюрингу и сводимости по Тьюрингу. [16]

Это следует из относительной рекурсивности определимых множеств S1S плюс униформизация:
- φ( s ) (как функция s ) может быть вычислена из параметров φ и значений φ( s ′ ) для конечного множества s ′ (с его размером, ограниченным числом состояний в детерминированном автомате для φ).
- Свидетель для ∃ S φ( S ) может быть получен путем выбора k и конечного фрагмента S ′ из S , и многократного расширения S ′ таким образом, чтобы наивысший приоритет во время каждого расширения был k и чтобы расширение могло быть завершено до S , удовлетворяющего φ , без достижения приоритетов выше k (это разрешено только для начального S ′ ). Кроме того, используя лексикографически наименьшие кратчайшие варианты, существует формула S1S φ' такая, что φ'⇒φ и ∃ S φ( S ) ⇔∃! S φ'( S ) (т.е. униформизация; φ может иметь свободные переменные, не показанные; φ' зависит только от формулы φ).

Минимальная модель S2S состоит из всех регулярных языков на двоичных строках. Это элементарная подмодель стандартной модели, поэтому если параметрически-свободный определяемый набор деревьев S2S непустой, то он включает регулярное дерево. Регулярный язык также можно рассматривать как регулярное {0,1}-меченое полное бесконечное бинарное дерево (идентифицированное с предикатами на строках). Помеченное дерево является регулярным, если его можно получить путем развертывания вершинно-меченого конечного ориентированного графа с начальной вершиной; (направленный) цикл в графе, достижимый из начальной вершины, дает бесконечное дерево. При такой интерпретации и кодировании регулярных деревьев каждое истинное предложение S2S может быть уже доказуемо в элементарной функциональной арифметике . Именно нерегулярные деревья могут потребовать непредикативного понимания для определенности (ниже). Существуют нерегулярные (т.е. содержащие нерегулярные языки) модели S1S (и, предположительно, S2S) (как со стандартной частью первого порядка, так и без нее) с вычислимым отношением удовлетворения. Однако набор рекурсивных наборов строк не образует модель S2S из-за отсутствия понимания и определенности.

Разрешимость S2S

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

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

Определенность: Доказуемо, что в ZFC игры Бореля определены , и доказательство определенности для булевых комбинаций формул Π 0 2 (с произвольными действительными параметрами) также дает здесь стратегию, которая зависит только от текущего состояния и позиции в дереве. Доказательство проводится индукцией по числу приоритетов. Предположим, что имеется k приоритетов, причем наивысший приоритет равен k , и что k имеет правильную четность для игрока 2. Для каждой позиции (позиция дерева + состояние) назначьте наименьший порядковый номер α (если есть) так, чтобы у игрока 1 была выигрышная стратегия со всеми введенными (после одного или нескольких шагов) позициями приоритета k (если есть) с метками <α. Игрок 1 может выиграть, если начальная позиция помечена: Каждый раз, когда достигается состояние приоритета k , порядковый номер уменьшается, и, более того, между уменьшениями игрок 1 может использовать стратегию для k -1 приоритетов. Игрок 2 может выиграть, если позиция не помечена: По определенности для k -1 приоритетов у игрока 2 есть стратегия, которая выигрывает или входит в непомеченное состояние приоритета k , в этом случае игрок 2 может снова использовать эту стратегию. Чтобы сделать стратегию позиционной (по индукции по k ), при игре во вспомогательную игру, если две выбранные позиционные стратегии ведут к одной и той же позиции, продолжайте со стратегией с более низким α или для того же α (или для игрока 2) с более низкой начальной позицией (чтобы мы могли переключать стратегию конечное число раз).

Детерминизация автоматов: Для детерминизации кондетерминированных древовидных автоматов достаточно рассмотреть ω-автоматы, обрабатывая выбор ветви как входные данные, детерминируя автомат и используя его для детерминированного древовидного автомата. Обратите внимание, что это не работает для недетерминированных древовидных автоматов, так как детерминизация для перехода влево (т. е. s → s 0) может зависеть от содержимого правой ветви; в отличие от недетерминированности, детерминированные древовидные автоматы не могут даже принимать точно непустые множества. Чтобы детерминировать недетерминированный ω-автомат M (для кондетерминированного взять дополнение, отметив, что детерминированные четные автоматы замкнуты относительно дополнений), мы можем использовать дерево Сафры , в котором каждый узел хранит набор возможных состояний M , а создание и удаление узлов основано на достижении состояний с высоким приоритетом. Подробности см. в [17] или. [18]

Разрешимость принятия: принятие недетерминированным автоматом четности пустого дерева соответствует игре четности на конечном графе G. Используя указанную выше позиционную (также называемую безпамятной) определенность, это можно смоделировать с помощью конечной игры, которая заканчивается, когда мы достигаем цикла, с условием выигрыша, основанным на состоянии с наивысшим приоритетом в цикле. Умная оптимизация дает алгоритм квазиполиномиального времени [19] , который является полиномиальным временем, когда число приоритетов достаточно мало (что часто встречается на практике).

Теория деревьев: Для разрешимости логики MSO на деревьях (т. е. графах, которые являются деревьями), даже с конечностью и модульными подсчетными квантификаторами для объектов первого порядка, мы можем встроить счетные деревья в полное бинарное дерево и использовать разрешимость S2S. Например, для узла s мы можем представить его потомков как s 1, s 01, s 001 и т. д. Для несчетных деревьев мы можем использовать теорему Шелаха-Ступа (ниже). Мы также можем добавить предикат для множества объектов первого порядка, имеющих мощность ω 1 , и предикат для мощности ω 2 , и так далее для бесконечных регулярных кардиналов. Графы ограниченной ширины дерева интерпретируются с помощью деревьев, и без предикатов над ребрами это также применимо к графам ограниченной ширины клики .

Объединение S2S с другими разрешимыми теориями

Расширения монадических теорий деревьев: По теореме Шелаха-Ступа [20] [21] если монадическая реляционная модель M разрешима, то разрешима и ее аналог дерева. Например, (по модулю выбора формализации) S2S является аналогом дерева {0,1}. В аналоге дерева объекты первого порядка являются конечными последовательностями элементов M, упорядоченными по расширению, и M -отношение P i отображается в P i '( vd 1 ,..., vd k ) ⇔ P i ( d 1 ,..., d k ) с P i ' false в противном случае ( d j ∈ M , а v является (возможно, пустой) последовательностью элементов M ). Доказательство похоже на доказательство разрешимости S2S. На каждом шаге (недетерминированный) автомат получает кортеж из M объектов (возможно, второго порядка) в качестве входных данных, и формула M определяет, какие переходы состояний разрешены. Игрок 1 (как и выше) выбирает отображение child⇒state, которое разрешено формулой (учитывая текущее состояние), а игрок 2 выбирает child (узла) для продолжения. Чтобы засвидетельствовать отклонение недетерминированным автоматом, для каждого (узла, состояния) выберите набор пар (child, state) таким образом, чтобы для каждого выбора по крайней мере одна из пар попадала, и чтобы все полученные пути приводили к отклонению.

Объединение монадической теории с теорией первого порядка: теорема Фефермана–Воота расширяется/применяется следующим образом. Если M — модель MSO, а N — модель первого порядка, то M остается разрешимой относительно оракула (Theory( M ) , Theory( N )) даже если M дополнена всеми функциями M → N , где M отождествляется со своими первыми объектами, и для каждого s ∈ M мы используем непересекающуюся копию N , с соответствующим образом измененным языком. Например, если N — это ( ,0,+,⋅), мы можем заявить ∀(function f ) ∀ s ∃ r ∈ N s f ( s ) + N s r = 0 N s . Если M есть S2S (или, в более общем смысле, древовидный аналог некоторой монадической модели), автоматы теперь могут использовать N -формулы и тем самым преобразовывать f : M → N k в кортеж из M множеств. Дизъюнктность необходима, так как в противном случае для любого бесконечного N с равенством расширенное S2S или просто WS1S неразрешимо. Кроме того, для (возможно неполной) теории T теория T M M -произведений T разрешима относительно оракула ( Theory ( M ) , T ) , где модель T M использует произвольную дизъюнктную модель N s из T для каждого s ∈ M (как и выше, M является моделью MSO; Theory( N s ) может зависеть от s ). Доказательство проводится индукцией по сложности формулы. Пусть v s будет списком свободных N s переменных, включая f ( s ), если функция f свободна. По индукции можно показать, что v s используется только через конечный набор N -формул с | v s | свободными переменными. Таким образом, мы можем количественно оценить все возможные результаты, используя N (или T Р {\displaystyle \mathbb {R} } ) ответить на вопрос, что возможно, и, имея список возможностей (или ограничений), сформулировать соответствующее предложение на языке М.

Кодирование в расширения S2S: Каждый разрешимый предикат на строках может быть закодирован (с линейным временем кодирования и декодирования) для разрешимости S2S (даже с расширениями выше) вместе с закодированным предикатом. Доказательство: Учитывая недетерминированный бесконечный древесный автомат, мы можем разбить множество конечных двоичных помеченных деревьев (имеющих метки, над которыми может работать автомат) на конечное число классов таким образом, что если полное бесконечное двоичное дерево может быть составлено из деревьев одного класса, принятие зависит только от класса и начального состояния (т. е. состояния, в котором автомат входит в дерево). (Обратите внимание на грубое сходство с леммой о накачке .) Например, (для автомата с четностью) присвойте деревьям один и тот же класс, если у них одинаковый предикат, заданный initial_state и множество Q пар (state, highest_priority_reached) возвращает , может ли игрок 1 (т. е. недетерминизм) одновременно заставить все ветви соответствовать элементам Q. Теперь для каждого k выберите конечный набор деревьев (подходящих для кодирования), которые принадлежат к одному и тому же классу для автоматов 1- k , с выбором класса, согласованным по k . Чтобы закодировать предикат, закодируйте некоторые биты, используя k =1, затем больше битов, используя k =2, и так далее.

Ссылки

  1. ^ Рабин, Майкл (1969). "Разрешимость теорий второго порядка и автоматов на бесконечных деревьях" (PDF) . Труды Американского математического общества . 141 .
  2. ^ Джанин, Дэвид; Ленци, Джакомо. О структуре монадической логики двоичного дерева. MFCS 1999. doi :10.1007/3-540-48340-3_28.
  3. ^ Siefkes, Dirk (1971), Система аксиом для слабой монадической теории второго порядка двух преемников
  4. ^ Риба, Колин (2012). Теоретико-модельное доказательство полноты аксиоматизации монадической логики второго порядка на бесконечных словах (PDF) . TCS 2012. doi :10.1007/978-3-642-33475-7_22.
  5. ^ Carayol, Arnaud; Löding, Christof (2007), "MSO на бесконечном двоичном дереве: выбор и порядок" (PDF) , Computer Science Logic , Lecture Notes in Computer Science, т. 4646, стр.  161– 176, doi :10.1007/978-3-540-74915-8_15, ISBN 978-3-540-74914-1, S2CID  14580598
  6. ^ Дас, Анупам; Риба, Колин (2020). «Функциональная (монадическая) теория второго порядка бесконечных деревьев». Логические методы в информатике . 16 (4). arXiv : 1903.05878 . doi : 10.23638/LMCS-16(4:6)2020. S2CID  76666389.(В предварительной версии 2015 года ошибочно утверждалось о доказательстве полноты без схемы детерминированности.)
  7. ^ Гуревич, Юрий; Шелах, Сахарон (1984). «Монадическая теория и «следующий мир»». Israel Journal of Mathematics . 49 ( 1– 3): 55– 68. doi : 10.1007/BF02760646 . S2CID  15807840.
  8. ^ «Какова степень Тьюринга монадической теории действительной прямой?». MathOverflow . Получено 14 ноября 2022 г.
  9. ^ Гуревич, Юрий; Магидор, Менахем; Шелах, Сахарон (1993). "Монадическая теория ω2" (PDF) . Журнал символической логики . 48 (2): 387– 398. doi :10.2307/2273556. JSTOR  2273556. S2CID  120260712.
  10. ^ Ниман, Итай (2008), «Монадическая определимость ординалов» (PDF) , Computational Prospects of Infinity , Lecture Notes Series, Institute for Mathematical Sciences, National University of Singapore, т. 15, стр.  193–205 , doi :10.1142/9789812796554_0010, ISBN 978-981-279-654-7
  11. ^ Боянчик, Миколай; Парис, Павел; Торуньчик, Шимон (2015), Теория MSO+U (N, <) неразрешима , arXiv : 1502.04578
  12. ^ Боянчик, Миколай (2014), Слабое MSO+U с квантификаторами пути над бесконечными деревьями , arXiv : 1404.7278
  13. ^ ab Kołodziejczyk, Leszek; Michalewski, Henryk (2016). Насколько недоказуема теорема Рабина о разрешимости? . LICS '16: 31-й ежегодный симпозиум ACM/IEEE по логике в компьютерных науках. arXiv : 1508.06780 .
  14. ↑ Колодзейчик, Лешек (19 октября 2015 г.). «Вопрос о разрешимости S2S». ФОМ.
  15. ^ Хайнач, Кристоф; Мёллерфельд, Михаэль (2010). «Сила определенности Π12-понимания» (PDF) . Annals of Pure and Applied Logic . 161 (12): 1462– 1470. doi :10.1016/j.apal.2010.04.012.
  16. ^ Колодзейчик, Лешек; Михалевский, Хенрик; Прадич, Сесилия; Скшипчак, Михал (2019). «Логическая сила теоремы Бючи о разрешимости». Логические методы в информатике . 15 (2): 16:1–16:31.
  17. ^ Питерман, Нир (2006). От недетерминированных автоматов Бюхи и Стритта к детерминированным автоматам четности . 21-й ежегодный симпозиум IEEE по логике в компьютерных науках (LICS'06). стр.  255–264 . arXiv : 0705.2205 . doi : 10.1109/LICS.2006.28.
  18. ^ Лёдинг, Кристоф; Пирогов, Антон. Детерминизация автоматов Бюхи: объединение подходов Сафры и Мюллера-Шуппа . ICALP 2019. arXiv : 1902.02139 .
  19. ^ Калуд, Кристиан; Джейн, Санджай; Хуссаинов, Бахадыр; Ли, Вэй; Стефан, Франк. Решение игр на четность за квазиполиномиальное время (PDF) . STOC 2017.
  20. ^ Shelah, Saharon (ноябрь 1975). "Монадическая теория порядка" (PDF) . Annals of Mathematics . 102 (3): 379– 419. arXiv : 2305.00968 . doi :10.2307/1971037. JSTOR  1971037. S2CID  122129926.
  21. ^ "Обобщение теоремы Шелаха–Ступа" (PDF) . Получено 14 ноября 2022 г.

Дополнительная ссылка: Weyer, Mark (2002). «Разрешимость S1S и S2S». Автоматы, логика и бесконечные игры . Конспект лекций по информатике. Том 2500. Springer. С.  207–230 . doi :10.1007/3-540-36387-4_12. ISBN
 978-3-540-00388-5.

Взято с "https://en.wikipedia.org/w/index.php?title=S2S_(математика)&oldid=1272891922"