S2S (mathematics)
गणित में, एस2एस दो उत्तराधिकारियों के साथ मठवासी द्वितीय क्रम सिद्धांत है। यह ज्ञात सबसे अभिव्यंजक प्राकृतिक निर्णायक सिद्धांतों में से एक है, जिसमें कई निर्णायक सिद्धांतों की व्याख्या एस2एस में की जा सकती है। इसकी निर्णायकता 1969 में राबिन द्वारा साबित की गई थी। बुनियादी गुण एस2एस की प्रथम क्रम की वस्तुएं परिमित द्विआधारी तार हैं। दूसरे क्रम की वस्तुएं परिमित द्विआधारी तारों के मनमाने समुच्चय (या यूनरी प्रेडिकेट्स) हैं। S2S में स्ट्रिंग्स पर फंक्शन s → s0 और s → s1 होते हैं, और s ω S (समकक्ष, S (s)) का अनुमान लगाते हैं जिसका अर्थ है स्ट्रिंग s सेट S से संबंधित है। कुछ गुण और परंपराएँः डिफ़ॉल्ट रूप से, छोटे अक्षर प्रथम क्रम की वस्तुओं को संदर्भित करते हैं, और बड़े अक्षर दूसरे क्रम की वस्तुओं को संदर्भित करते हैं। सेटों का समावेश एस2एस को दूसरा क्रम बनाता है, जिसमें "मोनाडिक" के> 1 के लिए के-एरी विधेय चर की अनुपस्थिति का संकेत देता है। स्ट्रिंग्स s और t के संयोजन को st द्वारा दर्शाया जाता है, और यह आम तौर पर S2S में उपलब्ध नहीं है, यहाँ तक कि s → 0s भी नहीं है। स्ट्रिंग्स के बीच उपसर्ग संबंध परिभाषित किया जा सकता है। समानता आदिम है, या इसे एस = टी. टी. आई. टी. एस (एस (एस) टी. एस (टी)) और एस = टी. टी. आई. टी. एस (एस (एस) टी (एस) के रूप में परिभाषित किया जा सकता है। तारों के स्थान पर, कोई भी (उदाहरण के लिए) प्राकृतिक संख्याओं का उपयोग कर सकता है जिसमें n → 2n + 1 और n → 2n + 2 हैं लेकिन कोई अन्य संचालन नहीं है। सभी द्विआधारी तारों के समूह को क्लेन स्टार का उपयोग करके {0,1} * द्वारा दर्शाया जाता है। {0,1} * के मनमाने उपसमुच्चय को कभी-कभी पेड़ों के साथ पहचाना जाता है, विशेष रूप से एक {0,1}-लेबल वाले पेड़ {0,1} * के रूप में; {0,1} * एक पूर्ण अनंत द्विआधारी पेड़ बनाता है। सूत्र जटिलता के लिए, स्ट्रिंग्स पर उपसर्ग संबंध को आमतौर पर प्रथम क्रम के रूप में माना जाता है। इसके बिना, सभी सूत्र Δ12 सूत्रों के बराबर नहीं होंगे। एस2एस में व्यक्त होने वाले गुणों के लिए (सभी द्विआधारी तारों के समूह को एक वृक्ष के रूप में देखते हुए), प्रत्येक नोड के लिए, केवल ओ (1) बिट्स को बाएं उप-वृक्ष और दाएं उप-वृक्ष और बाकी के बीच संचारित किया जा सकता है (संचार जटिलता देखें)। एक निश्चित k के लिए, स्ट्रिंग से k तक एक फलन (अर्थात। k) से नीचे की प्राकृतिक संख्याओं को एक एकल समूह द्वारा कूटबद्ध किया जा सकता है। इसके अलावा, s, t ुण s01t जहां t, t के प्रत्येक वर्ण को दोगुना करता है, वह इंजेक्टिव है, और s ुण {s01t: t णी {0,1} *} S2S परिभाषित है। इसके विपरीत, एक संचार जटिलता तर्क द्वारा, एस1एस (नीचे) में सेटों की एक जोड़ी एक एकल सेट द्वारा कूटबद्ध नहीं है। एस2एस की कमजोरियाँः कमजोर एस2एस (डब्ल्यूएस2एस) के लिए सभी सेटों को सीमित होने की आवश्यकता होती है (ध्यान दें कि कोनिग के लेम्मा का उपयोग करके एस2एस में परिमितता व्यक्त की जा सकती है)। एस1एस को इस आवश्यकता से प्राप्त किया जा सकता है कि '1' स्ट्रिंग्स में दिखाई न दे, और डब्ल्यूएस1एस को भी परिमितता की आवश्यकता होती है। यहां तक कि डब्ल्यू. एस. 1. एस. भी प्रेसबर्गर अंकगणित की व्याख्या 2 की शक्तियों के लिए एक विधेय के साथ कर सकता है, क्योंकि सेट का उपयोग निश्चित जोड़ के साथ असीमित द्विआधारी संख्याओं का प्रतिनिधित्व करने के लिए किया जा सकता है। निर्णय जटिलता S2S निर्णायक है, और S2S, S1S, WS2S, WS1S में से प्रत्येक में घातांक के रैखिक रूप से बढ़ते ढेर के अनुरूप एक अनुपूरक निर्णय जटिलता है। निचली सीमा के लिए, यह σ11 WS1S वाक्यों पर विचार करने के लिए पर्याप्त है। एक एकल द्वितीय क्रम परिमापक का उपयोग एक अंकगणितीय (या अन्य) गणना का प्रस्ताव करने के लिए किया जा सकता है, जिसे प्रथम क्रम परिमापक का उपयोग करके सत्यापित किया जा सकता है यदि हम परीक्षण कर सकते हैं कि कौन सी संख्याएँ बराबर हैं। इसके लिए, यदि हम उचित रूप से संख्या 1. m को कूटबद्ध करते हैं, तो हम द्विआधारी प्रतिनिधित्व i1i2.im के साथ एक संख्या को i1 1 i2 2 के रूप में कूटबद्ध कर सकते हैं। गार्ड के परीक्षण को विलय करके और परिवर्तनीय नामों का पुनः उपयोग करके, बिट्स की संख्या घातांक की संख्या में रैखिक होती है। ऊपरी सीमा के लिए, निर्णय प्रक्रिया (नीचे) का उपयोग करते हुए, k-गुना परिमापक प्रत्यावर्तन के साथ वाक्यों को वाक्य की लंबाई (समान स्थिरांक के साथ) के k + O (1)-गुना घातांक के अनुरूप समय में तय किया जा सकता है। स्वयंसिद्धीकरण डब्ल्यू. एस. 2. एस. को कुछ बुनियादी गुणों और प्रेरण योजना के माध्यम से स्वयंसिद्ध किया जा सकता है। एस2एस को आंशिक रूप से इस प्रकार स्वयंसिद्ध किया जा सकता हैः (1) एच. ई.! एस. टी. टी. (टी0  ऒत्त एस1  ऒत्त एस) (खाली स्ट्रिंग, जिसे ε द्वारा दर्शाया गया है; एच. ई. एस. का अर्थ है "अद्वितीय एस") (2) एस. टी. आई. एस., टी. आई. आई. आई. यू. एल. {0,1} जे. यू. एल. {0,1} (एस. आई. = टी. जे. ए. डी. एस. = टी. आई. आई. = जे) (आई. और जे. का उपयोग एक संक्षिप्त नाम है; आई. = जे. के लिए, 0 1 के बराबर नहीं है) (3) एस. टी. आई. एस. (एस. (ई.) एस. (एस.) एस. (एस.) एस. (एस.) एस. हमेशा की तरह, यदि φ में मुक्त चर नहीं दिखाए गए हैं, तो हम स्वयंसिद्ध का सार्वभौमिक समापन लेते हैं। यदि समानता विधेयकों के लिए आदिम है, तो कोई भी विस्तारता S = T ष्ण (s) ष्ण (s) भी जोड़ता है। चूँकि हमारी समझ है, प्रेरण एक योजना के बजाय एक कथन हो सकता है। एस1एस का अनुरूप स्वयंसिद्धीकरण पूरा हो गया है। हालाँकि, एस2एस के लिए, पूर्णता खुली है (2021 तक)। जबकि एस1एस में एकरूपता है, कोई एस2एस परिभाषित (यहां तक कि मापदंडों की अनुमति देने वाला) विकल्प कार्य नहीं है जो एक गैर-खाली सेट एस को एस का एक तत्व देता है, और समझ योजना को आमतौर पर पसंद के स्वयंसिद्ध के विभिन्न रूपों के साथ संवर्धित किया जाता है। हालांकि, (1)-(4) तब पूरा होता है जब कुछ समानता खेलों के लिए एक निर्धारकता योजना के साथ बढ़ाया जाता है। S2S को Π13 वाक्यों द्वारा भी स्वयंसिद्ध किया जा सकता है (एक आदिम के रूप में स्ट्रिंग पर उपसर्ग संबंध का उपयोग करते हुए)। हालाँकि, यह परिमित रूप से स्वयंसिद्ध नहीं है, और न ही इसे σ13 वाक्यों द्वारा स्वयंसिद्ध किया जा सकता है, भले ही हम प्रेरण योजना और अन्य वाक्यों का एक सीमित सेट जोड़ते हैं (यह Π12-CA0 से इसके संबंध से मिलता है)। S2S से संबंधित सिद्धांत प्रत्येक परिमित k के लिए, त्रि-चौड़ाई ≤ k (और एक संबंधित वृक्ष अपघटन) के साथ गणना योग्य ग्राफ का monadic द्वितीय क्रम (MSO) सिद्धांत S2S में व्याख्यायित किया जा सकता है (देखें Courcelle का प्रमेय)। उदाहरण के लिए, पेड़ों का एमएसओ सिद्धांत (ग्राफ के रूप में) या श्रृंखला-समानांतर ग्राफ निर्णायक है। यहाँ (अर्थात। बंधे हुए वृक्ष की चौड़ाई के लिए), हम शीर्षों (या किनारों) के एक समूह के लिए परिमितता परिमापक की व्याख्या भी कर सकते हैं, और एक निश्चित पूर्णांक में एक सेट मॉड्यूलो में शीर्षों (या किनारों) को भी गिन सकते हैं। अनगिनत ग्राफों को अनुमति देने से सिद्धांत नहीं बदलता है। इसके अलावा, तुलना के लिए, S1S बंधे हुए पथ चौड़ाई के जुड़े ग्राफ की व्याख्या कर सकता है। इसके विपरीत, असीमित त्रि-चौड़ाई के ग्राफ के प्रत्येक सेट के लिए, इसका अस्तित्व (अर्थात। 11) एम. एस. ओ. सिद्धांत अनिश्चित है यदि हम दोनों शीर्षों और किनारों पर विधेय की अनुमति देते हैं। इस प्रकार, एक अर्थ में, एस2एस की निर्णायकता सबसे अच्छी संभव है। असीम त्रि-चौड़ाई वाले ग्राफों में बड़े ग्रिड माइनर होते हैं, जिनका उपयोग ट्यूरिंग मशीन का अनुकरण करने के लिए किया जा सकता है। एस2एस में कमी से, गणना योग्य आदेशों का एमएसओ सिद्धांत निर्णायक है, जैसा कि उनके क्लीन-ब्रोवर आदेशों के साथ गणना योग्य पेड़ों का एमएसओ सिद्धांत है। हालाँकि, (, <) का एम. एस. ओ. सिद्धांत अनिश्चित है। ऑर्डिनल्स <ω2 का एमएसओ सिद्धांत निर्णायक है; ω2 के लिए निर्णायकता जेडएफसी से स्वतंत्र है (कॉन (जेडएफसी + कमजोर रूप से कॉम्पैक्ट कार्डिनल) मानते हुए)। इसके अलावा, एक ऑर्डिनल को ऑर्डिनल्स पर मोनैडिक सेकंड ऑर्डर लॉजिक का उपयोग करके परिभाषित किया जा सकता है यदि इसे ऑर्डिनल जोड़ और गुणन द्वारा परिभाषित नियमित कार्डिनल्स से प्राप्त किया जा सकता है। एस2एस कुछ मोडल लॉजिक्स की निर्णायकता के लिए उपयोगी है, जिसमें क्रिप्के शब्दार्थ स्वाभाविक रूप से पेड़ों की ओर ले जाता है। S2S + U (या सिर्फ S1S + U) अनिश्चित है यदि U अनबाउंडिंग क्वांटिफायर है-UX φ (X) यदि f φ (X) कुछ मनमाने ढंग से बड़े परिमित X के लिए धारण करता है। हालाँकि, WS2S + U, अनंत पथों पर परिमाणीकरण के साथ भी, निर्णायक है, यहां तक कि S2S उप-सूत्रों के साथ भी जिनमें U नहीं है। सूत्र जटिलता द्विआधारी तारों का एक समूह एस2एस में परिभाषित किया जा सकता है यदि यह नियमित है (अर्थात। एक नियमित भाषा बनाता है)। एस1एस में, सेट पर एक (यूनरी) विधेय (पैरामीटर-मुक्त) परिभाषित करने योग्य है यदि यह एक ω-नियमित भाषा है। एस2एस के लिए, उन सूत्रों के लिए जो अपने मुक्त चर का उपयोग केवल स्ट्रिंग पर करते हैं जिसमें 1 नहीं होता है, अभिव्यक्ति एस1एस के लिए समान है। प्रत्येक S2S सूत्र के लिए φ (S1,., Sk), (k मुक्त चर के साथ) और द्विआधारी तारों के परिमित वृक्ष T, φ (S1 θ T,., Sk θ T) की गणना समय रैखिक में |T। में की जा सकती है (देखें कोरसेल का प्रमेय), लेकिन जैसा कि ऊपर उल्लेख किया गया है, ओवरहेड को सूत्र आकार में घातीय रूप से दोहराया जा सकता है (अधिक सटीक रूप से, समय है)। S1S के लिए, प्रत्येक सूत्र एक Δ11 सूत्र के बराबर है, और Π02 अंकगणितीय सूत्रों के बूलियन संयोजन के बराबर है। इसके अलावा, प्रत्येक S1S सूत्र सूत्र के मापदंडों के एक संबंधित ω-स्वचालित द्वारा स्वीकृति के बराबर है। ऑटोमेटन एक नियतात्मक समता ऑटोमेटन हो सकता हैः एक समता ऑटोमेटन की प्रत्येक अवस्था के लिए एक पूर्णांक प्राथमिकता होती है, और यह स्वीकार करता है कि असीम रूप से देखी जाने वाली उच्चतम प्राथमिकता विषम (वैकल्पिक रूप से, सम) होती है। एस2एस के लिए, ट्री ऑटोमेटा (नीचे) का उपयोग करते हुए, प्रत्येक सूत्र एक Δ12 सूत्र के बराबर है। इसके अलावा, प्रत्येक एस2एस सूत्र केवल चार परिमापकों के साथ एक सूत्र के बराबर है, एच. ई. एस. टी. टी. एस. टी. टी. (यह मानते हुए कि हमारे औपचारिकरण में उपसर्ग संबंध और उत्तराधिकारी कार्य दोनों हैं)। एस1एस के लिए, तीन परिमापक (एच. ई. एस. आई. टी. एस. एच. टी.) पर्याप्त हैं, और डब्ल्यू. एस. 2एस और डब्ल्यू. एस. 1एस के लिए, दो परिमापक (एच. ई. एस. आई. टी.) पर्याप्त हैं; डब्ल्यू. एस. 2एस और डब्ल्यू. एस. 1एस के लिए यहाँ उपसर्ग संबंध की आवश्यकता नहीं है। हालांकि, मुक्त द्वितीय क्रम चर के साथ, प्रत्येक S2S सूत्र को केवल Π11 ट्रांसफाइनाइट रिकर्शन के माध्यम से द्वितीय क्रम अंकगणित में व्यक्त नहीं किया जा सकता है (विपरीत गणित देखें)। RCA0 + (स्कीमा) {τ: τ एक सच्चा S2S वाक्य है} (स्कीमा) के बराबर है {τ: τ एक Π13 वाक्य है जो Π12-CA0} में सिद्ध किया जा सकता है। एक आधार सिद्धांत पर, योजनाएँ (स्किमा ओवर के) के समतुल्य हैं। सीमित प्रेरण के कारण, Π12-CA0 यह साबित नहीं करता है कि सभी सत्य (मानक निर्णय प्रक्रिया के तहत) Π13 S2S कथन वास्तव में सत्य हैं, भले ही ऐसा प्रत्येक वाक्य Π12-CA0 सिद्ध करने योग्य हो। इसके अलावा, द्विआधारी तार एस और टी के दिए गए सेट, निम्नलिखित समतुल्य हैंः (1) टी एस से संगणनीय द्विआधारी तार बहुपद समय के कुछ सेट से एस 2 एस परिभाषित किया जा सकता है. (2) टी की गणना किसी खेल के लिए जीतने की स्थिति के सेट से की जा सकती है जिसका भुगतान Π02 (एस) सेट का एक सीमित बूलियन संयोजन है। (3) T को S से अंकगणितीय μ-कैलकुलस (अंकगणितीय सूत्र + न्यूनतम निश्चित-बिंदु तर्क) में परिभाषित किया जा सकता है (4) T सबसे कम β-मॉडल में है (यानी। एक ω-मॉडल जिसका सेट-सैद्धांतिक समकक्ष सकर्मक है) जिसमें S होता है और जो Π12-CA0 के सभी Π13 परिणामों को संतुष्ट करता है। एस1एस और एस2एस के मॉडल मानक मॉडल (जो एस1एस और एस2एस के लिए अद्वितीय एमएसओ मॉडल है) के अलावा, एस1एस और एस2एस के लिए अन्य मॉडल हैं, जो डोमेन के सभी सबसेट के बजाय कुछ का उपयोग करते हैं (हेंकिन शब्दार्थ देखें)। प्रत्येक S-ω के लिए, S में पुनरावर्ती सेट मानक S1S मॉडल का एक प्राथमिक उप-मॉडल बनाते हैं, और ट्यूरिंग जॉइन और ट्यूरिंग रिड्युसिबिलिटी के तहत बंद ω के उपसमुच्चय के प्रत्येक गैर-खाली संग्रह के लिए समान होते हैं। यह S1S परिभाषित समुच्चयों और एकरूपता की सापेक्ष पुनरावृत्ति से होता हैः-φ (s) (s के एक फलन के रूप में) की गणना φ के मापदंडों और s के एक सीमित समुच्चय के लिए φ (s) के मानों से की जा सकती है (इसके आकार के साथ φ के लिए एक निर्धारक स्वचालित में अवस्थाओं की संख्या से घिरा हुआ है)। - HE S φ (S) के लिए एक गवाह k और S के S के एक सीमित टुकड़े को चुनकर प्राप्त किया जा सकता है, और बार-बार S का विस्तार इस तरह से किया जा सकता है कि प्रत्येक विस्तार के दौरान सर्वोच्च प्राथमिकता k हो और विस्तार को k से ऊपर की प्राथमिकताओं को हिट किए बिना S को संतुष्ट करने में पूरा किया जा सके (इन्हें केवल प्रारंभिक S के लिए अनुमति दी जाती है)। इसके अलावा, लेक्सिकोग्राफिक रूप से सबसे कम छोटे विकल्पों का उपयोग करके, एक S1S सूत्र φ 'ऐसा है कि φ' ⇒φ और HE S φ (S) φ! S φ '(S) (यानी। एकरूपता; φ में मुक्त चर नहीं दिखाए जा सकते हैं; φ 'केवल सूत्र φ पर निर्भर करता है)। एस2एस के न्यूनतम मॉडल में द्विआधारी तार पर सभी नियमित भाषाएँ शामिल हैं। यह मानक मॉडल का एक प्राथमिक उप-मॉडल है, इसलिए यदि पेड़ों का एक एस2एस पैरामीटर-मुक्त परिभाषित सेट खाली नहीं है, तो इसमें एक नियमित पेड़ शामिल है। एक नियमित भाषा को एक नियमित {0,1}-लेबल पूर्ण अनंत द्विआधारी वृक्ष (तार पर विधेय के साथ पहचाना जाता है) के रूप में भी माना जा सकता है। एक लेबल वाला वृक्ष नियमित होता है यदि इसे प्रारंभिक शीर्ष के साथ एक शीर्ष-लेबल वाले परिमित निर्देशित ग्राफ को उतारकर प्राप्त किया जा सकता है; प्रारंभिक शीर्ष से पहुँचने योग्य ग्राफ में एक (निर्देशित) चक्र एक अनंत वृक्ष देता है। नियमित वृक्षों की इस व्याख्या और संकेतन के साथ, प्रत्येक वास्तविक S2S वाक्य पहले से ही प्राथमिक फलन अंकगणित में सिद्ध हो सकता है। यह गैर-नियमित पेड़ हैं जिन्हें निर्धारण के लिए गैर-अनुमानित समझ की आवश्यकता हो सकती है (नीचे)। गैर-नियमित हैं (अर्थात। एक संगणनीय संतुष्टि संबंध के साथ एस1एस (और संभवतः एस2एस) (मानक प्रथम क्रम भाग के साथ और बिना दोनों) के मॉडल। हालाँकि, स्ट्रिंग्स के पुनरावर्ती सेट का सेट समझ और निर्धारण की विफलता के कारण S2S का मॉडल नहीं बनाता है। एस2एस की निर्णायकता का प्रमाण यह दिखाना है कि प्रत्येक सूत्र एक गैर-निर्धारक ट्री ऑटोमेटन द्वारा स्वीकृति के बराबर है (ट्री ऑटोमेटन और अनंत-ट्री ऑटोमेटन देखें)। एक अनंत ट्री ऑटोमेटन जड़ से शुरू होता है और पेड़ को ऊपर ले जाता है, और पेड़ की हर शाखा द्वारा स्वीकार किए गए आई. एफ. एफ. को स्वीकार करता है। एक गैर-निर्धारक ट्री ऑटोमेटन स्वीकार करता है कि यदि खिलाड़ी 1 के पास जीतने की रणनीति है, जहां खिलाड़ी 1 नई अवस्थाओं (पी0, पी1) की एक अनुमत (वर्तमान स्थिति और इनपुट के लिए) जोड़ी का चयन करता है, जबकि खिलाड़ी 2 शाखा का चयन करता है, जिसमें पी0 में संक्रमण के साथ यदि 0 चुना जाता है और पी1 अन्यथा। एक सह-अनिर्धारित स्वचालित के लिए, सभी विकल्प खिलाड़ी 2 द्वारा होते हैं, जबकि नियतात्मक के लिए, (पी0, पी1) राज्य और इनपुट द्वारा तय किया जाता है; और एक खेल स्वचालित के लिए, दोनों खिलाड़ी शाखा और राज्य को निर्धारित करने के लिए एक सीमित खेल खेलते हैं। एक शाखा पर स्वीकृति शाखा पर असीम रूप से अक्सर देखी जाने वाली अवस्थाओं पर आधारित होती है; समानता स्वचालित यहाँ पर्याप्त रूप से सामान्य हैं। सूत्रों को स्वचालित में परिवर्तित करने के लिए, आधार मामला आसान है, और गैर-निर्धारणवाद अस्तित्वगत परिमापकों के तहत समापन देता है, इसलिए हमें केवल पूरक के तहत समापन की आवश्यकता है। समानता खेलों के स्थितिगत निर्धारण का उपयोग करते हुए (जहां हमें अभेद्य समझ की आवश्यकता होती है), खिलाड़ी 1 की जीतने की रणनीति का गैर-अस्तित्व एक खिलाड़ी को 2 जीतने की रणनीति एस देता है, जिसमें एक सह-अनिर्धारित ट्री ऑटोमेटन इसकी मजबूती को सत्यापित करता है। ऑटोमेटन को तब नियतात्मक बनाया जा सकता है (जहां हमें अवस्थाओं की संख्या में घातीय वृद्धि मिलती है), और इस प्रकार एस का अस्तित्व एक गैर-नियतात्मक ऑटोमेटन द्वारा स्वीकृति के अनुरूप है। निर्धारणः ZFC में, बोरेल खेल निर्धारित किए जाते हैं, और Π02 सूत्रों (मनमाने वास्तविक मापदंडों के साथ) के बूलियन संयोजन के लिए निर्धारण प्रमाण भी यहां एक रणनीति देता है जो केवल वर्तमान स्थिति और पेड़ में स्थिति पर निर्भर करता है। इसका प्रमाण प्राथमिकताओं की संख्या को शामिल करके है। मान लीजिए कि के प्राथमिकताएँ हैं, जिसमें सर्वोच्च प्राथमिकता के है, और उस के में खिलाड़ी 2 के लिए सही समानता है। प्रत्येक स्थिति (वृक्ष स्थिति + राज्य) के लिए कम से कम क्रमिक α (यदि कोई हो) इस तरह से निर्धारित करें कि खिलाड़ी 1 के पास सभी दर्ज (एक या अधिक चरणों के बाद) प्राथमिकता के पदों (यदि कोई हो) के साथ एक जीत की रणनीति हो जिसमें लेबल <α हो। खिलाड़ी 1 जीत सकता है यदि प्रारंभिक स्थिति को लेबल किया जाता हैः हर बार एक प्राथमिकता के राज्य तक पहुँचने पर, क्रम को कम कर दिया जाता है, और इसके अलावा कमी के बीच, खिलाड़ी 1 के-1 प्राथमिकताओं के लिए एक रणनीति का उपयोग कर सकता है। खिलाड़ी 2 जीत सकता है यदि स्थिति बिना लेबल वाली हैः के-1 प्राथमिकताओं के निर्धारण से, खिलाड़ी 2 के पास एक रणनीति होती है जो एक बिना लेबल वाली प्राथमिकता के स्थिति में जीतती है या प्रवेश करती है, जिस स्थिति में खिलाड़ी 2 फिर से उस रणनीति का उपयोग कर सकता है। रणनीति को स्थितिजन्य बनाने के लिए (के पर शामिल करके), सहायक खेल खेलते समय, यदि दो चुनी हुई स्थितिगत रणनीतियाँ एक ही स्थिति की ओर ले जाती हैं, तो निम्न α के साथ रणनीति के साथ जारी रखें, या उसी α (या खिलाड़ी 2 के लिए) निम्न प्रारंभिक स्थिति के लिए (ताकि हम एक रणनीति को कई बार सीमित रूप से बदल सकें)। स्वचालित निर्धारणः सह-गैर-निर्धारक वृक्ष स्वचालित के निर्धारण के लिए, ω-स्वचालित पर विचार करना पर्याप्त है, शाखा चयन को इनपुट के रूप में मानना, स्वचालित को निर्धारित करना, और निर्धारक वृक्ष स्वचालित के लिए इसका उपयोग करना। ध्यान दें कि यह बाएं जाने के निर्धारण के रूप में गैर-निर्धारक ट्री ऑटोमेटा के लिए काम नहीं करता है (यानी। s → s0) सही शाखा की सामग्री पर निर्भर कर सकता है; गैर-निर्धारणवाद के विपरीत, नियतात्मक ट्री ऑटोमेटा सटीक रूप से गैर-खाली सेट भी स्वीकार नहीं कर सकता है। एक गैर-नियतात्मक ω-स्वचालित M को निर्धारित करने के लिए (सह-नियतात्मक के लिए, पूरक लें, यह देखते हुए कि नियतात्मक समानता स्वचालित पूरक के तहत बंद हैं), हम प्रत्येक नोड के साथ एक सफरा ट्री का उपयोग कर सकते हैं जो M की संभावित स्थितियों के एक सेट को संग्रहीत करता है, और उच्च प्राथमिकता वाले राज्यों तक पहुंचने के आधार पर नोड निर्माण और विलोपन। विवरण के लिए, देखें या। स्वीकृति की निर्णायकताः खाली पेड़ की गैर-निर्धारक समानता स्वचालित द्वारा स्वीकृति एक सीमित ग्राफ जी पर एक समानता खेल से मेल खाती है। उपरोक्त स्थितिगत (जिसे स्मृतिहीन भी कहा जाता है) निर्धारण का उपयोग करके, इसे एक सीमित खेल द्वारा अनुकरण किया जा सकता है जो लूप में उच्चतम प्राथमिकता स्थिति के आधार पर जीतने की स्थिति के साथ एक लूप तक पहुंचने पर समाप्त होता है। एक चतुर अनुकूलन एक अर्ध-बहुपद समय एल्गोरिथ्म देता है, जो बहुपद समय होता है जब प्राथमिकताओं की संख्या काफी कम होती है (जो आमतौर पर व्यवहार में होती है)। पेड़ों का सिद्धांतः पेड़ों पर एमएसओ तर्क की निर्णायकता के लिए (अर्थात। ग्राफ जो ट्री हैं), यहां तक कि प्रथम क्रम की वस्तुओं के लिए परिमितता और मॉड्यूलर काउंटिंग क्वांटिफायर के साथ, हम गणना योग्य ट्री को पूर्ण द्विआधारी ट्री में एम्बेड कर सकते हैं और S2S की निर्णायकता का उपयोग कर सकते हैं। उदाहरण के लिए, एक नोड s के लिए, हम इसके बच्चों को s1, s01, s001, आदि द्वारा दर्शा सकते हैं। अनगिनत पेड़ों के लिए, हम शेलाह-स्टप प्रमेय (नीचे) का उपयोग कर सकते हैं। हम कार्डिनलिटी ω1 वाले सेट फर्स्ट ऑर्डर ऑब्जेक्ट्स के लिए एक विधेय भी जोड़ सकते हैं, और कार्डिनलिटी ω2 के लिए विधेय, और अनंत नियमित कार्डिनल्स के लिए भी। बंधे हुए पेड़ की चौड़ाई के ग्राफ की व्याख्या पेड़ों का उपयोग करके की जा सकती है, और किनारों पर भविष्यवाणी के बिना यह बंधे हुए गुट की चौड़ाई के ग्राफ पर भी लागू होता है। एस2एस को अन्य निर्णायक सिद्धांतों के साथ जोड़ना मोनडिक सिद्धांतों का वृक्ष विस्तारः शेलाह-स्टप प्रमेय के अनुसार, यदि एक मोनडिक संबंधपरक मॉडल एम निर्णायक है, तो इसका वृक्ष समकक्ष भी ऐसा ही है। उदाहरण के लिए, (औपचारिकरण का मॉडुलो विकल्प) S2S, {0,1} का वृक्ष समकक्ष है। वृक्ष समकक्ष में, प्रथम क्रम की वस्तुएं विस्तार द्वारा क्रमबद्ध M के तत्वों के परिमित अनुक्रम हैं, और एक M-संबंध Pi को Pi '(vd1,., vdk) ′Pi (d1,., dk) के साथ Pi' गलत अन्यथा (dj ωM, और v M के तत्वों का एक (संभवतः खाली) अनुक्रम है। प्रमाण एस2एस निर्णायकता प्रमाण के समान है। प्रत्येक चरण में, एक (गैर-निर्धारक) स्वचालित को इनपुट के रूप में एम वस्तुओं (संभवतः दूसरे क्रम) का एक टुपल मिलता है, और एक एम सूत्र निर्धारित करता है कि किस अवस्था संक्रमण की अनुमति है। खिलाड़ी 1 (जैसा कि ऊपर बताया गया है) एक मानचित्रण चाइल्ड स्टेट को चुनता है जो सूत्र द्वारा अनुमत है (वर्तमान स्थिति को देखते हुए), और खिलाड़ी 2 जारी रखने के लिए चाइल्ड (नोड के) को चुनता है। एक गैर-निर्धारक स्वचालित द्वारा अस्वीकृति को देखने के लिए, प्रत्येक (नोड, राज्य) के लिए (चाइल्ड, स्टेट) जोड़े का एक सेट चुनें जैसे कि प्रत्येक विकल्प के लिए, जोड़े में से कम से कम एक को मारा जाए, और इस तरह कि सभी परिणामी मार्ग अस्वीकृति की ओर ले जाएं। प्रथम क्रम सिद्धांत के साथ एक मठवासी सिद्धांत का संयोजनः फेफरमैन-वॉट प्रमेय निम्नानुसार विस्तारित/लागू होता है। यदि एम एक एमएसओ मॉडल है और एन एक प्रथम क्रम मॉडल है, तो एम एक (सिद्धांत (एम), सिद्धांत (एन)) दैवज्ञ के सापेक्ष निर्णायक बना रहता है, भले ही एम को सभी कार्यों एम → एन के साथ संवर्धित किया गया हो, जहां एम को इसकी पहली वस्तुओं के साथ पहचाना जाता है, और प्रत्येक एस के लिए एम हम एन की एक अलग प्रति का उपयोग करते हैं, जिसके अनुसार भाषा को संशोधित किया जाता है। उदाहरण के लिए, यदि N (, 0, +, ⋅) है, तो हम बता सकते हैं कि (फलन f) βs βr βr βr βr βr = 0Ns। यदि M S2S है (या अधिक सामान्य रूप से, कुछ मोनडिक मॉडल का ट्री समकक्ष), तो ऑटोमेटा अब N-सूत्रों का उपयोग कर सकता है, और इस तरह f: M → Nk को M सेटों के टुपल में परिवर्तित कर सकता है। असहमति आवश्यक है क्योंकि अन्यथा समानता के साथ प्रत्येक अनंत N के लिए, विस्तारित S2S या सिर्फ WS1S अनिश्चित है। इसके अलावा, एक (संभवतः अपूर्ण) सिद्धांत टी के लिए, टी के एम-उत्पादों का सिद्धांत टी. एम. एक (सिद्धांत (एम), टी) दैवज्ञ के सापेक्ष निर्णायक है, जहां टी. एम. का एक मॉडल प्रत्येक एस. के लिए टी के एक मनमाने ढंग से असंबद्ध मॉडल एन. एस. का उपयोग करता है। प्रमाण सूत्र जटिलता पर प्रेरण द्वारा है। मान लीजिए कि यह मुक्त एनएस चर की सूची है, जिसमें f (s) भी शामिल है यदि फलन f मुक्त है। प्रेरण द्वारा, एक यह दर्शाता है कि बनाम का उपयोग केवल |vs। मुक्त चर के साथ एन-सूत्रों के एक सीमित सेट के माध्यम से किया जाता है। इस प्रकार, हम क्या संभव है इसका उत्तर देने के लिए एन (या टी) का उपयोग करके सभी संभावित परिणामों की मात्रा निर्धारित कर सकते हैं, और एक सूची संभावनाओं (या बाधाओं) को देखते हुए, एम में एक संबंधित वाक्य तैयार कर सकते हैं। प्रमाणः एक गैर-निर्धारक अनंत वृक्ष स्वचालित को देखते हुए, हम परिमित द्विआधारी लेबल वाले पेड़ों के समूह (जिन पर लेबल होते हैं जिन पर स्वचालित काम कर सकते हैं) को सीमित रूप से कई वर्गों में विभाजित कर सकते हैं जैसे कि यदि एक पूर्ण अनंत द्विआधारी पेड़ समान श्रेणी के पेड़ों से बना हो सकता है, तो स्वीकृति केवल वर्ग और प्रारंभिक स्थिति (यानी। बता दें कि ऑटोमेटन पेड़ में प्रवेश करता है)। (पंपिंग लेम्मा के साथ एक मोटे तौर पर समानता पर ध्यान दें।) उदाहरण के लिए (एक पैरिटी ऑटोमेटन के लिए), एक ही वर्ग को वृक्ष निर्धारित करें यदि उनके पास एक ही विधेय है जो दिए गए प्रारंभिक _ अवस्था और सेट क्यू (राज्य, उच्चतम _ प्राथमिकता _ पहुँचा) जोड़े लौटाते हैं कि क्या खिलाड़ी 1 (यानी। गैर-निर्धारणवाद) एक साथ सभी शाखाओं को क्यू के तत्वों के अनुरूप होने के लिए मजबूर कर सकता है। अब, प्रत्येक k के लिए, पेड़ों का एक सीमित समूह (कोडिंग के लिए उपयुक्त) चुनें जो ऑटोमेटा 1-k के लिए एक ही वर्ग से संबंधित हो, जिसमें k के पार सुसंगत वर्ग का विकल्प हो। एक विधेय को कूटबद्ध करने के लिए, k = 1 का उपयोग करके कुछ बिट्स को कूटबद्ध करें, फिर k = 2 का उपयोग करके अधिक बिट्स, और इसी तरह। संदर्भ अतिरिक्त संदर्भः गणितीय तर्क संगणनीयता सिद्धांत प्रमाण वाले लेख