Avgränsad aritmetik

Begränsad aritmetik är ett samlingsnamn för en familj av svaga subteorier av Peano-arithmetik . Sådana teorier erhålls typiskt genom att kräva att kvantifierare är begränsade i induktionsaxiom eller motsvarande postulat (en begränsad kvantifierare är av formen ∀ x ≤ t eller ∃ x ≤ t , där t är en term som inte innehåller x ). Huvudsyftet är att karakterisera en eller annan klass av beräkningskomplexitet i den meningen att en funktion bevisligen är total om och endast om den tillhör en given komplexitetsklass. Vidare presenterar teorier om begränsad aritmetik enhetliga motsvarigheter till standardpropositionella bevissystem såsom Frege-systemet och är särskilt användbara för att konstruera bevis i polynomstorlek i dessa system. Karakteriseringen av standardkomplexitetsklasser och överensstämmelse med propositionella bevissystem gör det möjligt att tolka teorier om begränsad aritmetik som formella system som fångar olika nivåer av genomförbara resonemang (se nedan).

Tillvägagångssättet initierades av Rohit Jivanlal Parikh 1971 och utvecklades senare av Samuel R. Buss . och ett antal andra logiker.

Teorier

Cooks teori $PV_{1}$

Stephen Cook introducerade en ekvationsteori $PV$ (för polynomiellt verifierbara) som formaliserade genomförbart konstruktiva bevis (resp. polynomtidsresonemang). Språket för $PV$ består av funktionssymboler för alla polynomtidsalgoritmer som introduceras induktivt med hjälp av Cobhams karakterisering av polynomtidsfunktioner Axiom och härledningar av teorin introduceras samtidigt med symbolerna från språket. Teorin är ekvationell, dvs dess uttalanden hävdar bara att två termer är lika. En populär förlängning av $PV$ är en teori ${\displaystyle PV_{1}} ,$ en vanlig första ordningens teori. Axiom för $PV_{1}$ är universella meningar och innehåller alla ekvationer som kan bevisas i $PV$ . Dessutom $PV_{1}$ axiom som ersätter induktionsaxiom för öppna formler

Buss teorier $S_{2}^{i}$

Samuel Buss introducerade första ordningens teorier för begränsad aritmetik $S_{2}^{i}$ . $S_{2}^{i}$ är första ordningens teorier med likhet i språket ${\displaystyle L=\{0,S,+,\cdot ,\sharp ,|x|,\lfloor {\frac {x}{2}}\rfloor \}} , där$ funktionen $|x|$ är avsedd att beteckna $\lceil \log(x+1)\rceil$ (antalet siffror i den binära representationen av $x$ ) och $x\sharp y$ är $2^{|x|\cdot |y|}$ . (Observera att $|x\sharp x|\sim |x|^{2}$ , dvs. $\sharp$ tillåter att uttrycka polynomgränser i bit- längden på inmatningen.) Begränsade kvantifierare är uttryck av formen $\exists x\leq t\dots :=\exists x(x\leq t \wedge \dots )$ , $\forall x\leq t\dots :=\forall x(x\leq t\högerpil \dots )$ , där $t$ är en term utan förekomst av $x$ . En avgränsad kvantifierare är skarpt begränsad om $t$ har formen av $|s|$ för en term $s$ . En formel $\phi$ är skarpt avgränsad om alla kvantifierare i formeln är skarpt avgränsade. Hierarkin för formlerna $\Sigma _{i}^{b}$ och $\Pi _{i}^{b}$ definieras induktivt: ${\ displaystyle \Sigma _{0}^{b}=\Pi _{0}^{b}}$ är uppsättningen av skarpt avgränsade formler. $\Sigma _{i+1}^{b}$ är stängningen av $\Pi _{i}^{b}$ under avgränsade existentiella och skarpt avgränsade universella kvantifierare , och $\Pi _{i+1}^{b}$ är stängningen av $\Sigma _{i}^{b}$ under avgränsad universell och skarpt avgränsad existentiella kvantifierare. Begränsade formler fångar polynom-tidshierarkin : för alla ${\displaystyle i\geq 1} sammanfaller$ klassen $\Sigma _{i}^{P}$ med uppsättningen naturliga tal som kan definieras av $\Sigma _{i}^{b}$ i $\mathbb {N}$ (standardmodellen för aritmetik) och dubbelt ${\ displaystyle \Pi _{i}^{b}=\Pi _{i}^{P}(\mathbb {N} )}$ . Speciellt $NP=\Sigma _{1}^{b}(\mathbb {N} )$ .

Teorin $S_{2}^{i}$ består av en finit lista med öppna axiom betecknade BASIC och polynominduktionsschemat

\phi (0)\wedge \forall x\leq a(\phi (\lfloor { \frac {x}{2}}\rgolv )\högerpil \phi (x))\högerpil \phi (a)

där $\phi \in \Sigma _{i}^{b}$ .

Buss vittnessats

Buss (1986) bevisade att $\Sigma _{1}^{b}$ satser för $S_{2}^{1}$ bevittnas av polynomtidsfunktioner.

Teorem (Buss 1986)

Antag att ${\displaystyle S_{2}^{1}\vdash \forall x\exists y\phi (x,y)} ,$ med $\phi \in \Sigma _{1}^{b}$ . Sedan finns det en $PV$ -funktionssymbol $f$ så att $PV\vdash \forall x\phi (x ,f(x))$ .

Dessutom kan $S_{2}^{1}$ $\Sigma _{1}^{b}$ -definiera alla polynomtidsfunktioner. Det vill säga, $\Sigma _{1}^{b}$ -definierbara funktioner i $S_{2}^{1}$ är just de funktioner som kan beräknas i polynomtid. Karakteriseringen kan generaliseras till högre nivåer i polynomhierarkin.

Överensstämmelse med propositionella bevissystem

Teorier om bunden aritmetik studeras ofta i samband med propositionella bevissystem. På samma sätt som Turing-maskiner är enhetliga motsvarigheter till olikformiga beräkningsmodeller som booleska kretsar , kan teorier om gränsad aritmetik ses som enhetliga motsvarigheter till propositionella bevissystem. Kopplingen är särskilt användbar för konstruktioner av korta propositionsbevis. Det är ofta lättare att bevisa en sats i en teori om gränsad aritmetik och översätta första ordningens bevis till en sekvens av korta bevis i ett satsbevissystem än att designa korta satsbevis direkt i satsbevissystemet.

Korrespondensen introducerades av S. Cook.

Informellt kan en ${\displaystyle \Pi _{1}^{b}}-$ sats $\forall x\Phi (x)$ uttryckas ekvivalent som en sekvens av formler $\Phi _{n}(x):=\forall x(|x|=n\högerpil \Phi (x))$ . Eftersom $\Phi _{n}(x)$ är ett coNP-predikat kan varje $\Phi _{n}(x)$ i sin tur formuleras som en propositionell tautologi $||\phi ||^{n}$ (innehåller eventuellt nya variabler som behövs för att koda beräkningen av predikatet $\Phi _{n}$ ).

Teorem (Cook 1975)

Antag att $S_{2}^{1}\vdash \forall x\Phi (x)$ , där $\Phi \in \Pi _{1}^{b}$ . Sedan tautologier ${\displaystyle ||\phi ||^{n}} har$ utökade Frege- bevis i polynomstorlek . Dessutom är bevisen konstruerbara med en polynom-tidsfunktion och $PV$ bevisar detta faktum.

Vidare bevisar $S_{2}^{1}$ den så kallade reflektionsprincipen för Extended Frege-systemet, vilket innebär att Extended Frege-systemet är det svagaste bevissystemet med egenskapen från satsen ovan: varje bevissystem att uppfylla implikationen simulerar Extended Frege.

En alternativ översättning mellan andra ordningens påståenden och propositionella formler som ges av Jeff Paris och Alex Wilkie (1985) har varit mer praktiskt för att fånga subsystem av Extended Frege som Frege eller Frege med konstant djup.

Se även

Vidare läsning

Buss, Samuel , "Bounded Arithmetic", Bibliopolis, Neapel, Italien, 1986.
Cook, Stephen ; Nguyen, Phuong (2010), Logical Foundations of Proof Complexity , Perspectives in Logic, Cambridge: Cambridge University Press, : 10.1017 /CBO9780511676277 , ISBN 978-0-521-51729-4 , 89 MR 5205 doi ( draft 89 MR 5205
Krajíček, Jan (1995), Begränsad aritmetik, propositionell logik och komplexitetsteori , Cambridge University Press
Krajíček, Jan, Proof Complexity , Cambridge University Press, 2019.
Pudlák, Pavel (2013), Logical Foundations of Mathematics and Computational Complexity, en mild introduktion , Springer

externa länkar

Bevis komplexitet e-postlista.