限定算術

有界算術とは、ペアノ算術の弱い部分理論の集合の総称である。このような理論は、通常、帰納法の公理または同等の公準において量化子が有界であることを要求することによって得られる（有界量化子は、∀ x  ≤ tまたは ∃ x ≤ tの形式であり、tはxを含まない項である）。主な目的は、関数が証明可能全関数であるのは、それが特定の複雑性クラスに属する場合に限るという意味で、計算複雑性のクラスを特徴づけることである。さらに、有界算術の理論は、フレーゲ体系などの標準的な命題証明体系と統一的な対応関係を持ち、特にこれらの体系において多項式サイズの証明を構築する際に有用である。標準的な複雑性クラスの特徴づけと命題証明体系との対応関係により、有界算術の理論を、実行可能な推論のさまざまなレベルを捉える形式体系として解釈することができる（下記参照）。    

このアプローチは1971年にロヒット・ジバンラル・パリク^{[ 1 ]}によって開始され 、後にサミュエル・R・バス[ ^{2 ]や}他の多くの論理学者によって発展させられました。

Buss (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}}$これらはまさに多項式時間で計算可能な関数である。この特徴付けは、多項式階層のより高次のレベルにも一般化できる。

限定算術の理論は、命題論理の証明体系と関連付けて研究されることが多い。チューリングマシンがブール回路のような非均一な計算モデルの均一等価物であるのと同様に、限定算術の理論は命題論理の証明体系の均一等価物と見なすことができる。この関連性は、短い命題論理の証明を構成する際に特に有用である。限定算術の理論で定理を証明し、その一階述語論理の証明を命題論理の証明体系における一連の短い証明に変換する方が、命題論理の証明体系で直接短い命題論理の証明を設計するよりも容易な場合が多い。

この書簡はS.クックによって紹介された。^{[ 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）によって与えられた、2階述語と命題論理式の間の別の翻訳は、フレーゲや定数深さフレーゲなどの拡張フレーゲのサブシステムを捉えるのに実用的であった。^{[ 5 ] [ 6 ]}

• 証明の複雑さ
• 計算複雑性
• 数理論理学
• 証明論
• 複雑性クラス
• NP（複雑性）
• coNP

• Buss, Samuel、『限定算術』、Bibliopolis、ナポリ、イタリア、1986年。
• Cook, Stephen ; Nguyen, Phuong (2010), Logical Foundations of Proof Complexity , Perspectives in Logic, Cambridge: Cambridge University Press, doi : 10.1017/CBO9780511676277 , ISBN 978-0-521-51729-4MR 2589550​ （2008年の草稿）
• Krajíček, Jan (1995), 『限定算術、命題論理、および複雑性理論』、ケンブリッジ大学出版局
• Krajíček、Jan、『Proof Complexity』、ケンブリッジ大学出版局、2019 年。
• プドラック、パベル（2013）、『数学と計算複雑性の論理的基礎：入門』、シュプリンガー
• ハジェク、ペトル；プドラク、パヴェル（2016）。一階算術のメタ数学。論理学の展望。ケンブリッジ大学出版局。ISBN 978-1-107-16841-1OCLC 982287942​​ 

• 証明の複雑性に関するメーリングリスト。