プレスブルガー算術

プレスブルガー算術は、 1929 年にこの算術を提唱したモイジェシュ プレスブルガーにちなんで名付けられた、加算を伴う自然数の第一階理論です。プレスブルガー算術のシグネチャには、乗算演算を完全に省略し、加算演算と等式のみが含まれ、この理論は計算的に公理化可能であり、この公理には帰納法のスキーマが含まれます。

プレスブルガー算術は、加算と乗算の両方の演算を含むペアノ算術よりもはるかに弱い。ペアノ算術とは異なり、プレスブルガー算術は決定可能な理論である。つまり、プレスブルガー算術の言語で書かれた任意の文について、その文がプレスブルガー算術の公理から証明可能かどうかをアルゴリズム的に決定することができる。しかし、このアルゴリズムの漸近的な実行時の計算複雑性は、フィッシャーとラビン (1974) が示したように、少なくとも二重指数関数的である。

プレスブルガー算術の言語には、定数 0 と 1 および加算として解釈される 2 進関数 + が含まれます。

この言語では、プレスブルガー算術の公理は次の 普遍閉包です。

1. ¬(0 = x + 1)
2. x + 1 = y + 1 → x = y
3. x + 0 = x
4. x + ( y + 1 ) = ( x + y ) + 1 です
5. P ( x ) を、自由変数x (および場合によっては他の自由変数)を持つプレスブルガー算術言語の1 階式とします。次の式は公理です。
   ( P (0) ∧ ∀ x ( P ( x ) → P ( x + 1))) → ∀ y P ( y )。

(5)は帰納法の公理図式であり、無限個の公理を表す。これらは有限個の公理に置き換えることはできない。つまり、プレスブルガー算術は一階述語論理では有限に公理化できない。^[1]

プレスブルガー算術は、上記の公理の帰結をすべて含む等式を持つ一階の理論とみなすことができます。あるいは、意図された解釈において真である文の集合、つまり定数 0、1 を持つ非負整数の構造と非負整数の加算として定義することもできます。

プレスブルガー算術は、完全かつ決定可能であるように設計されています。したがって、割り切れるかどうかや素数かどうかなどの概念、またはより一般的には、変数の乗算につながる数の概念を形式化することはできません。ただし、割り切れるかどうかの個々のインスタンスを定式化することはできます。たとえば、「すべてのxに対して、 y が存在する : ( y + y = x ) ∨ ( y + y + 1 = x )」ということを証明します。これは、すべての数が偶数か奇数のいずれかであることを示しています。

プレスバーガー（1929）はプレスバーガー算術が次の通りであることを証明した。

• 一貫性: プレスブルガー算術には、その否定も演繹できるような公理から演繹できる命題は存在しない。
• 完全: プレスブルガー算術の言語における各ステートメントについては、公理からそれを演繹するか、またはその否定を演繹することが可能です。
• 決定可能:プレスブルガー算術における任意のステートメントが定理であるか非定理であるかを決定するアルゴリズムが存在します。「非定理」は証明できない式であり、一般に必ずしも否定が証明できる式ではありませんが、ここでのような完全な理論の場合には、両方の定義は同等であることに注意してください。

プレスブルガー算術の決定可能性は、算術合同性についての推論を補足した量指定子除去法を使って示すことができる。^{[2] [3] [4] [5] [6]}量指定子除去アルゴリズムを正当化するために使用される手順は、必ずしも帰納法の公理スキームを含まない計算可能な公理化を定義するために使用できる。^{[2] [7]}

対照的に、プレスブルガー算術に乗算を加えたペアノ算術は、決定可能ではない。これはチャーチが決定問題に対する否定的な答えとともに証明した通りである。ゲーデルの不完全性定理によれば、ペアノ算術は不完全であり、その無矛盾性は内部的に証明可能ではない（ただし、ゲンツェンの無矛盾性証明を参照）。

プレスブルガー算術の決定問題は、計算複雑性理論と計算における興味深い例です。プレスブルガー算術の文の長さをnとします。すると、Fischer & Rabin (1974) は、最悪の場合でも、一階述語論理における文の証明の長さは、ある定数c >0 に対して少なくとも であることを証明しました。したがって、プレスブルガー算術の決定アルゴリズムの実行時間は少なくとも指数関数的です。Fischer と Rabin はまた、任意の合理的な公理化 (彼らの論文で正確に定義されています) に対して、二重指数関数的な長さの証明を持つ長さnの定理が存在することを証明しました。Fischer と Rabin の研究は、入力が比較的大きな境界より小さい限り、プレスブルガー算術を使用して任意のアルゴリズムを正しく計算する式を定義できることも示唆しています。境界は増加できますが、新しい式を使用することによってのみ増加できます。一方、プレスブルガー算術の決定手順における三重指数上限は、オッペン (1978) によって証明されました。 ${\displaystyle 2^{2^{cn}}}$

より厳密な計算量上限は、Berman (1980) によって交代計算量クラスを使用して示されました。プレスブルガー算術 (PA) の真のステートメントの集合は、TimeAlternations (2 ^{2 n O(1)}、n) に対して完全であることが示されています。したがって、その計算量は、二重指数非決定性時間 (2-NEXP) と二重指数空間 (2-EXPSPACE) の間です。完全性は、多項式時間の多対一還元の下で得られます。(また、プレスブルガー算術は一般に PA と略されますが、数学全般において PA は通常ペアノ算術を意味します。)

よりきめ細かい結果を得るために、PA(i) を真の Σ _i PA ステートメントの集合とし、PA(i, j) を各量指定子ブロックが j 変数に制限された真の Σ _i PA ステートメントの集合とする。'<' は量指定子なしとみなされる。ここでは、制限された量指定子は量指定子としてカウントされる。PA
(1, j) は P に含まれるが、PA(1) は NP 完全である。^[8]
i > 0 かつ j > 2 の場合、PA(i + 1, j) はΣ _i ^P完全である。困難性の結果には、最後の量指定子ブロックで j>2 (j=1 ではなく) のみが必要である。i
>0 の場合、PA(i+1) はΣ _i ^EXP完全である。^[9]

短いプレスブルガー算術 ( ) は完全です (したがって に対して NP 完全です)。ここで、「短い」とは、整数定数が無制限であることを除いて、制限された (つまり ) 文のサイズを必要とします (ただし、2 進数でのビット数は入力サイズに対してカウントされます)。また、2 変数 PA (「短い」という制限なし) は NP 完全です。^[10]短い(したがって) PA は P に属し、これは固定次元のパラメトリック整数線形計画法に拡張されます。^[11]${\displaystyle \Sigma _{n}}$${\displaystyle n>2}$${\displaystyle \Sigma _{n-2}^{P}}$${\displaystyle n=3}$${\displaystyle O(1)}$${\displaystyle \Sigma _{2}}$${\displaystyle \Pi_{2}}$${\displaystyle \Sigma _{2}}$

プレスブルガー算術は決定可能であるため、プレスブルガー算術用の自動定理証明器が存在する。例えば、Coq証明支援システムにはプレスブルガー算術用の戦術 omega があり、Isabelle 証明支援システムには Nipkow (2010) による検証済みの量指定子除去手順が含まれている。理論の二重指数的複雑さにより、複雑な式に定理証明器を使用することは不可能であるが、この動作はネストされた量指定子がある場合にのみ発生する。Nelson & Oppen (1978) は、ネストされた量指定子のない拡張プレスブルガー算術に単体アルゴリズムを使用して、量指定子のないプレスブルガー算術式の例のいくつかを証明する自動定理証明器について説明している。より最近の理論を法とする充足可能性ソルバーは、量指定子のないプレスブルガー算術理論の断片を処理するために完全な整数計画法の手法を使用している。^[12]

プレスブルガー算術は、定数による乗算を含むように拡張できます。乗算は繰り返し加算であるためです。配列の添え字計算のほとんどは、決定可能な問題の領域に入ります。^[13]このアプローチは、1970年代後半のスタンフォードパスカル検証から始まり、2005年のマイクロソフトのSpec#システムまで、少なくとも5つの^{[引用が必要]}コンピュータプログラムの正しさの証明システムの基礎となっています。

プレスブルガー算術で定義可能な整数関係について、いくつかの特性が与えられました。簡単にするために、このセクションで考慮されるすべての関係は非負の整数に関するものです。

関係がプレスブルガー定義可能であるのは、それが半線型集合である場合に限ります。^[14]

単項整数関係、つまり非負整数の集合は、それが最終的に周期的である場合に限り、プレスブルガー定義可能です。つまり、となるすべての整数に対して、 となる閾値と正の周期が存在する場合、となる場合のみ、 となります。 ${\displaystyle R}$${\displaystyle t\in \mathbb {N} }$${\displaystyle p\in \mathbb {N} ^{>0}}$${\displaystyle n}$${\displaystyle |n|\geq t}$${\displaystyle n\in R}$${\displaystyle n+p\in R}$

コブハム・セミョーノフの定理によれば、関係がプレスブルガー定義可能であるのは、すべての に対して を基底とするビュッヒ算術で定義可能な場合のみである。^{[15] [16]}およびに対してを基底とするビュッヒ算術で定義可能であり、かつ乗法的に独立した整数である関係はプレスブルガー定義可能である。 ${\displaystyle k}$${\displaystyle k\geq 2}$${\displaystyle k}$${\displaystyle k'}$${\displaystyle k}$${\displaystyle k'}$

整数関係がプレスブルガー定義可能であるのは、加算と（つまり、プレスブルガー算術と の述語）を含む一階述語論理で定義可能な整数のすべての集合がプレスブルガー定義可能である場合のみです。^[17]同様に、プレスブルガー定義可能でない各関係に対して、加算とを含む一階述語論理式が存在し、その論理式は加算だけでは定義できない整数の集合を定義します。 ${\displaystyle R}$${\displaystyle R}$${\displaystyle R}$${\displaystyle R}$${\displaystyle R}$

プレスブルガー定義可能な関係は、ムクニクの定理による別の特徴付けが可能である。^[18]これは述べるのがより複雑であるが、前の2つの特徴付けの証明につながった。ムクニクの定理を述べる前に、いくつかの追加の定義を導入する必要がある。

を集合とすると、およびに対するの切断は次のように定義される 。${\displaystyle R\subseteq \mathbb {N} ^{d}}$${\displaystyle x_{i}=j}$${\displaystyle R}$${\displaystyle i<d}$${\displaystyle j\in \mathbb {N} }$

${\displaystyle \left\{(x_{0},\ldots ,x_{i-1},x_{i+1},\ldots ,x_{d-1})\in \mathbb {N} ^{d-1}\mid (x_{0},\ldots ,x_{i-1},j,x_{i+1},\ldots ,x_{d-1})\in R\right\}.}$

2つの集合と整数の-組が与えられたとき、となるすべての集合に対して となる場合、となるときかつ となる場合に限り、 において は-周期的であるといわれる。となるいくつかの集合 に対してとなる場合、 はにおいて-周期的であるといわれる。 ${\displaystyle R,S\subseteq \mathbb {N} ^{d}}$${\displaystyle d}$${\displaystyle (p_{0},\ldots,p_{d-1})\in \mathbb {N} ^{d}}$${\displaystyle R}$${\displaystyle (p_{0},\dots ,p_{d-1})}$${\displaystyle S}$${\displaystyle (x_{0},\dots ,x_{d-1})\in S}$${\displaystyle (x_{0}+p_{0},\dots ,x_{d-1}+p_{d-1})\in S,}$${\displaystyle (x_{0},\ldots ,x_{d-1})\in R}$${\displaystyle (x_{0}+p_{0},\dots ,x_{d-1}+p_{d-1})\in R}$${\displaystyle s\in \mathbb {N} }$${\displaystyle R}$${\displaystyle s}$${\displaystyle S}$${\displaystyle (p_{0},\ldots,p_{d-1})}$${\displaystyle (p_{0},\dots ,p_{d-1})\in \mathbb {Z} ^{d}}$

${\displaystyle \sum _{i=0}^{d-1}|p_{i}|<s.}$

最後に、let ${\displaystyle k,x_{0},\dots ,x_{d-1}\in \mathbb {N} }$

${\displaystyle C(k,(x_{0},\ldots ,x_{d-1}))=\left\{(x_{0}+c_{0},\dots ,x_{d-1}+c_{d-1})\mid 0\leq c_{i}}$

小さい方の角が である大きさの立方体を表します。 ${\displaystyle k}$${\displaystyle (x_{0},\dots ,x_{d-1})}$

直感的に、整数はシフトの長さを表し、整数は立方体のサイズであり、周期性の前の閾値です。この結果は、条件が ${\displaystyle s}$${\displaystyle k}$${\displaystyle t}$

${\displaystyle \sum _{i=0}^{d-1}x_{i}>t}$

はまたは に置き換えられます。 ${\displaystyle \min(x_{0},\ldots,x_{d-1})>t}$${\displaystyle \max(x_{0},\ldots,x_{d-1})>t}$

この特徴付けにより、いわゆる「プレスブルガー算術における定義可能性の定義可能基準」が生まれました。つまり、加算と-ary述語を含む一階式が存在し、それがプレスブルガー定義可能な関係によって解釈される場合にのみ成立するということです。また、ムクニクの定理により、自動シーケンスがプレスブルガー定義可能なセットを受け入れる かどうかが決定可能であることを証明することもできます。${\displaystyle d}$${\displaystyle R}$${\displaystyle R}$

• ロビンソン算術
• スコーレム算術

• Philipp Rümmer によるプレスブルガー算術の完全な定理証明器