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

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

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

Теории

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

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

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

Сэмюэл Басс представил теории ограниченной арифметики первого порядка . ^[2] являются теориями первого порядка с равенством на языке , где функция предназначена для обозначения (количество цифр в двоичном представлении ) и равно . (Обратите внимание , что , т.е. позволяет выразить полиномиальные границы в битовой длины входа.) Bounded квантификаторы выражения вида , где это термин , без возникновения . Ограниченный квантор строго ограничен, если имеет вид для члена . Формула${\ displaystyle S_ {2} ^ {i}}$ ${\ displaystyle S_ {2} ^ {i}}$${\ Displaystyle L = \ {0, S, +, \ cdot, \ sharp, | x |, \ lfloor {\ frac {x} {2}} \ rfloor \}}$${\ displaystyle | x |}$${\ Displaystyle \ lceil \ журнал (х + 1) \ rceil}$${\ displaystyle x}$${\ Displaystyle х \ диез у}$${\ Displaystyle 2 ^ {| х | \ cdot | у |}}$${\ displaystyle | x \ sharp x | \ sim | x | ^ {2}}$${\ displaystyle \ sharp}$${\ Displaystyle \ существует х \ Leq T \ точек: = \ существует х (х \ Leq т \ клин \ точек)}$${\ 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}$строго ограничен, если все кванторы в формуле строго ограничены. Иерархия и формулы определяются индуктивно: есть множество резко ограниченные формулы. является замыканием недостаточно универсальных кванторов существования и строго ограниченных универсальных кванторов и является замыканием ограниченных универсальных и строго ограниченных кванторов существования. Ограниченные формулы отражают иерархию полиномиального времени : для любого класс совпадает с множеством натуральных чисел, определяемых in (стандартная модель арифметики) и двойственно . В частности, .${\ displaystyle \ Sigma _ {я} ^ {b}}$${\ displaystyle \ Pi _ {я} ^ {b}}$${\ displaystyle \ Sigma _ {0} ^ {b} = \ Pi _ {0} ^ {b}}$${\ displaystyle \ Sigma _ {я + 1} ^ {b}}$${\ displaystyle \ Pi _ {я} ^ {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} )}$

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

${\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) доказал, что теоремы о полиномиальных функциях времени засвидетельствованы . ^[2]${\displaystyle \Sigma _{1}^{b}}$${\displaystyle S_{2}^{1}}$

Теорема (Басс, 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]

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

использованная литература

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

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

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

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