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

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

Подход был инициирован Рохит Дживанлал Парих^[1] в 1971 году, а затем разработан Сэмюэл Р. Басс. ^[2] и ряд других логиков.

Теории

Теория Кука ${\displaystyle PV_{1}}$

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

Теории Бусса ${\displaystyle S_{2}^{i}}$

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

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

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

куда ${\displaystyle \phi \in \Sigma _{i}^{b}}$.

Теорема Басса о наблюдении

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

Теорема (Buss 1986)

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

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

Соответствие пропозициональным системам доказательства

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

Переписку ввел С. Кук.^[3]

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

Теорема (Повар 1975)

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

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

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

Смотрите также

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

Рекомендации

1. Рохит Дж. Парих. Существование и выполнимость в арифметике, Jour. Символическая логика 36 (1971) 494–508.
2. Басс, Сэмюэл. «Ограниченная арифметика». Библиополис, Неаполь, Италия, 1986 г..
3. Повар, Стивен (1975). «Возможные конструктивные доказательства и исчисление высказываний». Proc. 7-й ежегодный симпозиум ACM по теории вычислений. С. 83–97.
4. Крайичек, Ян; Пудлак, Павел; Такеути, Г. (1991). «Ограниченная арифметика и полиномиальная иерархия». Анналы чистой и прикладной логики. С. 143–153.
5. Пэрис, Джефф; Уилки, Алекс (1985). «Счетные задачи в ограниченной арифметике». Методы математической логики. 1130. С. 317–340.
6. Повар, Стивен; Нгуен, Фыонг (2010). «Логические основы сложности доказательства». Перспективы в логике. Кембридж: Издательство Кембриджского университета. Дои:10.1017 / CBO9780511676277. ISBN  978-0-521-51729-4. МИСТЕР  2589550. (проект от 2008 г. )

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

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

внешняя ссылка

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