S2S（数学）

数学において、S2Sは2つの後継を持つ単項2階理論である。その1階対象は有限の2進文字列である。S2Sは、多くの決定可能理論がS2Sで解釈可能であり、最も表現力豊かな自然決定可能理論の1つである。その決定可能性は1969年にラビンによって証明された。^{[ 1 ]}

S2S の一次オブジェクトは有限バイナリ文字列です。二次オブジェクトは、有限バイナリ文字列の任意の集合（または単項述語）です。S2S には、文字列に文字を 1 つ追加する関数s ↦ s 0 とs ↦ s 1、および文字列sが集合Sに属することを意味する述語s ∈ S（またはS ( s )）があります。2 つの文字列s 0 とs 1 は、この理論の名前の由来となったsの 2 つの後継文字列です。

いくつかの特性と慣例：

• デフォルトでは、小文字は一階述語論理のオブジェクトを、大文字は二階述語論理のオブジェクトを表します。
• セットを含めることでS2Sは2階となり、「単項」とはk >1の場合にk項述語変数が存在しないことを意味する。
• 文字列sとtの連結はstで表され、 S2S では一般に利用できません。s ↦0 sも同様です。文字列間の接頭辞関係は定義可能です。
• 等号は基本的であり、 s = t ⇔ ∀ S ( S ( s ) ⇔ S ( t )) およびS = T ⇔ ∀ s ( S ( s ) ⇔ T ( s ))と定義できます。
• 文字列の代わりに、（例えば）n ↦2 n +1 とn ↦2 n +2 のような演算はできるが、その他の演算はできない自然数を使うことができる。
• すべてのバイナリ文字列の集合は、クリーネスターを使用して{0,1} ^*で表されます。
• {0,1} ^*の任意の部分集合は、木と同一視されることがあり、具体的には {0,1} ラベル付き木 {0,1} ^*として識別されます。 {0,1} ^*は完全な無限二分木を形成します。
• 数式の複雑さに関しては、文字列の接頭辞関係は通常、一階述語として扱われます。それがなければ、すべての数式が等価になるわけではありません。${\displaystyle \Delta _{2}^{1}}$数式。^{[ 2 ]}
• S2Sで表現可能なプロパティ（すべてのバイナリ文字列の集合を木と見なす）の場合、各ノードについて、左サブツリーと右サブツリーと残りの部分との間で通信できるのはO （1）ビットのみです（通信複雑性を参照）。
• 固定されたkに対して、文字列からk (つまりk未満の自然数)への関数は、単一の集合で符号化できます。さらに、s , t ⇒ s 01 t ′ ( t ′はtのすべての文字を2倍にする) は単射であり、s ⇒ { s 01 t ′ : t ∈{0,1} ^* } は S2S で定義可能です。対照的に、通信複雑性の議論により、S1S (下記) では、2 つの集合は単一の集合で符号化できません。

S2S の弱化: 弱 S2S (WS2S) では、すべての集合が有限である必要があります (有限性は、ケーニッヒの補題を使用して S2S で表現できることに注意してください)。S1S は、文字列に「1」が出現しないことを要求することで得られ、WS1S も有限性を必要とします。WS1S でさえ、定義可能な加算を持つ無制限の二進数を表すために集合を使用できることから、2 のべき乗の述語を使用してプレスバーガー算術を解釈できます。

意思決定の複雑性

S2Sは決定可能であり、S2S、S1S、WS2S、WS1Sのそれぞれは、指数関数の線形増加スタックに対応する非初等的な決定複雑度を持つ。下限については、以下を考慮すれば十分である。${\displaystyle {\シグマ }_{1}^{1}}$WS1S文。単一の2階量化子を使用して算術演算（またはその他の演算）を提案できます。どの数値が等しいかをテストできれば、1階量化子を使用して検証できます。このために、数値1..mを適切にエンコードすると、バイナリ表現i ₁ i ₂ ... i _mを持つ数値を、ガードを前に付けてi ₁ 1 i ₂ 2 ... i _m mとしてエンコードできます。ガードのテストを統合し、変数名を再利用することで、ビット数は指数関数の数に比例します。上限については、決定手順（下記）を使用すると、k重量化子交替を持つ文は、文の長さのk + O (1)重指数関数（均一定数を使用）に対応する時間で決定できます。

公理化

WS2Sは、いくつかの基本的な性質と帰納的スキームによって公理化することができる。^{[ 3 ]}

S2S は、 (1) ∃!によって部分的に公理化できる。s ∀ t ( t 0≠ s ∧ t 1≠ s ) (空文字列、ε で表す。 ∃! s は「一意のsが存在する」という意味) (2) ∀ s , t ∀ i ∈{0,1} ∀ j ∈{0,1} ( si = tj ⇒ s = t ∧ i = j ) ( iとjの使用は省略形。i = jの場合、0 は 1 と等しくない) (3) ∀ S ( S (ε) ∧ ∀ s ( S ( s ) ⇒ S ( s 0) ∧ S ( s 1))⇒ ∀ s S (s)) (帰納法) (4) ∃ S ∀ s ( S ( s ) ⇔ φ( s )) ( S はφ で自由ではない)

（4）は、二階述語論理では常に成り立つ、論理式φに対する内包表記図です。通常どおり、φに示されていない自由変数がある場合は、公理の普遍閉包を取ります。述語に対して等号が基本である場合、外延性S = T ⇔ ∀ s ( S ( s ) ⇔ T ( s ))も追加します。内包表記があるため、帰納法は図式ではなく単一の文で表すことができます。

S1S の類似の公理化は完全である。^{[ 4 ]}しかし、S2S については、完全性は未解決である (2021 年現在)。S1S は均一化されているが、空でない集合Sが与えられたときにSの要素を返すS2S 定義可能な (パラメータを許容しても)選択関数は存在しない。^{[ 5 ]}また、内包表記法は、選択公理のさまざまな形式で拡張されるのが一般的である。ただし、特定のパリティ ゲームに対する決定性表記法で拡張すると、(1)-(4) は完全である。^{[ 6 ]}

^{S2S は、Π 1} ₃文 (文字列の接頭辞関係を基本要素として使用)によって公理化することもできます。しかし、有限に公理化できるわけではなく、帰納スキーマと有限個の他の文を追加してもΣ ¹ _{3文によって公理化することもできません (これは、Π} ¹ ₂ -CA ₀との関連性から導かれます)。

任意の有限kに対して、木幅≤ kの可算グラフの単項二階 (MSO) 理論(および対応する木分解) は S2S で解釈可能です ( Courcelle の定理を参照)。たとえば、木 (グラフとして) または直並列グラフの MSO 理論は決定可能です。ここで (つまり、有界木幅の場合)、頂点 (または辺) の集合の有限性量化子を解釈することも、固定整数を法として集合内の頂点 (または辺) を数えることもできます。非可算グラフを許容しても理論は変わりません。また、比較のために、S1S は有界パス幅の連結グラフを解釈できます。

対照的に、無制限の木幅を持つグラフの任意の集合に対して、その存在量（つまり${\displaystyle {\シグマ }_{1}^{1}}$) 頂点と辺の両方に述語を許容すると、MSO 理論は決定不能になります。したがって、ある意味では、S2S の決定可能性は可能な限り最良です。無制限の木幅を持つグラフは大きなグリッドマイナーを持ち、これを使用してチューリング マシンをシミュレートできます。

S2Sへの還元により、可算線形順序のMSO理論は決定可能であり、クリーネ・ブロワー順序を持つ可算木のMSO理論も同様である。しかし、(${\displaystyle \mathbb {R} }$, < ) は決定不能です。^{[ 7 ] [ 8 ]}順序数< ω ₂ の MSO 理論は決定可能です。ω _{2の決定可能性は}ZFCに依存しません(Con(ZFC +弱コンパクト基数) を仮定)。^{[ 9 ]}また、順序数は、定義可能な正規基数から順序数の加算と乗算によって 得られる場合に限り、順序数上の単項二階論理を使用して定義可能です。^{[ 10 ]}

S2Sは特定の様相論理の決定可能性を調べるのに役立ち、クリプキ意味論は自然に木構造へと導く。

S2S+U (または単に S1S+U) は、U が非有界量化子である場合、すなわち、 U X Φ( X ) が任意の大きな有限Xに対して成り立つ場合に限り、決定不能である。^{[ 11 ]}しかし、WS2S+Uは 、無限パス上の量化であっても、U を含まない S2S 部分式であっても、決定可能である。^{[ 12 ]}

バイナリ文字列の集合は、それが正規である（つまり正規言語を形成する）場合に限り、S2S で定義可能です。S1S では、集合に対する（単項）述語は、それがω-正規言語である場合に限り、（パラメータなしで）定義可能です。S2S では、自由変数を 1 を含まない文字列のみで使用する式の場合、表現力は S1S と同じです。

任意の S2S 式 φ( S ₁ ,..., S _k ) ( k 個の自由変数を持つ) とバイナリ文字列の有限木Tに対して、φ( S ₁ ∩T,..., S _k ∩T) は | T |に線形の時間で計算できます( Courcelle の定理を参照)。ただし、上記のように、オーバーヘッドは式のサイズに対して指数関数的に反復できます (より正確には、時間は${\displaystyle O(|T|k)+2_{O(|\phi |)}^{2}}$)

^{S1S の場合、すべての式は Δ 1} ₁式と Π ⁰ ₂算術式のブール結合に等価です。さらに、すべての S1S 式は、対応するω オートマトンによる式のパラメータの受理に等価です。オートマトンには決定性パリティ オートマトンがあります。パリティ オートマトンは各状態に整数優先度を持ち、無限回観測された最高優先度が奇数 (または偶数) の場合に限り受理します。

S2S の場合、ツリー オートマトン (下記参照) を使用すると、すべての式は Δ ¹ ₂式と等価になります。さらに、すべての S2S 式は、4 つの量化子のみを持つ式 ∃ S ∀ T ∃ s ∀ t ... と等価です (形式化に前置関係と後継関数の両方が含まれていると仮定した場合)。S1S の場合は 3 つの量化子 (∃ S ∀ s ∃ t ) で十分であり、WS2S および WS1S の場合は 2 つの量化子 (∃ S ∀ t ) で十分です。WS2S および WS1S では前置関係は必要ありません。

しかし、自由二次変数では、すべてのS2S式がΠ ¹ ₁超限再帰のみで二次算術で表現できるわけではありません（逆数学を参照）。RCA ₀ + (schema) {τ: τは真のS2S文である}は、(schema) {τ: τはΠ ¹ ₂ -CA _{0で証明可能なΠ} ¹ ₃文である}と同等です。^{[ 13 ] [ 14 ]} 基本理論上では、スキーマは(schema over k ) ∀ S ⊆ω ∃α ₁ < ... < α _k L _{α 1} ( S ) ≺ _{Σ 1} ... ≺ _{Σ 1} L _{α k} (S)と同等です。ここでLは構成可能な宇宙です（大きな可算順序数 も参照）。帰納法が限定されているため、Π ¹ ₂ -CA _{0 は}、すべての真（標準決定手続きの下で）Π ¹ ₃ S2S ステートメントが実際に真であることを証明しません。ただし、そのような各文は Π ¹ ₂ -CA ₀で証明可能です。

さらに、バイナリ文字列の集合SとTが与えられたとき、以下は同等である: (1) Tは、 Sから多項式時間で計算可能なバイナリ文字列の集合から S2S 定義可能である。 (2) T は、利得が Π ⁰ ₂ ( S ) 集合の有限ブール結合であるゲームの勝利位置の集合から計算できる。 (3) T は、算術 μ 計算 (算術式 +最小不動点論理)でSから定義できる。 (4) Tは、 Sを含み、Π ¹ ₂ -CA ₀におけるΠ ¹ ₃のすべての帰結を満たす最小β モデル(つまり、集合論的対応物が推移的である ω モデル)に含まれる。

標準モデル（S1SおよびS2Sの唯一のMSOモデル）に加えて、S1SおよびS2Sには、ドメインのすべてではなく一部のサブセットを使用する他のモデルも存在します（ヘンキン意味論を参照）。

任意のS ⊆ωに対して、Sで再帰的な集合は標準 S1S モデルの基本的な部分モデルを形成し、チューリング結合とチューリング還元可能性に関して閉じている ω の空でない部分集合のコレクションについても同様である。^{[ 16 ]}

これは、S1S 定義可能集合の相対的再帰性と一様化から導かれる。 - φ( s ) ( sの関数として) は、φ のパラメータと、有限集合s ′ (そのサイズは φ の決定性オートマトンの状態数によって制限される)の φ( s ′ ) の値から計算できる。 - ∃ S φ( S ) の証拠は、kとSの有限断片S ′を選択し、各拡張中の最高優先度がkであり、 kを超える優先度(これらは最初のS ′に対してのみ許可される) にヒットすることなく φ を満たすSに拡張を完了できるようなS ′を繰り返し拡張することによって得られる。また、辞書式最短最小の選択を使用することにより、φ'⇒φ および ∃ S φ( S ) ⇔∃!となる S1S 式 φ' が存在する。S φ'( S ) (すなわち均一化。φ には表示されていない自由変数がある可能性がある。φ' は式 φ のみに依存する)。

S2S の最小モデルは、バイナリ文字列上のすべての正規言語で構成されます。これは標準モデルの基本サブモデルであるため、S2S のパラメータフリー定義可能ツリー集合が空でない場合、正規ツリーが含まれます。正規言語は、正規 {0,1} ラベル付き完全無限二分木 (文字列上の述語と同一視) としても扱うことができます。ラベル付きツリーは、開始頂点を持つ頂点ラベル付き有限有向グラフを展開することによって得られる場合に正規です。開始頂点から到達可能なグラフ内の (有向) サイクルは、無限ツリーを与えます。正規ツリーのこの解釈と符号化により、すべての真の S2S 文は、すでに基本関数演算で証明できる可能性があります。非正規ツリーは、決定性のために非述語的理解を必要とする場合があります (下記参照)。計算可能な充足関係を持つ、非正規（つまり非正規言語を含む）なS1S（そしておそらくS2S）モデル（標準的な一階述語部分の有無を問わず）が存在する。しかし、文字列の再帰的集合の集合は、理解と決定性の不備のため、S2Sモデルを形成しない。

決定可能性の証明は、すべての式が非決定性木オートマトンによる受理と同等であることを示すことによって行われます（木オートマトンと無限木オートマトンを参照）。無限木オートマトンはルートから開始して木を上に移動し、すべての木の枝が受理する場合に限り受理します。非決定性木オートマトンは、プレイヤー 1 が勝利戦略を持っている場合に限り受理します。勝利戦略とは、プレイヤー 1 が（現在の状態と入力に対して）許可された新しい状態のペア ( p ₀、p ₁ ) を選択し、プレイヤー 2 が枝を選択し、0 が選択された場合はp _{0に、それ以外の場合は p 1}に遷移する戦略です。共非決定性オートマトンの場合、すべての選択はプレイヤー 2 によって行われますが、決定性の場合、(p ₀、p ₁ ) は状態と入力によって固定されます。また、ゲームオートマトンの場合、2 人のプレイヤーは有限ゲームをプレイして枝と状態を設定します。枝の受理は、枝上で無限回出現する状態に基づいています。ここではパリティオートマトンで十分一般的である。

数式をオートマトンに変換するには、基本ケースは簡単で、非決定性によって存在量化子の下で閉包が得られるため、補集合の下での閉包のみが必要となります。パリティゲームの位置決定性（ここで非述語的内包が必要になります）を使用すると、プレイヤー1の勝利戦略が存在しないことから、プレイヤー2の勝利戦略Sが得られ、その健全性を検証する共非決定性木オートマトンが存在します。その後、オートマトンを決定性にすることができ（ここで状態数が指数関数的に増加します）、したがってSの存在は非決定性オートマトンによる受理に対応します。

決定性: ZFC では、ボレル ゲームは決定可能であることが証明されており、Π ⁰ ₂式のブール結合 (任意の実パラメータを持つ) の決定性証明は、現在の状態とツリー内の位置のみに依存する戦略もここで与えます。証明は、優先度の数に関する帰納法によるものです。優先度がkあり、最も高い優先度がkであり、k がプレイヤー 2 に対して正しいパリティを持つと仮定します。各位置 (ツリーの位置 + 状態) に対して、プレイヤー 1 が、入力されたすべての優先度kの位置 (ある場合) のラベルが< α であるような最小の順序数 α (ある場合) を割り当てます。プレイヤー 1 は、初期位置が次のようにラベル付けされている場合に勝つことができます。優先度k の状態に到達するたびに順序数が減少し、さらに減少の間に、プレイヤー 1 はk -1 優先度の戦略を使用できます。プレイヤー 2 は、局面がラベル付けされていない場合に勝つことができます。k -1 の優先度の決定性により、プレイヤー 2 は、勝つか、ラベル付けされていない優先度kの状態に入る戦略を持ち、その場合、プレイヤー 2 はその戦略を再び使用できます。戦略を位置的（kに関する帰納法による）にするには、補助ゲームをプレイしているときに、選択された 2 つの位置的戦略が同じ局面につながる場合は、より低い α の戦略、または同じ α の場合はより低い初期局面（またはプレイヤー 2 の場合は）の戦略を継続します（これにより、戦略を有限回切り替えることができます）。

オートマトン決定化: 共非決定性木オートマトンを決定化するには、ω-オートマトンを考慮し、分岐選択を入力として扱い、オートマトンを決定化し、それを決定性木オートマトンに使用すれば十分です。ただし、左に進む (つまりs ↦ s 0) の決定化は右分岐の内容に依存する可能性があるため、非決定性木オートマトンではこの方法は機能しません。非決定性とは対照的に、決定性木オートマトンでは正確に空でない集合を受け入れることさえできません。非決定性 ω-オートマトンM (共非決定性の場合は補集合を取り、決定性パリティオートマトンが補集合の下で閉じていることに注意) を決定化するには、各ノードがMの可能な状態の集合を格納し、ノードの作成と削除が優先度の高い状態に到達することに基づくSafra 木を使用できます。詳細は^{[ 17 ]}または^{[ 18 ]を参照してください。}

受理の決定可能性: 空の木の非決定性パリティ オートマトンによる受理は、有限グラフG上のパリティ ゲームに対応します。上記の位置的 (メモリレスとも呼ばれる) 決定性を使用すると、ループに到達したときに終了する有限ゲームでこれをシミュレートできます。勝敗条件は、ループ内の最高優先度状態に基づいています。巧妙な最適化により、準多項式時間アルゴリズム^{[ 19 ]}が得られます。これは、優先度の数が十分に小さい場合 (実際にはよくあることです) には多項式時間になります。

木の理論: 木 (つまり、木であるグラフ) 上の MSO 論理の決定可能性については、有限性と一階述語対象のモジュラー計数量化子を使用しても、可算木を完全二分木に埋め込み、S2S の決定可能性を使用できます。たとえば、ノードsの場合、その子をs 1、s 01、s 001 などで表すことができます。非可算木の場合は、Shelah–Stup の定理 (下記) を使用できます。また、基数 ω ₁を持つ一階述語対象の集合に対する述語、基数 ω ₂に対する述語など、無限の正則基数に対する述語を追加することもできます。木の幅が制限されているグラフは木を使用して解釈可能であり、エッジに対する述語がない場合、これはクリークの幅が制限されているグラフにも適用されます。

単項理論の木拡張: Shelah–Stup 定理により、^{[ 20 ] [ 21 ]}単項関係モデルMが決定可能であれば、その木対応物も決定可能です。たとえば、(形式化の選択を除いて) S2S は {0,1} の木対応物です。木対応物では、一階オブジェクトは拡張によって順序付けられたMの要素の有限シーケンスであり、M関係P _iはP _i '( vd ₁ ,..., vd _k ) ⇔ P _i ( d ₁ ,..., d _k )にマッピングされ、それ以外の場合はP _i ' は偽となります ( d _j ∈ M、vはMの要素の (空である可能性のある) シーケンス)。証明は S2S の決定可能性証明と同様です。各ステップで、（非決定性）オートマトンに（2階述語論理の場合もある）M個のオブジェクトのタプルが入力として渡され、 M個の式によってどの状態遷移が許可されるかが決定されます。プレイヤー1（上記参照）は、式によって許可される写像 child⇒state（現在の状態が与えられた場合）を選択し、プレイヤー2は（ノードの）子を選択して処理を続行します。非決定性オートマトンによる拒否を確認するには、各（ノード、状態）について、すべての選択で少なくとも1つのペアがヒットし、結果として得られるすべてのパスが拒否につながるような（子、状態）ペアのセットを選択します。

モナド理論と一階理論の組み合わせ:フェファーマン-ヴォート定理は次のように拡張/適用されます。M が MSO モデルで N が一階モデルである場合、 Mが最初のオブジェクトと同一視されるすべての関数M → Nで拡張され、各s ∈ Mに対して言語がそれに応じて変更されたNの非連結コピーを使用する場合でも、 Mは (Theory( M ), Theory( N ))オラクルに関して決定可能です。たとえば、Nが (${\displaystyle \mathbb {R} }$,0,+,⋅)、∀(関数f ) ∀ s ∃ r ∈ N _s f ( s ) + _{N s} r = 0 _{N s}と述べることができます。M が S2S (またはより一般的には、何らかのモナド モデルのツリー対応) である場合、オートマタはN式を使用し、それによってf : M → N ^{k を}M個の集合のタプルに変換できます。非交差性は必要であり、そうでない場合は、等号を持つすべての無限Nに対して、拡張 S2S または単に WS1S は決定不能になります。また、（不完全な可能性のある）理論Tに対して、 TのM積の理論T ^Mは、(Theory( M ), T ) オラクルに関して決定可能です。ここで、 T ^Mのモデルは、各s ∈ Mに対して、 Tの任意の互いに素なモデルN _{s を}使用します(上記のように、Mは MSO モデルです。Theory( N _s ) はsに依存する可能性があります)。証明は、式の複雑さに関する帰納法によるものです。v s_を、関数fが自由である場合はf ( s ) を含む、自由N _s変数のリストとします。帰納法により、 v _{s は、} | v _s | 個の自由変数を持つ有限個のN式を通してのみ使用されることが示されます。したがって、 N (またはT )を使用して何が可能かを答えることで、すべての可能な結果を​​定量化でき、可能性のリスト (または制約) が与えられた場合、Mで対応する文を定式化できます。

S2S の拡張への符号化:文字列上の決定可能な述語はすべて、符号化された述語とともに、S2S の決定可能性 (上記の拡張があっても) のために (線形時間の符号化と復号化で) 符号化できます。証明: 非決定的な無限木オートマトンが与えられた場合、有限二分ラベル付き木 (オートマトンが操作できるラベルを持つ) の集合を有限個のクラスに分割できます。完全な無限二分木が同じクラスの木で構成できる場合、受理はクラスと初期状態 (つまり、オートマトンが木に入る状態) のみに依存します。(ポンピング補題と大まかな類似性があることに注意してください。) 例えば (パリティ オートマトンの場合)、初期状態と (状態、到達した最高優先度) ペアの集合Qが与えられたときに、プレイヤー 1 (つまり非決定性) がすべての分岐を同時にQの要素に対応させることができるかどうかを返す述語が同じである場合、木を同じクラスに割り当てます。次に、各kに対して、オートマトン 1～ kに対して同じクラスに属する有限個の木（符号化に適したもの）を選択します。クラスの選択はk全体で一貫している必要があります。述語を符号化するには、k = 1 を使用していくつかのビットを符号化し、次にk = 2を使用してさらに多くのビットを符号化する、といった具合に続けます。

• Weyer, Mark (2002). 「S1SとS2Sの決定可能性」 . Automata, Logics, and Infinite Games . Lecture Notes in Computer Science. Vol.  2500. Springer. pp. 207–230 . doi : 10.1007/3-540-36387-4_12 . ISBN  978-3-540-00388-5。