S2S (गणित)

गणित में, S2S दो उत्तराधिकारियों के साथ मोनैडिक दूसरे क्रम का तर्क है। यह ज्ञात सबसे अभिव्यंजक प्राकृतिक निर्णायक सिद्धांतों में से एक है, जिसमें S2S में कई निर्णायक सिद्धांतों की व्याख्या की जा सकती है। इसकी निर्णायकता 1969 में माइकल ओ. राबिन द्वारा सिद्ध की गई थी।

मूल गुण

S2S की प्रथम क्रम की वस्तुएं परिमित बाइनरी स्ट्रिंग हैं। दूसरे क्रम की वस्तुएं परिमित बाइनरी स्ट्रिंग्स के मनमाने सेट (या एकात्मक विधेय) हैं। S2S में स्ट्रिंग्स पर फ़ंक्शन s→s0 और s→s1 हैं, और विधेय s∈S (समकक्ष, S(s)) का अर्थ है कि स्ट्रिंग s सेट S से संबंधित है।

कुछ गुण और परंपराएँ:

• डिफ़ॉल्ट रूप से, लोअरकेस अक्षर पहले क्रम की वस्तुओं को संदर्भित करते हैं, और अपरकेस दूसरे क्रम की वस्तुओं को संदर्भित करते हैं।
• सेटों का समावेश S2S को दूसरे क्रम का बनाता है, जिसमें k>1 के लिए k-ary विधेय चर की अनुपस्थिति का संकेत मिलता है।
• स्ट्रिंग्स s और t का संयोजन st द्वारा दर्शाया जाता है, और यह आम तौर पर S2S में उपलब्ध नहीं है, यहां तक ​​कि s→0s में भी नहीं। स्ट्रिंग्स के बीच स्ट्रिंग ऑपरेशन निश्चित है।
• समानता आदिम है, या इसे s = t ⇔ ∀S (S(s) ⇔ S(t)) और S = T ⇔ ∀s (S(s) ⇔ T(s)) के रूप में परिभाषित किया जा सकता है।
• स्ट्रिंग्स के स्थान पर, कोई (उदाहरण के लिए) n→2n+1 और n→2n+2 के साथ प्राकृतिक संख्याओं का उपयोग कर सकता है, लेकिन कोई अन्य ऑपरेशन नहीं।
• सभी बाइनरी स्ट्रिंग्स का सेट {0,1} द्वारा दर्शाया गया है^*, क्लेन स्टार का उपयोग करते हुए।
• {0,1} का मनमाना उपसमुच्चय^* को कभी-कभी पेड़ों से पहचाना जाता है, विशेष रूप से {0,1}-लेबल वाले पेड़ {0,1} के रूप में^*; {0,1}^* एक पूर्ण अनंत बाइनरी ट्री बनाता है।
• सूत्र जटिलता के लिए, स्ट्रिंग्स पर उपसर्ग संबंध को आम तौर पर पहले क्रम के रूप में माना जाता है। इसके बिना, सभी सूत्र Δ के समतुल्य नहीं होंगे¹₂ सूत्र.
• S2S में अभिव्यक्त गुणों के लिए (सभी बाइनरी स्ट्रिंग्स के सेट को एक पेड़ के रूप में देखते हुए), प्रत्येक नोड के लिए, केवल O(1) बिट्स को बाएं सबट्री और दाएं सबट्री और बाकी के बीच संचारित किया जा सकता है (संचार जटिलता देखें)।
• एक निश्चित k के लिए, स्ट्रिंग से k तक एक फ़ंक्शन (यानी k के नीचे की प्राकृतिक संख्या) को एक सेट द्वारा एन्कोड किया जा सकता है। इसके अलावा, s,t ⇒ s01t′ जहां टी′ t के प्रत्येक वर्ण को दोगुना कर देता है, और s ⇒ {s01t′: t∈{0,1}^*} S2S निश्चित है। इसके विपरीत, संचार जटिलता तर्क के अनुसार, S1S (नीचे) में सेट की एक जोड़ी एक सेट द्वारा एन्कोड करने योग्य नहीं है।

S2S की कमजोरियाँ: कमजोर S2S (WS2S) के लिए सभी सेटों का परिमित होना आवश्यक है (ध्यान दें कि परिमितता कोनिग के लेम्मा का उपयोग करके S2S में व्यक्त की जा सकती है)। S1S को यह आवश्यक करके प्राप्त किया जा सकता है कि '1' स्ट्रिंग्स में प्रकट न हो, और WS1S को भी परिमितता की आवश्यकता होती है। यहां तक ​​कि WS1S भी 2 की शक्तियों के विधेय के साथ प्रेस्बर्गर अंकगणित की व्याख्या कर सकता है, क्योंकि सेट का उपयोग निश्चित जोड़ के साथ असीमित बाइनरी संख्याओं का प्रतिनिधित्व करने के लिए किया जा सकता है।

'निर्णय जटिलता'

S2S निर्णय लेने योग्य है, और S2S, S1S, WS2S, WS1S में से प्रत्येक में घातांक के रैखिक रूप से बढ़ते ढेर के अनुरूप एक गैर-प्राथमिक समस्या निर्णय जटिलता है। निचली सीमा के लिए, Σ पर विचार करना पर्याप्त है¹₁ WS1S वाक्य. अंकगणित (या अन्य) गणना का प्रस्ताव करने के लिए एक दूसरे क्रम के क्वांटिफायर का उपयोग किया जा सकता है, जिसे पहले ऑर्डर क्वांटिफायर का उपयोग करके सत्यापित किया जा सकता है यदि हम परीक्षण कर सकते हैं कि कौन सी संख्याएं बराबर हैं। इसके लिए, यदि हम संख्याओं 1..m को उचित रूप से एन्कोड करते हैं, तो हम बाइनरी प्रतिनिधित्व i के साथ एक संख्या को एनकोड कर सकते हैं₁i₂...मैं_m जैसे मैं₁ 1 मैं₂ 2... मैं_m मी, एक गार्ड से पहले। गार्ड के परीक्षण को मर्ज करने और चर नामों का पुन: उपयोग करने से, बिट्स की संख्या घातांक की संख्या में रैखिक होती है। ऊपरी सीमा के लिए, निर्णय प्रक्रिया (नीचे) का उपयोग करके, के-गुना क्वांटिफायर विकल्प वाले वाक्यों को वाक्य की लंबाई (समान स्थिरांक के साथ) के के + ओ (1)-गुना घातांक के अनुरूप समय में तय किया जा सकता है।

'स्वयंसिद्धीकरण'

WS2S को कुछ बुनियादी गुणों और प्रेरण स्कीमा के माध्यम से स्वयंसिद्ध किया जा सकता है। S2S को आंशिक रूप से स्वयंसिद्ध किया जा सकता है:
(1) ∃!s ∀t ( t0≠s ∧ t1≠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(s0) ∧ S(s1))⇒ ∀s S(s)) (गणितीय प्रेरण)
(4) ∃S ∀s (S(s) ⇔ φ(s)) (S φ में मुक्त नहीं है)

(4) सूत्र φ पर विनिर्देशन की स्वयंसिद्ध स्कीमा है, जो हमेशा दूसरे क्रम के तर्क के लिए होती है। हमेशा की तरह, यदि φ में मुक्त चर नहीं दिखाए गए हैं, तो हम अभिगृहीत का सार्वभौमिक समापन लेते हैं। यदि समानता विधेय के लिए आदिम है, तो कोई विस्तारात्मकता का सिद्धांत भी जोड़ता है S=T ⇔ ∀s (S(s) ⇔ T(s))। चूँकि हमारे पास समझ है, इंडक्शन स्कीमा के बजाय एकल कथन हो सकता है।

S1S का अनुरूप स्वयंसिद्धीकरण पूरा हो गया है। हालाँकि, S2S के लिए, पूर्णता खुली है (2021 तक)। जबकि S1S में एकरूपता है, कोई S2S परिभाषित (यहां तक ​​कि पैरामीटर की अनुमति देने वाला) विकल्प फ़ंक्शन नहीं है जो एक गैर-खाली सेट दिया गया S, S का एक तत्व लौटाता है, और समझ स्कीमों को आम तौर पर पसंद के सिद्धांत के विभिन्न रूपों के साथ संवर्धित किया जाता है। हालाँकि, (1)-(4) कुछ समता खेलों के लिए निर्धारण स्कीमा के साथ विस्तारित होने पर पूर्ण हो जाता है। S2S को Π द्वारा भी स्वयंसिद्ध किया जा सकता है¹₃ वाक्य (स्ट्रिंग्स पर उपसर्ग संबंध को आदिम के रूप में उपयोग करना)। हालाँकि, यह अंतिम रूप से स्वयंसिद्ध नहीं है, न ही इसे Σ द्वारा स्वयंसिद्ध किया जा सकता है¹₃ वाक्य भले ही हम प्रेरण स्कीमा और अन्य वाक्यों का एक सीमित सेट जोड़ते हैं (यह Π से इसके संबंध से पता चलता है)¹₂-वह₀).

S2S से संबंधित सिद्धांत

प्रत्येक परिमित k के लिए, वृक्ष-चौड़ाई ≤k (और संबंधित वृक्ष अपघटन) के साथ गणनीय ग्राफ़ का मोनैडिक द्वितीय क्रम (MSO) सिद्धांत S2S में व्याख्या योग्य है (कोर्सेल का प्रमेय देखें)। उदाहरण के लिए, पेड़ों का एमएसओ सिद्धांत (ग्राफ़ के रूप में) या श्रृंखला-समानांतर ग्राफ़ का निर्णय लेने योग्य है। यहां (यानी बंधे हुए पेड़ की चौड़ाई के लिए), हम शीर्षों (या किनारों) के एक सेट के लिए परिमितता परिमाणक की व्याख्या भी कर सकते हैं, और एक निश्चित पूर्णांक के सेट मॉड्यूलो में शीर्षों (या किनारों) की गिनती भी कर सकते हैं। बेशुमार ग्राफ़ की अनुमति देने से सिद्धांत नहीं बदलता है। इसके अलावा, तुलना के लिए, S1S बंधे हुए पथ-चौड़ाई के जुड़े ग्राफ़ की व्याख्या कर सकता है।

इसके विपरीत, असंबद्ध वृक्ष-चौड़ाई के ग्राफ़ के प्रत्येक सेट के लिए, इसका अस्तित्व (यानी Σ)¹₁) यदि हम शीर्षों और किनारों दोनों पर विधेय की अनुमति देते हैं तो एमएसओ सिद्धांत अनिर्णीत है। इस प्रकार, एक अर्थ में, S2S की निर्णायकता सर्वोत्तम संभव है। अनबाउंड ट्रीविड्थ वाले ग्राफ़ में बड़े ग्रिड माइनर होते हैं, जिनका उपयोग ट्यूरिंग मशीन का अनुकरण करने के लिए किया जा सकता है।

S2S में कमी करके, गणनीय आदेशों का MSO सिद्धांत निर्णायक है, जैसा कि उनके क्लेन-ब्रौवर आदेशों के साथ गणनीय पेड़ों का MSO सिद्धांत है। हालाँकि, एमएसओ सिद्धांत ($\mathbb {R}$, <) अनिर्णीत है। ऑर्डिनल्स का एमएसओ सिद्धांत <ω₂ निर्णययोग्य है; ω के लिए निर्णायकता₂ ZFC से स्वतंत्र है (Con(ZFC + कमजोर रूप से कॉम्पैक्ट कार्डिनल मानते हुए))। इसके अलावा, एक ऑर्डिनल को ऑर्डिनल्स पर मोनैडिक सेकेंड ऑर्डर लॉजिक का उपयोग करके परिभाषित किया जा सकता है यदि इसे ऑर्डिनल जोड़ और गुणा द्वारा निश्चित नियमित कार्डिनल्स से प्राप्त किया जा सकता है। S2S कुछ मोडल लॉजिक्स की निर्णायकता के लिए उपयोगी है, क्रिपके शब्दार्थ स्वाभाविक रूप से पेड़ों की ओर ले जाता है।

S2S+U (या सिर्फ S1S+U) अनिर्णीत है यदि U अनबाउंडिंग क्वांटिफायर है - UX Φ(X) यदि Φ(X) कुछ मनमाने ढंग से बड़े परिमित X के लिए है। हालाँकि, WS2S+U, अनंत पथों पर परिमाणीकरण के साथ भी, निर्णय लेने योग्य है, यहां तक ​​कि S2S उपसूत्रों के साथ भी, जिनमें U शामिल नहीं है।

सूत्र जटिलता

बाइनरी स्ट्रिंग्स का एक सेट S2S में निश्चित है यदि यह नियमित है (यानी एक नियमित भाषा बनाता है)। S1S में, सेट पर एक (एकात्मक) विधेय (पैरामीटर-मुक्त) निश्चित है यदि यह एक ओमेगा-नियमित भाषा है|ω-नियमित भाषा है। S2S के लिए, उन सूत्रों के लिए जो अपने मुक्त चर का उपयोग केवल उन स्ट्रिंग्स पर करते हैं जिनमें 1 नहीं है, अभिव्यक्ति S1S के समान ही है।

प्रत्येक S2S सूत्र के लिए φ(S₁,...,एस_k), (k मुक्त चर के साथ) और बाइनरी स्ट्रिंग्स T, φ(S) का परिमित वृक्ष₁∩टी,...,एस_k∩T) की गणना |T| में रैखिक समय में की जा सकती है (कोर्सेल का प्रमेय देखें), लेकिन जैसा कि ऊपर बताया गया है, ओवरहेड को सूत्र आकार में घातीय रूप से दोहराया जा सकता है (अधिक सटीक रूप से, समय है $O(|T|k)+2_{O(|\phi |)}^{2}$).

S1S के लिए, प्रत्येक सूत्र Δ के बराबर है¹₁ सूत्र, और Π के बूलियन संयोजन के लिए⁰₂ अंकगणितीय सूत्र. इसके अलावा, प्रत्येक S1S सूत्र सूत्र के मापदंडों के संगत ω-ऑटोमेटन द्वारा स्वीकृति के बराबर है। ऑटोमेटन एक नियतात्मक समता ऑटोमेटन हो सकता है: एक समता ऑटोमेटन में प्रत्येक राज्य के लिए एक पूर्णांक प्राथमिकता होती है, और यदि अनंत रूप से देखी जाने वाली सर्वोच्च प्राथमिकता अक्सर विषम (वैकल्पिक रूप से, सम) होती है, तो इसे स्वीकार करता है।

S2S के लिए, ट्री ऑटोमेटा (नीचे) का उपयोग करते हुए, प्रत्येक सूत्र Δ के बराबर है¹₂ सूत्र. इसके अलावा, प्रत्येक S2S सूत्र केवल चार क्वांटिफायर, ∃S∀T∃s∀t ... वाले सूत्र के बराबर है (यह मानते हुए कि हमारी औपचारिकता में उपसर्ग संबंध और उत्तराधिकारी कार्य दोनों हैं)। S1S के लिए, तीन परिमाणक (∃S∀s∃t) पर्याप्त हैं, और WS2S और WS1S के लिए, दो परिमाणक (∃S∀t) पर्याप्त हैं; WS2S और WS1S के लिए यहां उपसर्ग संबंध की आवश्यकता नहीं है।

हालाँकि, मुक्त दूसरे क्रम के चर के साथ, प्रत्येक S2S सूत्र को केवल Π के माध्यम से दूसरे क्रम के अंकगणित में व्यक्त नहीं किया जा सकता है¹₁ ट्रांसफ़िनिट रिकर्सन (रिवर्स गणित देखें)। आरसीए₀ + (स्कीमा) {τ: τ एक सच्चा S2S वाक्य है} (स्कीमा) के बराबर है {τ: τ एक Π है¹₃ Π में सिद्ध वाक्य¹₂-वह₀ }. आधार सिद्धांत पर, स्कीमा (k पर स्कीमा) ∀S⊆ω ∃α के बराबर हैं₁<...<ए_k L_{α1</उप>(एस) ≺Σ1... ≺ उप>एस1</उप>एल उप>एk}(एस) जहां एल रचनात्मक ब्रह्मांड है (बड़े गणनीय क्रमसूचक भी देखें)। सीमित प्रेरण के कारण, Π¹₂-वह₀ यह सिद्ध नहीं करता कि सब सत्य है (मानक निर्णय प्रक्रिया के अंतर्गत) Π¹₃ S2S कथन वास्तव में सत्य हैं, भले ही ऐसा प्रत्येक वाक्य सिद्ध करने योग्य हो¹₂-वह₀.

इसके अलावा, बाइनरी स्ट्रिंग एस और टी के दिए गए सेट, निम्नलिखित समतुल्य हैं:
(1) टी एस2एस है जिसे एस से गणना योग्य बाइनरी स्ट्रिंग्स बहुपद समय के कुछ सेट से परिभाषित किया जा सकता है।
(2) टी की गणना कुछ गेम के लिए जीतने की स्थिति के सेट से की जा सकती है जिसका भुगतान Π का एक सीमित बूलियन संयोजन है⁰₂(एस) सेट.
(3) टी को अंकगणित μ-कैलकुलस में एस से परिभाषित किया जा सकता है (अंकगणित सूत्र + निश्चित-बिंदु तर्क | कम से कम निश्चित-बिंदु तर्क)
(4) टी सबसे कम बीटा-मॉडल में है|β-मॉडल (यानी एक ω-मॉडल जिसका सेट-सैद्धांतिक समकक्ष सकर्मक मॉडल है) जिसमें एस शामिल है और सभी Π को संतुष्ट करता है¹₃ Π के परिणाम¹₂-वह₀.

Proof sketch:

See and, but briefly the proof runs as follows. (1)⇒(2) follows from the below decidability proof using tree automata. (2)⇒(1) follows by converting the game associated with a binary string s into a tree parity game with a fixed number of priorities and then merging these trees into a single tree (the binary trees can be merged here using s,t ⇒ s01t′ where t′ doubles every character of t). The below determinacy proof (in the decidability section) also leads to (2)⇒(3). Π¹₂-CA₀ proves Δ¹₂ monotonic induction, so (3)⇒(4).

For (3)⇒(2), define a game where player 1 attempts to show that the desired element s is inside the least fixed point. Player 1 gradually labels elements including s with rational numbers, intended to correspond to ordinal stages of the monotonic induction (any countable ordinal is embeddable into $\mathbb {Q}$). Player 2 plays elements with strictly descending labels (and he can pass) and wins iff the sequence is infinite or player 2 wins the last auxiliary game. In the auxiliary game, player 1 attempts to show that the last element picked by player 2 is a valid inductive step using elements with smaller labels. Now, if s is not in the least fixed-point, then the set of labels is ill-founded, or an inductive step is wrong, and (using monotonicity) this can be picked up by player 2. (If player 1 plays a smaller label outside the least fixed point, player 2 can use it (abandoning the auxiliary game), otherwise (using monotonicity) player 2 can use an auxiliary game strategy that assumes that the set of smaller labels in the original game will equal the least fixed point.)

For (4)⇒(3), we use monotonic induction to build an initial segment of the constructible hierarchy above a given real number r. This works as long as each ordinal α is identified by some appropriately expressible property of α so that we can encode α by a natural number and continue. Now, suppose that we built L_α(r) and the inductive step (which uses L_α(r) as a parameter) allows examining L_β(r). If a new Σ₁^(L(r),∈,r) fact appears between α and β, we can use it to label α and continue. Otherwise, we get the above Σ₁ elementary chains whose length corresponds to the nesting depth of the monotonic inductive definitions.

For the equivalence of RCA₀+S2S with {Π¹₃ φ: Π¹₂-CA₀⊢φ}, for each k the positional determinacy with k priorities is provable in Π¹₂-CA₀, while the rest (in terms of proving S2S sentences) can be done in a weak base theory. Conversely, RCA₀+S2S gives us a determinacy schema that gives existence of least fixed points (by a modification of the above (3)⇒(2) and even without requiring positionality; see the reference). In turn, their existence (using (4)⇒(3)) gives the desired Σ₁ elementary chains.

S1S और S2S के मॉडल

मानक मॉडल (जो S1S और S2S के लिए अद्वितीय MSO मॉडल है) के अलावा, S1S और S2S के लिए अन्य मॉडल भी हैं, जो डोमेन के सभी सबसेट के बजाय कुछ का उपयोग करते हैं (रिफंड नैरो सीएस देखें)।

प्रत्येक S⊆ω के लिए, S में पुनरावर्ती सेट मानक S1S मॉडल का एक प्राथमिक उपमॉडल बनाते हैं, और ट्यूरिंग जॉइन और ट्यूरिंग रिड्यूसिबिलिटी के तहत बंद किए गए ω के प्रत्येक गैर-रिक्त संग्रह के लिए समान होते हैं। यह S1S निश्चित सेटों की सापेक्ष पुनरावर्तीता और एकरूपता से निम्नानुसार है:
- φ(s) (s के एक फ़ंक्शन के रूप में) की गणना φ के मापदंडों और φ(s) के मानों से की जा सकती है′) एस के एक सीमित सेट के लिए′ (इसका आकार φ के लिए एक नियतात्मक ऑटोमेटन में राज्यों की संख्या से घिरा हुआ है)।
- ∃S φ(S) के लिए एक गवाह k और S का एक सीमित टुकड़ा चुनकर प्राप्त किया जा सकता है′ का, और बार-बार एस का विस्तार करना′ जैसे कि प्रत्येक विस्तार के दौरान सर्वोच्च प्राथमिकता k है और विस्तार को k से ऊपर की प्राथमिकताओं को प्रभावित किए बिना S को संतुष्ट करते हुए S में पूरा किया जा सकता है (इन्हें केवल प्रारंभिक S के लिए अनुमति दी गई है)′). इसके अलावा, लेक्सिकोग्राफ़िक रूप से कम से कम सबसे छोटे विकल्पों का उपयोग करके, एक S1S सूत्र φ' है, जैसे कि φ'⇒φ और ∃S φ(S) ⇔∃!S φ'(S) (यानी एकरूपता; φ में मुक्त चर नहीं दिखाए जा सकते हैं; φ' केवल सूत्र φ) पर निर्भर करता है।

S2S के न्यूनतम मॉडल में बाइनरी स्ट्रिंग्स पर सभी नियमित भाषाएँ शामिल हैं। यह मानक मॉडल का एक प्रारंभिक उपमॉडल है, इसलिए यदि पेड़ों का एक S2S पैरामीटर-मुक्त निश्चित सेट गैर-रिक्त है, तो इसमें एक नियमित पेड़ शामिल है। एक नियमित भाषा को एक नियमित {0,1}-लेबल पूर्ण अनंत बाइनरी ट्री (स्ट्रिंग्स पर विधेय के साथ पहचाना गया) के रूप में भी माना जा सकता है। एक लेबल वाला पेड़ नियमित होता है यदि इसे प्रारंभिक शीर्ष के साथ शीर्ष-लेबल वाले परिमित निर्देशित ग्राफ को अनियंत्रित करके प्राप्त किया जा सकता है; प्रारंभिक शीर्ष से पहुंच योग्य ग्राफ़ में एक (निर्देशित) चक्र एक अनंत वृक्ष देता है। नियमित पेड़ों की इस व्याख्या और एन्कोडिंग के साथ, प्रत्येक सच्चा S2S वाक्य प्राथमिक फ़ंक्शन अंकगणित में पहले से ही सिद्ध हो सकता है। यह गैर-नियमित पेड़ हैं जिन्हें निर्धारण के लिए गैर-विधेयात्मक समझ की आवश्यकता हो सकती है (नीचे)। गणना योग्य संतुष्टि संबंध के साथ S1S (और संभवतः S2S) (मानक प्रथम क्रम भाग के साथ और बिना दोनों) के गैर-नियमित (यानी गैर-नियमित भाषाओं वाले) मॉडल हैं। हालाँकि, स्ट्रिंग के पुनरावर्ती सेट का सेट समझ और निर्धारण की विफलता के कारण S2S का मॉडल नहीं बनाता है।

S2S की निर्णायकता

निर्णायकता का प्रमाण यह दर्शाकर है कि प्रत्येक सूत्र एक गैर-नियतात्मक वृक्ष ऑटोमेटन द्वारा स्वीकृति के बराबर है (वृक्ष स्वचालन और अनंत-वृक्ष ऑटोमेटन देखें)। एक अनंत वृक्ष ऑटोमेटन जड़ से शुरू होता है और पेड़ की ओर बढ़ता है, और यदि प्रत्येक वृक्ष शाखा स्वीकार करती है तो इसे स्वीकार करती है। एक गैर-नियतात्मक ट्री ऑटोमेटन स्वीकार करता है कि क्या खिलाड़ी 1 के पास जीतने की रणनीति है, जहां खिलाड़ी 1 नए राज्यों की एक अनुमत (वर्तमान स्थिति और इनपुट के लिए) जोड़ी चुनता है (पी)₀,पी₁), जबकि खिलाड़ी 2 पी में संक्रमण के साथ शाखा चुनता है₀ यदि 0 चुना गया है और पी₁ अन्यथा। एक सह-नॉनडेटर्मिनिस्टिक ऑटोमेटन के लिए, सभी विकल्प खिलाड़ी 2 के अनुसार होते हैं, जबकि नियतात्मक के लिए, (पी)₀,पी₁) राज्य और इनपुट द्वारा तय किया गया है; और एक गेम ऑटोमेटन के लिए, दो खिलाड़ी शाखा और राज्य को सेट करने के लिए एक सीमित गेम खेलते हैं। किसी शाखा पर स्वीकृति शाखा पर अनंत बार देखी जाने वाली स्थितियों पर आधारित होती है; समता ऑटोमेटा यहाँ पर्याप्त रूप से सामान्य हैं।

सूत्रों को ऑटोमेटा में परिवर्तित करने के लिए, आधार मामला आसान है, और गैर-नियतत्ववाद अस्तित्वगत परिमाणकों के तहत समापन देता है, इसलिए हमें केवल पूरकता के तहत समापन की आवश्यकता है। समता खेलों की स्थितिगत निर्धारण का उपयोग करते हुए (जहां हमें पूर्वव्यापी समझ की आवश्यकता होती है), खिलाड़ी 1 जीतने वाली रणनीति की गैर-मौजूदगी एक खिलाड़ी 2 जीतने वाली रणनीति एस देती है, एक सह-नॉनडेटर्मिनिस्टिक ट्री ऑटोमेटन इसकी सुदृढ़ता की पुष्टि करता है। फिर ऑटोमेटन को नियतिवादी बनाया जा सकता है (जहां हमें राज्यों की संख्या में तेजी से वृद्धि मिलती है), और इस प्रकार एस का अस्तित्व एक गैर-नियतात्मक ऑटोमेटन द्वारा स्वीकृति से मेल खाता है।

निश्चयात्मकता: ZFC में, बोरेल खेल निश्चयात्मकता हैं, और Π के बूलियन संयोजनों के लिए निर्धारण प्रमाण हैं⁰₂ सूत्र (मनमाने वास्तविक मापदंडों के साथ) यहां एक रणनीति भी देते हैं जो केवल वर्तमान स्थिति और पेड़ की स्थिति पर निर्भर करती है। इसका प्रमाण प्राथमिकताओं की संख्या पर प्रेरण द्वारा है। मान लें कि k प्राथमिकताएँ हैं, सर्वोच्च प्राथमिकता k है, और k में खिलाड़ी 2 के लिए सही समता है। प्रत्येक स्थिति (वृक्ष स्थिति + स्थिति) के लिए कम से कम क्रमसूचक α (यदि कोई हो) निर्दिष्ट करें ताकि खिलाड़ी 1 की जीत हो सभी दर्ज की गई (एक या अधिक चरणों के बाद) प्राथमिकता k स्थितियों (यदि कोई हो) के साथ रणनीति जिसमें लेबल <α हो। यदि प्रारंभिक स्थिति को लेबल किया गया है तो खिलाड़ी 1 जीत सकता है: हर बार प्राथमिकता k स्थिति तक पहुंचने पर, क्रमसूचक कम हो जाता है, और इसके अलावा घटने के बीच, खिलाड़ी 1 k-1 प्राथमिकताओं के लिए एक रणनीति का उपयोग कर सकता है। यदि स्थिति लेबल रहित है तो खिलाड़ी 2 जीत सकता है: k-1 प्राथमिकताओं के निर्धारण के अनुसार, खिलाड़ी 2 के पास एक रणनीति होती है जो जीतती है या एक गैर-लेबल प्राथमिकता k स्थिति में प्रवेश करती है, जिस स्थिति में खिलाड़ी 2 फिर से उस रणनीति का उपयोग कर सकता है। रणनीति को स्थितिगत बनाने के लिए (k पर प्रेरण द्वारा), सहायक खेल खेलते समय, यदि दो चुनी गई स्थितीय रणनीतियाँ एक ही स्थिति में ले जाती हैं, तो निम्न α के साथ रणनीति जारी रखें, या उसी α के लिए (या खिलाड़ी 2 के लिए) कम प्रारंभिक स्थिति (ताकि हम एक रणनीति को कई बार सीमित रूप से बदल सकें)।

ऑटोमेटा निर्धारण: सह-नॉनडेटर्मिनिस्टिक ट्री ऑटोमेटा के निर्धारण के लिए, ω-ऑटोमेटा पर विचार करना, शाखा की पसंद को इनपुट के रूप में मानना, ऑटोमेटन का निर्धारण करना और नियतात्मक ट्री ऑटोमेटन के लिए इसका उपयोग करना पर्याप्त है। ध्यान दें कि यह गैर-नियतात्मक ट्री ऑटोमेटा के लिए काम नहीं करता है क्योंकि बाईं ओर जाने का निर्धारण (यानी s→s0) दाहिनी शाखा की सामग्री पर निर्भर हो सकता है; गैर-नियतिवाद के विपरीत, नियतिवादी वृक्ष ऑटोमेटा सटीक रूप से गैर-रिक्त सेटों को भी स्वीकार नहीं कर सकता है। एक गैर-नियतात्मक ω-ऑटोमेटन एम को निर्धारित करने के लिए (सह-नॉनडेटर्मिनिस्टिक के लिए, पूरक लें, यह ध्यान में रखते हुए कि नियतात्मक समता ऑटोमेटा पूरक के तहत बंद हैं), हम प्रत्येक नोड के साथ एम के संभावित राज्यों का एक सेट संग्रहीत करने और नोड निर्माण के लिए एक सफरा पेड़ का उपयोग कर सकते हैं। और उच्च प्राथमिकता वाले राज्यों तक पहुंचने के आधार पर विलोपन। विवरण के लिए देखें या। स्वीकृति की निर्णायकता: खाली पेड़ के एक गैर-नियतात्मक समता ऑटोमेटन द्वारा स्वीकृति एक परिमित ग्राफ जी पर एक समता खेल से मेल खाती है। उपरोक्त स्थितीय (जिसे स्मृतिहीन भी कहा जाता है) निर्धारण का उपयोग करते हुए, इसे एक परिमित खेल द्वारा अनुकरण किया जा सकता है जो तब समाप्त होता है जब हम एक तक पहुंचते हैं लूप, लूप में सर्वोच्च प्राथमिकता वाले राज्य के आधार पर जीतने की स्थिति के साथ। एक चतुर अनुकूलन एक अर्धबहुपद समय एल्गोरिथ्म देता है, जो बहुपद समय है जब प्राथमिकताओं की संख्या काफी कम होती है (जो आमतौर पर व्यवहार में होती है)।

पेड़ों का सिद्धांत: पेड़ों पर एमएसओ तर्क की निर्णायकता के लिए (यानी ग्राफ़ जो पेड़ हैं), यहां तक ​​​​कि पहले क्रम की वस्तुओं के लिए परिमितता और मॉड्यूलर गिनती क्वांटिफायर के साथ, हम गणनीय पेड़ों को पूर्ण बाइनरी पेड़ में एम्बेड कर सकते हैं और एस 2 एस की निर्णायकता का उपयोग कर सकते हैं। उदाहरण के लिए, एक नोड s के लिए, हम उसके बच्चों को s1, s01, s001 इत्यादि द्वारा दर्शा सकते हैं। अनगिनत पेड़ों के लिए, हम शेलह-स्टुप प्रमेय (नीचे) का उपयोग कर सकते हैं। हम कार्डिनलिटी ω वाले सेट प्रथम क्रम ऑब्जेक्ट के लिए एक विधेय भी जोड़ सकते हैं₁, और कार्डिनैलिटी के लिए विधेय ω₂, और इसी तरह अनंत नियमित कार्डिनल्स के लिए। बंधे हुए पेड़ की चौड़ाई के ग्राफ़ को पेड़ों का उपयोग करके व्याख्या की जा सकती है, और किनारों पर विधेय के बिना यह बंधे हुए क्लिक चौड़ाई के ग्राफ़ पर भी लागू होता है।

S2S को अन्य निर्णायक सिद्धांतों के साथ जोड़ना

अद्वैत सिद्धांतों के वृक्ष विस्तार: शेलह-स्टूप प्रमेय द्वारा, यदि एक मोनैडिक रिलेशनल मॉडल एम निर्णायक है, तो उसका वृक्ष समकक्ष भी ऐसा ही है। उदाहरण के लिए, (औपचारिकरण का मॉड्यूलो विकल्प) S2S, {0,1} का वृक्ष समकक्ष है। ट्री समकक्ष में, पहले क्रम की वस्तुएं विस्तार द्वारा क्रमित एम के तत्वों के परिमित अनुक्रम हैं, और एक एम-संबंध पी_i पी पर मैप किया गया है_i(सीईओ₁,...,सीईओ_k) ⇔ पी_i(डी₁,...,डी_k) पी के साथ_i' अन्यथा गलत (डी_j∈M, और v, M के तत्वों का एक (संभवतः खाली) अनुक्रम है)। प्रमाण S2S निर्णायकता प्रमाण के समान है। प्रत्येक चरण में, एक (नॉनडेटर्मिनिस्टिक) ऑटोमेटन को इनपुट के रूप में एम ऑब्जेक्ट्स (संभवतः दूसरे क्रम) का एक टुपल मिलता है, और एक एम फॉर्मूला निर्धारित करता है कि किस राज्य संक्रमण की अनुमति है। खिलाड़ी 1 (जैसा कि ऊपर है) एक मैपिंग चाइल्ड⇒स्टेट चुनता है जिसे सूत्र (वर्तमान स्थिति को देखते हुए) द्वारा अनुमति दी जाती है, और खिलाड़ी 2 जारी रखने के लिए चाइल्ड (नोड का) चुनता है। एक गैर-नियतात्मक ऑटोमेटन द्वारा अस्वीकृति देखने के लिए, प्रत्येक (नोड, राज्य) के लिए (बच्चे, राज्य) जोड़े का एक सेट चुनें, जैसे कि हर विकल्प के लिए, कम से कम एक जोड़े को हिट किया जाए, और इस तरह कि सभी परिणामी पथ आगे बढ़ें अस्वीकृति के लिए.

एक मोनैडिक सिद्धांत को प्रथम क्रम सिद्धांत के साथ जोड़ना: फ़ेफ़रमैन-वॉथ प्रमेय निम्नानुसार विस्तारित/लागू होता है। यदि एम एक एमएसओ मॉडल है और एन एक प्रथम क्रम मॉडल है, तो एम एक (थ्योरी (एम), थ्योरी (एन)) ओरेकल मशीन के सापेक्ष निर्णायक रहता है, भले ही एम को सभी कार्यों एम → एन के साथ संवर्धित किया गया हो जहां एम की पहचान की जाती है इसकी पहली वस्तुएं, और प्रत्येक s∈M के लिए हम N की एक असंयुक्त प्रतिलिपि का उपयोग करते हैं, भाषा को तदनुसार संशोधित किया जाता है। उदाहरण के लिए, यदि N है ($\mathbb {R}$,0,+,⋅), हम बता सकते हैं ∀(function f) ∀s ∃r∈N_s एफ(एस)+_Nsआर = 0 उप>एन_s</उप>. यदि M S2S है (या अधिक सामान्यतः, कुछ मोनैडिक मॉडल का वृक्ष समकक्ष), तो ऑटोमेटा अब N-सूत्रों का उपयोग कर सकता है, और इस प्रकार f:M→N को परिवर्तित कर सकता है^kM सेट के टुपल में। असम्बद्धता आवश्यक है क्योंकि अन्यथा समानता वाले प्रत्येक अनंत N के लिए, विस्तारित S2S या केवल WS1S अनिर्णीत है। इसके अलावा, (संभवतः अपूर्ण) सिद्धांत टी के लिए, सिद्धांत टी^{टी के एम-उत्पादों का एम (थ्योरी (एम), टी) ओरेकल के सापेक्ष निर्णय योग्य है, जहां टी का एक मॉडलM एक मनमाना असंयुक्त मॉडल N का उपयोग करता है_s प्रत्येक s∈M के लिए T का (जैसा कि ऊपर बताया गया है, M एक MSO मॉडल है; थ्योरी(N_s) एस पर निर्भर हो सकता है)। इसका प्रमाण सूत्र जटिलता पर प्रेरण द्वारा है। चलो वी_s निःशुल्क एन की सूची बनें_s यदि फ़ंक्शन f मुफ़्त है, तो f(s) सहित चर। प्रेरण द्वारा, कोई यह दर्शाता है कि v_s इसका उपयोग केवल |v के साथ एन-सूत्रों के एक सीमित सेट के माध्यम से किया जाता है_s| मुक्त चर. इस प्रकार, हम जो संभव है उसका उत्तर देने के लिए एन (या टी) का उपयोग करके सभी संभावित परिणामों की मात्रा निर्धारित कर सकते हैं, और एक सूची संभावनाओं (या बाधाओं) को देखते हुए, एम में एक संबंधित वाक्य तैयार कर सकते हैं।}

S2S के एक्सटेंशन में कोडिंग: स्ट्रिंग्स पर प्रत्येक निर्णायक विधेय को एन्कोडेड विधेय के साथ S2S (यहां तक ​​​​कि उपरोक्त एक्सटेंशन के साथ) की निर्णायकता के लिए एन्कोड किया जा सकता है (रैखिक समय एन्कोडिंग और डिकोडिंग के साथ)। प्रमाण: एक गैर-नियतात्मक अनंत वृक्ष ऑटोमेटन को देखते हुए, हम परिमित बाइनरी लेबल वाले पेड़ों के सेट को विभाजित कर सकते हैं (जिन पर ऑटोमेटन संचालित हो सकता है) को कई वर्गों में विभाजित किया जा सकता है, जैसे कि यदि एक पूर्ण अनंत बाइनरी ट्री समान श्रेणी के पेड़ों से बना हो सकता है, स्वीकृति केवल वर्ग और प्रारंभिक स्थिति पर निर्भर करती है (अर्थात ऑटोमेटन पेड़ में प्रवेश करता है)। (पम्पिंग लेम्मा के साथ एक मोटे समानता पर ध्यान दें।) उदाहरण के लिए (एक समता ऑटोमेटन के लिए), पेड़ों को एक ही वर्ग में असाइन करें यदि उनके पास एक ही विधेय है जो दिए गए प्रारंभिक_स्टेट और (स्टेट, उच्चतम_प्राथमिकता_पहुंचे हुए) जोड़े का क्यू देता है तो खिलाड़ी 1 ( यानी गैर-नियतिवाद) एक साथ सभी शाखाओं को Q के तत्वों के अनुरूप होने के लिए मजबूर कर सकता है। अब, प्रत्येक k के लिए, पेड़ों का एक सीमित सेट चुनें (कोडिंग के लिए उपयुक्त) जो कि ऑटोमेटा 1-k के लिए एक ही वर्ग से संबंधित है, वर्ग की पसंद के अनुरूप के पार किसी विधेय को एनकोड करने के लिए, कुछ बिट्स को k=1 का उपयोग करके एनकोड करें, फिर अधिक बिट्स को k=2 का उपयोग करके एनकोड करें, इत्यादि।

संदर्भ

Additional reference:
Weyer, Mark (2002). "Decidability of S1S and 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.