Ograniczona arytmetyka

Arytmetyka ograniczona to zbiorcza nazwa rodziny słabych podteorii arytmetyki Peano . Takie teorie są zwykle uzyskiwane poprzez wymaganie, aby kwantyfikatory były ograniczone aksjomatem indukcyjnym lub równoważnymi postulatami (kwantyfikator ograniczony ma postać ∀ x ≤ t lub ∃ x ≤ t , gdzie t jest terminem niezawierającym x ). Głównym celem jest scharakteryzowanie jednej lub drugiej klasy złożoności obliczeniowej w tym sensie, że funkcja jest dająca się udowodnić całkowita wtedy i tylko wtedy, gdy należy do danej klasy złożoności. Co więcej, teorie ograniczonej arytmetyki stanowią jednolite odpowiedniki standardowych systemów dowodowych, takich jak system Fregego, i są w szczególności przydatne do konstruowania dowodów wielkości wielomianów w tych systemach. Charakterystyka standardowych klas złożoności i zgodności ze zdaniowymi systemami dowodowymi pozwala interpretować teorie ograniczonej arytmetyki jako systemy formalne, które wychwytują różne poziomy wykonalnego rozumowania (patrz poniżej).

Podejście to zostało zapoczątkowane przez Rohita Jivanlala Parikha w 1971 roku, a następnie rozwinięte przez Samuela R. Bussa . i wielu innych logików.

teorie

teoria Cooka ${\ Displaystyle PV_ {1}}$

Stephen Cook przedstawił teorię równań (od wielomianu weryfikowalnego ), formalizując wykonalnie konstruktywne dowody (odp. Rozumowanie w czasie $)$ Język składa się z symboli funkcyjnych dla wszystkich algorytmów czasu wielomianowego wprowadzonych indukcyjnie przy użyciu charakterystyki funkcji czasu $Cobhama$ Aksjomaty i wyprowadzenia teorii są wprowadzane równocześnie z symbolami z języka. Teoria jest równaniowa, tzn. jej twierdzenia stwierdzają tylko, że dwa wyrazy są równe. Popularnym rozszerzeniem $\ displaystyle PV}$ ${$ teoria , teoria pierwszego rzędu Aksjomaty są zdaniami uniwersalnymi i zawierają wszystkie równania $displaystyle$ które można udowodnić w $PV}$ . Ponadto $otwartych$ aksjomaty indukcyjne dla formuł

Teorie Bussa ${\ Displaystyle S_ {2} ^ {i}}$

Samuel Buss przedstawił teorie pierwszego rzędu arytmetyki ograniczonej ${\ displaystyle S_ {2} ^ {i}}$ . ${\ Displaystyle S_ {2} ^ {i}}$ są teoriami pierwszego rzędu z równością w języku $_$ _ ${\ Displaystyle | x |}$ ma na celu wyznaczenie $\ Displaystyle \ lceil \ log (x + 1) \ rceil}$ w binarnej reprezentacji $x {$ ) i ${\ displaystyle x \ ostry y}$ wynosi ${\ Displaystyle 2 ^ {| x | \ cdot | y |}}$ . (Zauważ, że ${\ Displaystyle | x \ ostry x | \ sim | x | ^ {2}}$ $,$ tj pozwala wyrazić granice wielomianu w bit- ${\ Displaystyle \ istnieje x \ równoważnik t \ kropki: = \ istnieje x (x \ równoważnik$ … , ${\ Displaystyle \ forall x \ równoważnik t \ kropki: = \ forall x (x \ równoważnik t \ strzałka w prawo \ kropki)}$ , gdzie jest terminem bez wystąpienia ${\$ $x}$ . Ograniczony kwantyfikator jest ostro ograniczony, $postać$ ma ${\ displaystyle | s |}$ na termin ${\ displaystyle s}$ . Formuła $ostro ograniczona$ jeśli wszystkie kwantyfikatory we wzorze są ostro ograniczone. Hierarchia formuł $\ Displaystyle \ Pi$ $i} ^ {b}} jest$ ${\ displaystyle \Sigma _{0}^{b}=\Pi _{0}^{b}}$ zdefiniowana indukcyjnie: to zbiór ostro ograniczonych formuł. ${\ Displaystyle \ Sigma _ {i + 1} ^ {b}}$ jest zamknięciem pod ograniczonymi kwantyfikatorami egzystencjalnymi i ostro ograniczonymi uniwersalnymi kwantyfikatorami ${\ Displaystyle \ Pi _ {i} ^ {b}}$ Π ${\ Displaystyle \ Pi _ {i + 1} ^ {b}}$ zamknięciem pod ograniczonym uniwersalnym i ostro ograniczonym ${\ Displaystyle \ Sigma _ {i} ^ {b}}$ kwantyfikatory egzystencjalne. Formuły ograniczone przechwytują hierarchię czasu wielomianowego $:$ dla dowolnego klasa pokrywa się ze zbiorem definiowalnych liczb naturalnych $P}}$ przez $}}$ ${\ styl wyświetlania \Pi _{i}^{b}=\Pi _{i}^{P}(\mathbb {N} )}$ $b$ w (standardowy model arytmetyki) i podwójnie . W szczególności ${\ Displaystyle NP = \ Sigma _ {1} ^ {b} (\ mathbb {N})}$ .

Teoria składa się ze skończonej listy otwartych aksjomatów oznaczonych jako BASIC i schematu indukcji wielomianowej ${\ displaystyle S_ {2} ^ {i}}$

{\ Displaystyle \ phi (0) \ klin \ dla wszystkich x \ równoważnik a (\ phi (\ lfloor {{ \frac {x}{2}}\rfloor )\rightarrow \phi (x)}\rightarrow \phi (a)}

gdzie ${\ Displaystyle \ phi \ in \ Sigma _ {i} ^ {b}}$ .

Twierdzenie Bussa o świadkach

$,$ że twierdzenia ${\ displaystyle S_ {2} ^ {1}}$ obserwowane przez czasu wielomianowego

Twierdzenie (Buss 1986)

Załóżmy, że ${\ Displaystyle S_ {2} ^ {1} \ vdash \ forall x \ istnieje y \ phi (x, y)}$ , z ${\ Displaystyle \ phi \ in \ Sigma _ {1} ^ {b}}$ . Wtedy istnieje symbol funkcji $taki$ $phi ($ , $Displaystyle$ .

$Co$ więcej można $_$ wszystkie $są$ to, że $obliczalnymi$ dokładnie w czasie wielomianowym Charakterystykę można uogólnić na wyższe poziomy hierarchii wielomianów.

Korespondencja ze zdaniowymi systemami dowodowymi

Teorie ograniczonej arytmetyki są często badane w powiązaniu z systemami dowodowymi zdań. Podobnie jak maszyny Turinga są jednolitymi odpowiednikami niejednorodnych modeli obliczeń, takich jak obwody boolowskie , teorie ograniczonej arytmetyki można postrzegać jako jednolite odpowiedniki systemów dowodowych zdań. Połączenie jest szczególnie przydatne przy konstrukcjach krótkich dowodów zdaniowych. Często łatwiej jest udowodnić twierdzenie w teorii arytmetyki ograniczonej i przetłumaczyć dowód pierwszego rzędu na sekwencję krótkich dowodów w systemie dowodowym zdaniowym, niż zaprojektować krótkie dowody zdaniowe bezpośrednio w systemie dowodowym zdaniowym.

Korespondencję przedstawił S. Cook.

Nieformalnie stwierdzenie $\ Displaystyle \ Pi$ jako sekwencję formuł ${\ Displaystyle \ Phi _ {n} (x): = \ forall x (| x | = n \ strzałka w prawo \ Phi (x)) }$ ${1} ^ {b}$ . Ponieważ $Displaystyle \ Phi _ {n} (x$ predykatem coNP, każdy $można z kolei$ jako tautologia zdaniowa ${\ displaystyle ||\ phi ||^ {n}}$ (prawdopodobnie zawierające nowe zmienne potrzebne do zakodowania obliczenia predykatu ${\ displaystyle \ Phi _ {n}})$ .

Twierdzenie (kucharz 1975)

Załóżmy, że ${\ Displaystyle S_ {2} ^ {1} \ vdash \ forall x \ Phi (x)}$ , gdzie ${\ Displaystyle \ Phi \ in \ Pi _{1}^{b}}$ . Następnie tautologie ${\ displaystyle ||\ phi ||^ {n}}$ mają wielomianowe dowody Extended Frege . Co więcej, dowody można skonstruować za pomocą funkcji czasu wielomianowego i $fakt$ .

Co więcej, $udowadnia$ tak zwaną zasadę odbicia dla systemu Extended Frege, z której wynika, że system Extended Frege jest najsłabszym systemem dowodowym z właściwością z powyższego twierdzenia: spełnienie implikacji symuluje Extended Frege.

Alternatywne tłumaczenie zdań drugiego rzędu na formuły zdaniowe podane przez Jeffa Parisa i Alexa Wilkie'go (1985) było bardziej praktyczne w przypadku uchwycenia podsystemów Extended Frege, takich jak Frege lub Frege o stałej głębokości.

Zobacz też

Dalsza lektura

Buss, Samuel , „Bounded Arithmetic”, Bibliopolis, Neapol, Włochy, 1986.
Gotuj, Stefan ; Nguyen, Phuong (2010), Logiczne podstawy złożoności dowodu , Perspectives in Logic , Cambridge: Cambridge University Press, doi : 10.1017/CBO9780511676277 , ISBN 978-0-521-51729-4 , MR 2589550 ( wersja robocza z 2008 r .)
Krajíček, Jan (1995), ograniczona arytmetyka, logika zdań i teoria złożoności , Cambridge University Press
Krajíček, Jan, Złożoność dowodu , Cambridge University Press, 2019.
Pudlák, Pavel (2013), Logiczne podstawy matematyki i złożoności obliczeniowej, delikatne wprowadzenie , Springer

Linki zewnętrzne

Lista mailingowa dowodu złożoności.