スコーレム算術

数理論理学において、スコーレム算術は乗法を含む自然数の第一階理論であり、トラルフ・スコーレムにちなんで名付けられました。スコーレム算術の記号は乗算と等号のみで構成され、加算は完全に省略されています。

スコーレム算術は、加算と乗算の両方の演算を含むペアノ算術よりも弱い。^[1]ペアノ算術とは異なり、スコーレム算術は決定可能理論である。これは、スコーレム算術の言語で書かれた任意の文について、その文がスコーレム算術の公理から証明可能かどうかを効果的に決定できることを意味する。この決定問題の漸近的な実行時計算複雑度は、3倍の指数関数的である。^[2]

公理

以下の略語を定義する

• a | b  := ∃ n .( an = b )
• 1( e ) := ∀ n .( ne = n )
• 素数( p ) := ¬素数( p ) ∧ ∀ a .( a | p → (素数( a ) ∨ a = p ))
• PrimePower( p , P ) := Prime( p ) ∧ p | P ∧ چ q .(Prime( q ) ∧ ¬( q = p ) → ¬( q | P ))
• InvAdicAbs( p , n , P ) := PrimePower( p , P ) ∧ P | n ∧ ∀Q.((PrimePower( p , Q ) ∧ Q | n ) → Q | P ) [ Pはpをnで割る最大の累乗である]
• AdicAbsDiff _n ( p , a , b ) := Prime( p ) ∧ p | ab ∧ ∃ P .∃ Q .(InvAdicAbs( p , a , P ) ∧ InvAdicAbs( p , b , Q ) ∧ Q = p ⁿ P ) が、各整数n > 0 に対して成り立ちます。[ p をbで割る最大の累乗は、 pをaで割る最大の累乗のp ⁿ倍です。]

スコーレム算術の公理は以下の通りである: ^[3]

1. ∀ a . ∀ b . ( ab = ba )
2. ∀ a . ∀ b . ∀ c . (( ab ) c = a ( bc ))
3. ∃ e .One( e )
4. ∀ a . ∀ b .(One( ab ) → One( a ) ∨ One( b ))
5. ∀ a . ∀ b . ∀ c . ( ac = bc → a = b )
6. ∀ a . ∀ b . ( a ⁿ = b ⁿ → a = b ) （各整数n > 0について）
7. ∀ x .∃ a .∃ r .( x = ar ⁿ ∧ ∀ b .∀ s .( x = bs ⁿ → a | b )) （各整数n > 0について）
8. ∀ a .∃ p .(Prime( p ) ∧ ¬( p | a )) [素数の無限性]
9. ∀ p . ∀ P . ∀ Q . ( (PrimePower( p , P ) ∧ PrimePower( p , Q )) → ( P | Q ∨ Q | P ))
10. ∀ p .∀ n .(Prime( p ) → ∃ P .InvAdicAbs( p , n , P ))
11. ∀ n . . ...​​​​​​​​​​​​​​​​​​​​​​
12. ∀ p .∀ n .∀ m .(Prime( p ) → ∃ P .∃ Q .(InvAdicAbs( p , n , P ) ∧ InvAdicAbs( p , m , Q ) ∧ InvAdicAbs( p , nm , PQ ))) [ p進数の絶対値は乗法です]
13. ∀ a .∀ b .(∀ p .(Prime( p ) → ∃ P .∃ Q .(InvAdicAbs( p , a , P ) ∧ InvAdicAbs( p , b , Q ) ∧ P | Q )) → a | b ) [すべての素数pに対して、 aのp進値がbの値より小さい場合、a | b ]
14. ∀ a . . ... . . . . . . . . . . . .​​​​​​​​​​​​​​​​​​​​​​​​
15. ∀ a .∃ b .∀ p .(Prime( p ) → (∃ P .(InvAdicAbs( p , a , P ) ∧ InvAdicAbs( p , b , pP ))) ∧ ( p | b → p | a ))) [ aの素因数分解における各指数を1 ずつ増やす]
16. ∀ a . . ...​​​​​​_​​​​​​​​​​​​​​​​​​_​​​​​​​​​​​​​​​​​^​​​​​​

表現力

正の整数の等式と乗算を用いた一階述語論理は、関係式を表現できます 。この関係式と等式を用いて、正の整数に関する次の関係式を定義できます ${\displaystyle c=a\cdot b}$

• 割り切れるかどうか：${\displaystyle b|c\ \Leftrightarrow \ \exists a.c=a\cdot b}$
• 最大公約数：${\displaystyle d=\gcd(a,b)\ \Leftrightarrow \ d|a\land d|b\land \forall d'.(d'|a\land d'|b)\Rightarrow d'|d}$
• 最小公倍数：${\displaystyle m=\mathrm {lcm} (a,b)\ \Leftrightarrow \ a|m\land b|m\land \forall m'.(a|m'\land b|m')\Rightarrow m|m'}$
• 定数：${\displaystyle 1}$ ${\displaystyle \forall a.1|a}$
• 素数:${\displaystyle \mathrm {prime} (p)\ \Leftrightarrow \ p\neq 1\land \forall a.a|p\Rightarrow (a=1\lor a=p)}$
• 数は素数の積です（固定値の場合）:${\displaystyle b}$ ${\displaystyle k}$ ${\displaystyle k}$ ${\displaystyle \exists a_{1},...a_{k}.\ \mathrm {prime} (a_{1})\land \ldots \land \mathrm {prime} (a_{k})\land b=a_{1}\cdot \ldots \cdot a_{k}}$
• 数は素数の累乗です:${\displaystyle b}$ ${\displaystyle \mathrm {ppower} (b)\ \Leftrightarrow \ \exists p.\mathrm {prime} (p)\land \forall a.(a\neq 1\land a|b)\Rightarrow p|a}$
• 数は正確に素数の累乗の積です:${\displaystyle b}$ ${\displaystyle k}$ ${\displaystyle \exists a_{1},...a_{k}.\ \mathrm {ppower} (a_{1})\land \ldots \land \mathrm {ppower} (a_{k})\land b=a_{1}\cdot \ldots \cdot a_{k}}$

決定可能性の考え方

スコーレム算術の式の真理値は、素因数分解を構成する非負整数の列の真理値に還元することができ、乗算は列の点ごとの加算となる。したがって、決定可能性は、量指定子消去を用いて示せるフェファーマン・ヴォート定理から導かれる。これを別の言い方で述べると、正整数の第一階理論は、多重集合和演算を伴う非負整数の有限多重集合の第一階理論と同型であり、その決定可能性は元論の決定可能性に還元される。

より詳しくは、算術の基本定理によれば、正の整数は素数の累乗として表すことができます。 ${\displaystyle a>1}$

${\displaystyle a=p_{1}^{a_{1}}p_{2}^{a_{2}}\cdots }$

素数が因数として現れない場合、その指数は0と定義されます。したがって、無限数列 において、指数が0でないものは有限個しかありません。このような非負整数列を と表記します。 ${\displaystyle p_{k}}$ ${\displaystyle a_{k}}$ ${\displaystyle a_{1},a_{2},\ldots }$ ${\displaystyle N^{*}}$

ここで別の正の数の分解を考えてみましょう。

${\displaystyle b=p_{1}^{b_{1}}p_{2}^{b_{2}}\cdots }$

乗算は指数の各点の加算に対応します。 ${\displaystyle ab}$

${\displaystyle ab=p_{1}^{a_{1}+b_{1}}p_{2}^{a_{2}+b_{2}}\cdots }$

シーケンス上の対応する点ごとの加算を次のように定義します。

${\displaystyle (a_{1},a_{2},\ldots ){\bar {+}}(b_{1},b_{2},\ldots )=(a_{1}+b_{1},a_{2}+b_{2},\ldots )}$

したがって、乗算を伴う正の整数の構造と、有限個の要素のみがゼロでない非負整数のシーケンスの点ごとの加算の構造との間には同型性があります。 ${\displaystyle (N,\cdot )}$ ${\displaystyle (N^{*},{\bar {+}})}$

一階述語論理のフェファーマン・ヴォート定理から、列とその点ごとの加法に関する一階述語論理式の真理値は、アルゴリズム的に、加法を伴う列の元の理論における式の真理値、つまりこの場合プレスブルガー算術に帰着する。プレスブルガー算術は決定可能であるため、スコーレム算術も決定可能である。

計算量

フェランテとラックオフ（1979、第5章）は、エーレンフォイヒト・フレッセゲームを用いて、理論の弱直冪の決定問題の計算量の上限を証明する方法を確立した。彼らはこの方法を適用して、の三重指数空間計算量、ひいてはスコーレム算術の 計算量を得た${\displaystyle (N^{*},{\bar {+}})}$

Grädel(1989、第5節)は、スコーレム算術の量指定子のないフラグメントの充足可能性問題がNP複雑性クラスに属することを証明している。

決定可能な拡張

フェファーマン・ヴォート定理を用いた上記の還元により、素因数の多重集合の理論を強化することで、より広範な関係式を定義する開式を持つ一階理論を得ることができる。例えば、と が異なる素因数の個数を持つ 場合に限り真となる関係式を考えてみよう。${\displaystyle a\sim b}$ ${\displaystyle a}$ ${\displaystyle b}$

${\displaystyle |\{p\mid \mathrm {prime} (p)\land (p|a)\}|\ =\ |\{p\mid \mathrm {prime} (p)\land (p|b)\}|}$

たとえば、両辺が 2 つの異なる素因数を持つ数を表す場合などです。 ${\displaystyle 2^{10}\cdot 3^{100}\sim 5^{8}\cdot 19^{9}}$

この関係をスコーレム算術に加えても、決定可能性は維持されます。これは、フェファーマン・ヴォート定理によって示されるように、集合上の等数性作用素が存在する場合でも、添え字集合の理論が決定可能性を維持するためです。 ${\displaystyle \sim }$

決定不能な拡張

後続述語を用いたスコーレム算術の拡張は、タルスキの恒等式を用いて加法関係を定義できる。^{[4] [5]}${\displaystyle succ(n)=n+1}$

${\displaystyle (c=0\lor c=a+b)\Leftrightarrow (ac+1)(bc+1)=c^{2}(ab+1)+1}$

正の整数の 関係を次のように定義する。${\displaystyle c=a+b}$

${\displaystyle \mathrm {succ} (ac)\,\mathrm {succ} (bc)=\mathrm {succ} (c^{2}\mathrm {succ} (ab))}$

乗算と加算の両方を表現できるため、結果として得られる理論は決定不可能です。

自然数（より小さい、）に対する順序述語がある場合、次のように 表すことができます。${\displaystyle <}$ ${\displaystyle \mathrm {succ} }$

${\displaystyle \mathrm {succ} (a)=b\ \ \Leftrightarrow \ \ a<b\land \forall c.{\big (}a<c\Rightarrow (b=c\lor b<c){\big )}}$

したがって、 による拡張も決定できません。 ${\displaystyle <}$

参照

• プレスバーガー算術
• ロビンソン算術
• 量指定子除去

参考文献

1. Nadel 1981
2. Ferrante & Rackoff 1979, p. 135
3. セギエルスキ 1981.
4. ロビンソン 1949年、100ページ。
5. ベス＆リチャード 1998.

参考文献

• アレクシス・ベス（2001年）「算術的定義可能性の概説」（PDF）。マルセル・クラッベ、フランソワーズ・ポイント、クリスチャン・ミショー（編）『モーリス・ボッファへのトリビュート』ブリュッセル：ベルギー数学協会、 pp .  1-54

• ベス, アレクシス; リチャード, デニス (1998). 「スコーレム算術の決定不能な拡張」. Journal of Symbolic Logic . 63 (2): 379– 401. CiteSeerX  10.1.1.2.1139 . doi :10.2307/2586837. JSTOR  2586837. S2CID  14566619.

• Cegielski、Patrick (1981)、「Théorie élémentaire de la multiplication des entiers Naturels」、ベルリン、シャンタル。マクアルーン、ケネス。 Ressayre、Jean-Pierre (編)、『Model Theory and Arithmetic』、ベルリン: Springer、44 ～ 89 ページ。

• フェランテ, ジャンヌ; ラックオフ, チャールズ W. (1979). 論理理論の計算複雑性. ベルリン・ハイデルベルク, ニューヨーク: シュプリンガー・フェアラーク. doi :10.1007/BFb0062837. ISBN 3-540-09501-2。

• グレーデル、エーリッヒ（1989年6月）「ドミノと論理理論のサブクラスの複雑性」純粋応用論理年報43 ( 1): 1–30 . doi : 10.1016/0168-0072(89) 90023-7

• Nadel, Mark E. (1981). 「ペアノ乗算の完全性」 .イスラエル数学ジャーナル. 39 (3): 225– 233. doi : 10.1007/bf02760851 . 2022年9月8日閲覧。

• Robinson, Julia Hall Bowman (1949). 「算術における定義可能性と決定問題」(PDF) . Journal of Symbolic Logic . 14 (2): 98– 114. doi :10.2307/2266510. JSTOR  2266510. S2CID  40861592. 2022年9月5日閲覧.