スコレム算術

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

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

以下に、略語を定義します。

$${\displaystyle {\begin{aligned}a\mid b&:=\exists n\;(a\cdot n=b)\\\operatorname {One} (e)&:=\forall n\;(n\cdot e=n)\\\operatorname {Prime} (p)&:=\lnot \operatorname {One} (p)\land \forall a\;(a\mid p\to (\operatorname {One} (a)\lor a=p))\\\operatorname {PrimePower} (p,P)&:=\operatorname {Prime} (p)\land p\mid P\land \forall q\;(\operatorname {Prime} (q)\land \lnot (q=p)\to \lnot (q\mid P))\\\operatorname {InvAdicAbs} (p,n,P)&:=\operatorname {PrimePower} (p,P)\land P\mid n\land \forall Q\;((\operatorname {PrimePower} (p,Q)\land Q\mid n)\to Q\mid P)\\\operatorname {AdicAbsDiff} _{n}(p,a,b)&:=\operatorname {Prime} (p)\land p\mid ab\land \exists P\,\exists Q\;(\operatorname {InvAdicAbs} (p,a,P)\land \operatorname {InvAdicAbs} (p,b,Q)\land Q=p^{n}P)\end{aligned}}}$$ 平易な言葉で言うと：

• ${\displaystyle \operatorname {InvAdicAbs} (p,n,P)}$成り立つのは、${\displaystyle P}$は最大の整数乗です${\displaystyle p}$分裂させる${\displaystyle n}$その通り。

• ${\displaystyle \operatorname {AdicAbsDiff} _{n}(p,a,b)}$が成り立つのは、 p進評価が${\displaystyle b}$^{[ 3 ]}は p 進評価を超える${\displaystyle a}$ちょうど${\displaystyle n}$つまり${\displaystyle v_{p}(b)=v_{p}(a)+n}$。

スコレム算術の公理は次のとおりです。^{[ 4 ]}

1. ${\displaystyle \forall a\,\forall b\;(ab=ba)}$
2. ${\displaystyle \forall a\,\forall b\,\forall c\;((ab)c=a(bc))}$
3. ${\displaystyle \exists e\;\operatorname {One} (e)}$
4. ${\displaystyle \forall a\,\forall b\;(\operatorname {One} (ab)\to \operatorname {One} (a)\land \operatorname {One} (b))}$
5. ${\displaystyle \forall a\,\forall b\,\forall c\;(ac=bc\to a=b)}$
6. ${\displaystyle \forall a\,\forall b\;(a^{n}=b^{n}\to a=b){\text{ for each integer }}n>0}$
7. ${\displaystyle \forall x\,\exists a\,\exists r\;(x=ar^{n}\land \forall b\,\forall s\;(x=bs^{n}\to a\mid b)){\text{ for each integer }}n>0}$
8. ${\displaystyle \forall a\,\exists p\;(\operatorname {Prime} (p)\land \lnot (p\mid a))}$^{[ 5 ]}
9. ${\displaystyle \forall p\,\forall P\,\forall Q\;((\operatorname {PrimePower} (p,P)\land \operatorname {PrimePower} (p,Q))\to (P\mid Q\lor Q\mid P))}$
10. ${\displaystyle \forall p\,\forall n\;(\operatorname {Prime} (p)\to \exists P\;\operatorname {InvAdicAbs} (p,n,P))}$
11. ${\displaystyle \forall n\,\forall m\;\left(n=m\leftrightarrow \forall p\;(\operatorname {Prime} (p)\to \exists P\;(\operatorname {InvAdicAbs} (p,n,P)\land \operatorname {InvAdicAbs} (p,m,P)))\right)}$^{[ 6 ]}
12. ${\displaystyle \forall p\,\forall n\,\forall m\;\left(\operatorname {Prime} (p)\to \exists P\,\exists Q\;(\operatorname {InvAdicAbs} (p,n,P)\land \operatorname {InvAdicAbs} (p,m,Q)\land \operatorname {InvAdicAbs} (p,nm,PQ))\right)}$^{[ 7 ]}
13. ${\displaystyle \forall a\,\forall b\;\left(\forall p\;(\operatorname {Prime} (p)\to \exists P\,\exists Q\;(\operatorname {InvAdicAbs} (p,a,P)\land \operatorname {InvAdicAbs} (p,b,Q)\land P\mid Q))\to a\mid b\right)}$^{[ 8 ]}
14. ${\displaystyle \forall a\,\forall b\,\exists c\,\forall p\;\left(\operatorname {Prime} (p)\to \left((p\mid a\to \exists P\;(\operatorname {InvAdicAbs} (p,b,P)\land \operatorname {InvAdicAbs} (p,c,P)))\land (p\mid b\to p\mid a)\right)\right)}$^{[ 9 ]}
15. ${\displaystyle \forall a\,\exists b\,\forall p\;\left(\operatorname {Prime} (p)\to \left(\exists P\;(\operatorname {InvAdicAbs} (p,a,P)\land \operatorname {InvAdicAbs} (p,b,pP))\right)\land (p\mid b\to p\mid a)\right)}$^{[ 10 ]}
16. ${\displaystyle \forall a\,\forall b\,\exists c\,\forall p\;\left(\operatorname {Prime} (p)\to \left((\operatorname {AdicAbsDiff} _{n}(p,a,b)\to \operatorname {InvAdicAbs} (p,c,p))\land (p\mid c\to \operatorname {AdicAbsDiff} _{n}(p,a,b))\right)\right)}$^{[ 11 ]}

正の整数の等号と乗算を用いた一階述語論理は、関係を表現できる。 ${\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})}$

スコレム算術の式の真偽値は、素因数分解を構成する非負整数の列の真偽値に帰着し、乗算は列の要素ごとの加算となる。決定可能性は、量化子消去を用いて示すことができるフェファーマン・ヴォートの定理から導かれる。別の言い方をすれば、正整数の1階理論は、多重集合和演算を持つ非負整数の有限多重集合の1階理論と同型であり、その決定可能性は要素理論の決定可能性に帰着する。

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

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

素数の場合${\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 {+}})}$。

1 階述語論理のFeferman–Vaught 定理によれば、数列とその数列上の各要素の加算に関する 1 階述語論理式の真理値は、アルゴリズム的に、加算を伴う数列の要素の理論における式の真理値に帰着し、この場合はPresburger 算術となる。Presburger 算術は決定可能であるため、Skolem 算術も決定可能である。^{[ 12 ]}

Ferrante & Rackoff (1979 、第5章)は、Ehrenfeucht–Fraïssé ゲームを使用して、理論の弱い直接べき乗の決定問題の複雑さの上限を証明する方法を確立しました。彼らはこの方法を適用して、3 倍指数的な空間複雑性を得ました。${\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)\}|}$

例えば、${\displaystyle 2^{10}\cdot 3^{100}\sim 5^{8}\cdot 19^{9}}$なぜなら、両辺とも2つの異なる素因数を持つ数を表しているからである。

関係を追加すると${\displaystyle \sim }$スコレム算術に関しては、決定可能である。これは、フェファーマン・ヴォートの定理で示されているように、集合上の等数性演算子が存在する場合でも、インデックス集合の理論が決定可能であるためである。

後継述語によるスコレム算術の拡張、${\displaystyle succ(n)=n+1}$タルスキの恒等式を用いて加算関係を定義できる。^{[ 13 ] [ 14 ]}

${\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 <}$これも決定不能である。

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