Ограниченная арифметика

Ограниченная арифметика — собирательное название семейства слабых подтеорий арифметики Пеано . Такие теории обычно получаются, требуя, чтобы кванторы были ограничены в аксиоме индукции или эквивалентных постулатах (ограниченный квантор имеет форму ∀ x ≤ t или ∃ x ≤ t , где t — термин, не содержащий x ). Основная цель — охарактеризовать тот или иной класс вычислительной сложности в том смысле, что функция доказуемо тотальна тогда и только тогда, когда она принадлежит данному классу сложности. Кроме того, теории ограниченной арифметики представляют собой однородные аналоги стандартных систем пропозициональных доказательств, таких как система Фреге , и, в частности, полезны для построения доказательств полиномиального размера в этих системах. Характеристика стандартных классов сложности и соответствие системам пропозициональных доказательств позволяют интерпретировать теории ограниченной арифметики как формальные системы, охватывающие различные уровни допустимых рассуждений (см. Ниже).

Этот подход был инициирован Рохитом Дживанлалом Парихом. в 1971 году и позже разработан Сэмюэлем Р. Бассом . и ряд других логиков.

Теории

Эквациональная теория Кука

Стивен Кук представил эквациональную теорию $PV$ (для полиномиально проверяемых) формализация осуществимо конструктивных доказательств (соответственно рассуждения за полиномиальное время). Язык $PV$ состоит из функциональных символов для всех алгоритмов с полиномиальным временем, введенных индуктивно с использованием характеристики Кобэма функций с полиномиальным временем. Аксиомы и выводы теории вводятся одновременно с символами языка. Теория является эквациональной, т.е. ее утверждения утверждают только, что два члена равны. Популярное расширение $PV$ это теория $PV_{1}$, обычная теория первого порядка. Аксиомы $PV_{1}$ являются универсальными предложениями и содержат все уравнения, доказуемые в $PV$. Кроме того, $PV_{1}$ содержит аксиомы, заменяющие аксиомы индукции для открытых формул.

порядка

Сэмюэл Басс представил теории ограниченной арифметики первого порядка. $S_{2}^{i}$. $S_{2}^{i}$ являются теориями первого порядка с равенством в языке $L=\{0,S,+,\cdot ,\sharp ,|x|,\lfloor {\frac {x}{2}}\rfloor \}$, где функция $|x|$ предназначен для обозначения $\lceil \log(x+1)\rceil$ (количество цифр в двоичном представлении $x$) и $x\sharp y$ является $2^{|x|\cdot |y|}$. (Обратите внимание, что $|x\sharp x|\sim |x|^{2}$, то есть $\sharp$ позволяет выразить полиномиальные границы в битовой длине входных данных.) Ограниченные кванторы — это выражения вида $\exists x\leq t\dots :=\exists x(x\leq t\wedge \dots )$, $\forall x\leq t\dots :=\forall x(x\leq t\rightarrow \dots )$, где $t$ это термин, в котором не встречается $x$. Ограниченный квантор называется четко ограниченным, если $t$ имеет форму $|s|$ на срок $s$. Формула $\phi$ является резко ограниченным, если все кванторы в формуле четко ограничены. Иерархия $\Sigma _{i}^{b}$ и $\Pi _{i}^{b}$ формулы определяется индуктивно: $\Sigma _{0}^{b}=\Pi _{0}^{b}$ есть набор резко ограниченных формул. $\Sigma _{i+1}^{b}$ это закрытие $\Pi _{i}^{b}$ при ограниченных экзистенциальных и резко ограниченных кванторах всеобщности и $\Pi _{i+1}^{b}$ это закрытие $\Sigma _{i}^{b}$ при ограниченных всеобщих и резко ограниченных кванторах существования. Ограниченные формулы отражают иерархию полиномиального времени : для любого $i\geq 1$, класс $\Sigma _{i}^{P}$ совпадает с множеством натуральных чисел, определяемых формулой $\Sigma _{i}^{b}$ в $\mathbb {N}$ (стандартная модель арифметики) и двойственно $\Pi _{i}^{b}=\Pi _{i}^{P}(\mathbb {N} )$. В частности, $NP=\Sigma _{1}^{b}(\mathbb {N} )$.

Теория $S_{2}^{i}$ состоит из конечного списка открытых аксиом, обозначаемых BASIC, и схемы полиномиальной индукции.

$\phi (0)\wedge \forall x\leq a(\phi (\lfloor {\frac {x}{2}}\rfloor )\rightarrow \phi (x))\rightarrow \phi (a)$

где $\phi \in \Sigma _{i}^{b}$.

Басса

Басс (1986) доказал, что $\Sigma _{1}^{b}$ теоремы $S_{2}^{1}$ подтверждаются функциями с полиномиальным временем.

Теорема (Бусс, 1986)

Предположим, что $S_{2}^{1}\vdash \forall x\exists y\phi (x,y)$, с $\phi \in \Sigma _{1}^{b}$. Тогда существует $PV$-символ функции $f$ такой, что $PV\vdash \forall x\phi (x,f(x))$.

Более того, $S_{2}^{1}$ может $\Sigma _{1}^{b}$-определить все функции с полиномиальным временем. То есть, $\Sigma _{1}^{b}$-определяемые функции в $S_{2}^{1}$ являются в точности функциями, вычислимыми за полиномиальное время. Характеристика может быть обобщена на более высокие уровни полиномиальной иерархии.

Соответствие

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

Переписку представил С. Кук.

Неофициально, $\Pi _{1}^{b}$ заявление $\forall x\Phi (x)$ можно эквивалентно выразить в виде последовательности формул $\Phi _{n}(x):=\forall x(|x|=n\rightarrow \Phi (x))$. С $\Phi _{n}(x)$ является предикатом coNP, каждый $\Phi _{n}(x)$ в свою очередь может быть сформулировано как пропозициональная тавтология $||\phi ||^{n}$ (возможно, содержащие новые переменные, необходимые для кодирования вычисления предиката $\Phi _{n}$).

Теорема (Кук, 1975)

Предположим, что $S_{2}^{1}\vdash \forall x\Phi (x)$, где $\Phi \in \Pi _{1}^{b}$. Тогда тавтологии $||\phi ||^{n}$ полиномиального размера имеют расширенные доказательства Фреге . Более того, доказательства можно построить с помощью функции полиномиального времени и $PV$ доказывает этот факт.

Дальше, $S_{2}^{1}$ доказывает так называемый принцип отражения для расширенной системы Фреге, из которого следует, что расширенная система Фреге является самой слабой системой доказательства со свойством из приведенной выше теоремы: каждая система доказательства, удовлетворяющая импликации, моделирует расширенную систему Фреге.

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

См. также

• Сложность доказательства
• Вычислительная сложность
• Математическая логика
• Теория доказательств
• Классы сложности
• НП (сложность)
• КОНП

Дальнейшее чтение

• Басс, Сэмюэл , «Ограниченная арифметика», Библиополис, Неаполь, Италия, 1986.
• Кук, Стивен ; Нгуен, Фуонг (2010), Логические основы сложности доказательств , Перспективы логики, Кембридж: Издательство Кембриджского университета, doi : 10.1017/CBO9780511676277 , ISBN  978-0-521-51729-4 , МР   2589550 ( проект от 2008 г. )
• Крайичек, Ян (1995), Ограниченная арифметика, логика высказываний и теория сложности , Cambridge University Press
• Крайчек, Ян, Сложность доказательства , Cambridge University Press, 2019.
• Пудлак, Павел (2013), Логические основы математики и сложности вычислений, нежное введение , Springer

Внешние ссылки

• Список рассылки «Доказательство сложности».