Спектр предложения

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

Определение

Пусть ψ — предложение логики первого порядка . Спектр — это ψ n набор натуральных чисел таких , что существует конечная модель ψ с n элементами.

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

Примеры

• Спектр формулы первого порядка

$\exists z,o~\forall a,b,c~\exists d,e$

$a+z=a=z+a~\land ~a\cdot z=z=z\cdot a~\land ~a+d=z$

$\land ~a+b=b+a~\land ~a\cdot (b+c)=a\cdot b+a\cdot c~\land ~(a+b)+c=a+(b+c)$

$\land ~a\cdot o=a=o\cdot a~\land ~a\cdot e=o~\land ~(a\cdot b)\cdot c=a\cdot (b\cdot c)$

является $\{p^{n}\mid p{\text{ prime}},n\in \mathbb {N} \}$, набор степеней простого числа . Действительно, с $z$ для $0$ и $o$ для $1$это предложение описывает набор полей ; мощность — это степень конечного поля простого числа.

• Спектр формулы монадической логики второго порядка $\exists S,T~\forall x~\left\{x\in S\iff x\not \in T\land ~f(f(x))=x\land ~x\in S\iff f(x)\in T\right\}$ представляет собой набор четных чисел. Действительно, $f$ является биекцией между $S$ и $T$, и $S$ и $T$ являются частью Вселенной. Следовательно, мощность Вселенной четная.
• Множество конечных и коконечных множеств представляет собой множество спектров логики первого порядка с отношением следования.
• Множество предельно периодических множеств — это множество спектров монадической логики второго порядка с унарной функцией. Это также набор спектров монадической логики второго порядка с функцией-преемником.

сложность

Теорема Феджина — это результат дескриптивной теории сложности , которая утверждает, что набор всех свойств, выражаемых в экзистенциальной логике второго порядка , в точности соответствует классу сложности NP . Это примечательно, поскольку это характеристика класса NP, которая не использует такую ​​модель вычислений, как машина Тьюринга . Теорему доказал Рональд Феджин в 1974 году (строго, в 1973 году в своей докторской диссертации).

Как следствие, Джонс и Селман показали, что множество является спектром тогда и только тогда, когда оно принадлежит классу сложности NEXP .

Одно из направлений доказательства — показать, что для любой формулы первого порядка $\varphi$, проблема определения того, существует ли модель формулы мощности n, эквивалентна проблеме удовлетворения формулы полинома размера от n , которая находится в NP(n) и, следовательно, в NEXP входных данных для задачи ( число n в двоичной форме, которое представляет собой строку размера log( n )).

Это делается путем замены каждого квантора существования в $\varphi$ с дизъюнкцией по всем элементам модели и заменой каждого универсальности конъюнкцией квантора по всем элементам модели. Теперь каждый предикат относится к элементам модели, и, наконец, каждое появление предиката к конкретным элементам заменяется новой пропозициональной переменной. Равенства заменяются их истинностными значениями в соответствии с их назначениями.

Например:

$\forall {x}\forall {y}\left(P(x)\wedge P(y)\right)\rightarrow (x=y)$

Для модели мощности 2 (т.е. n = 2) заменяется на

${\big (}\left(P(a_{1})\wedge P(a_{1})\right)\rightarrow (a_{1}=a_{1}){\big )}\wedge {\big (}\left(P(a_{1})\wedge P(a_{2})\right)\rightarrow (a_{1}=a_{2}){\big )}\wedge {\big (}\left(P(a_{2})\wedge P(a_{1})\right)\rightarrow (a_{2}=a_{1}){\big )}\wedge {\big (}\left(P(a_{2})\wedge P(a_{2})\right)\rightarrow (a_{2}=a_{2}){\big )}$

Который затем заменяется на ${\big (}\left(p_{1}\wedge p_{1}\right)\rightarrow \top {\big )}\wedge {\big (}\left(p_{1}\wedge p_{2}\right)\rightarrow \bot {\big )}\wedge {\big (}\left(p_{2}\wedge p_{1}\right)\rightarrow \bot {\big )}\wedge {\big (}\left(p_{2}\wedge p_{2}\right)\rightarrow \top {\big )}$

где $\top$ это истина, $\bot$ является ложью, и $p_{1}$, $p_{2}$ являются пропозициональными переменными.В данном конкретном случае последняя формула эквивалентна $\neg (p_{1}\wedge p_{2})$, что является выполнимым.

Другое направление доказательства — показать, что для каждого набора двоичных строк, принимаемого недетерминированной машиной Тьюринга, работающей за экспоненциальное время ( $2^{cx}$ для входной длины x) существует формула первого порядка $\varphi$ такой, что набор чисел, представленный этими двоичными строками, представляет собой спектр $\varphi$.

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

Другая недвижимость

Множество спектров теории замкнуто относительно объединения , пересечения , сложения и умножения. В полной общности неизвестно, замкнуто ли множество спектров теории дополнением; это так называемая проблема Ассера. Согласно результату Джонса и Селмана, это эквивалентно проблеме: NEXPTIME = co-NEXPTIME; то есть, закрыт ли NEXPTIME при дополнении.

См. также

• Спектр теории

Ссылки

• Феджин, Рональд (1974). «Обобщенные спектры первого порядка и наборы, распознаваемые за полиномиальное время» (PDF) . В Карпе, Ричард М. (ред.). Сложность вычислений . Учеб. Сып. Приложение. Математика. Материалы SIAM-AMS. Том. 7. С. 27–41. Збл   0303.68035 .
• Гредель, Эрих; Колайтис, Фокион Г.; Либкин Леонид ; Мартен, Маркс; Спенсер, Джоэл ; Варди, Моше Ю .; Венема, Иде; Вайнштейн, Скотт (2007). Теория конечных моделей и ее приложения . Тексты по теоретической информатике. Серия EATCS. Берлин: Springer-Verlag . дои : 10.1007/3-540-68804-8 . ISBN  978-3-540-00428-8 . Збл   1133.03001 .
• Иммерман, Нил (1999). Описательная сложность . Тексты для аспирантов по информатике. Нью-Йорк: Springer-Verlag. стр. 113–119 . ISBN  0-387-98600-6 . Збл   0918.68031 .
• Дюран, Арно; Джонс, Нил; Марковский, Иоганн; Подробнее, Малика (2012). «Пятьдесят лет проблемы спектра: обзор и новые результаты». Бюллетень символической логики . 18 (4): 505–553. arXiv : 0907.5495 . Бибкод : 2009arXiv0907.5495D . дои : 10.2178/bsl.1804020 . S2CID   9507429 .