S2S (गणित): Difference between revisions

'''गणित''' में, '''S2S''' दो उत्तराधिकारियों वाला मोनैडिक द्वितीय क्रम सिद्धांत होता है। यह ज्ञात सबसे अभिव्यंजक प्राकृतिक निर्णायक सिद्धांतों में से एक होता है, जिसमें S2S में कई निर्णायक सिद्धांतों की व्याख्या की जा सकती है। इसकी निर्णायकता 1969 में माइकल ओ. राबिन द्वारा सिद्ध की गई थी।<ref>{{Cite journal |title=अनंत पेड़ों पर दूसरे क्रम के सिद्धांतों और ऑटोमेटा की निर्णायकता|last=Rabin |first=Michael |journal=Transactions of the American Mathematical Society |volume=141 |date=1969 |url=https://www.ams.org/journals/tran/1969-141-00/S0002-9947-1969-0246760-1/S0002-9947-1969-0246760-1.pdf}}</ref>

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

* [[क्लेन स्टार]] का उपयोग करते हुए, सभी बाइनरी स्ट्रिंग्स के समुच्चय को {0,1} द्वारा प्रदर्शित किया जाता है।

* {0,1} का अनैतिक उपसमुच्चय^* को कभी-कभी ट्री से पहचाना जाता है, विशेष रूप से {0,1}-लेबल वाले ट्री {0,1} के रूप में^*; {0,1} एक पूर्ण अनंत बाइनरी ट्री बनाता है।

* सूत्र जटिलता के लिए, स्ट्रिंग्स पर उपसर्ग संबंध को सामान्यतः पहले क्रम के रूप में माना जाता है। इसकेअतिरिक्त, सभी सूत्र Δ¹₂ के समतुल्य नहीं होंगे।<ref>{{Cite conference |title=बाइनरी ट्री के मोनैडिक लॉजिक की संरचना पर|last1=Janin |first1=David |last2=Lenzi |first2=Giacomo |url=https://hal.archives-ouvertes.fr/hal-00676277 |conference=MFCS 1999 |doi=10.1007/3-540-48340-3_28}}</ref>

* S2S में अभिव्यक्त गुणों के लिए (सभी बाइनरी स्ट्रिंग्स के समुच्चय को एक ट्री के रूप में देखते हुए), प्रत्येक नोड के लिए, मात्र O(1) बिट्स को बाएं सबट्री और दाएं सबट्री और बाकी के मध्य संचारित किया जा सकता है ([[संचार जटिलता]] देखें)।

* एक निश्चित k के लिए, स्ट्रिंग से k तक एक फलन (अर्थात् k के नीचे की प्राकृतिक संख्या) को एक समुच्चय द्वारा एनकोड किया जा सकता है। इसके अतिरिक्त, s,t ⇒ s01t{{prime}} जहां T{{prime}} t के प्रत्येक वर्ण को दोगुना कर देता है, और s ⇒ {s01t{{prime}}: t∈{0,1}^*} S2S निश्चित होता है। इसके विपरीत, संचार जटिलता युक्ति के अनुसार, S1S (नीचे) में समुच्चय की एक जोड़ी को एक समुच्चय द्वारा एनकोड करने योग्य नहीं होता है।

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

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

S2S को आंशिक रूप से स्वयंसिद्ध किया जा सकता है:<br />(1) ∃!s ∀t ( t0≠s ∧ t1≠s) (रिक्त स्ट्रिंग, जिसे ε द्वारा दर्शाया गया है; ∃!s का अर्थ है कि "अद्वितीय s" होता है)<br />(2) ∀s,t ∀i∈{0,1} ∀j∈{0,1} (si=tj ⇒ s=t ∧ i=j) (i और j का उपयोग एक संक्षिप्त रूप होता है; i= j के लिए, 0, 1 के बराबर नहीं होता है)<br />(3) ∀S (S(ε) ∧ ∀s (S(s) ⇒ S(s0) ∧ S(s1))⇒ ∀s S(s)) ([[गणितीय प्रेरण]])<br />(4) ∃S ∀s (S(s) ⇔ φ(s)) (S φ में मुक्त नहीं होता है)

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

S1S का अनुरूप स्वयंसिद्धीकरण पूरा हो जाता है।<ref>{{Cite conference |url=https://link.springer.com/content/pdf/10.1007%2F978-3-642-33475-7_22.pdf |last=Riba |first=Colin |title=अनंत शब्दों पर राक्षसी दूसरे क्रम के तर्क के स्वयंसिद्धीकरण की पूर्णता का एक मॉडल सैद्धांतिक प्रमाण|conference=TCS 2012 |date=2012 |doi=10.1007/978-3-642-33475-7_22}}</ref> यघपि, S2S के लिए, पूर्णता खुली रहती है (2021 तक)। जबकि S1S में एकरूपता होती है, कोई S2S परिभाषित (यहां तक ​​कि पैरामीटर की अनुमति देने वाला) विकल्प फलन नहीं होता है जो एक गैर-रिक्त समुच्चय दिखाता है, S, S का एक तत्व लौटाता है,<ref>{{Citation |chapter-url=https://hal-upec-upem.archives-ouvertes.fr/hal-00620169/file/csl07.pdf |chapter=MSO on the Infinite Binary Tree: Choice and Order |last1=Carayol |first1=Arnaud |last2= Löding|first2=Christof |title=Computer Science Logic |series=Lecture Notes in Computer Science |date=2007 |volume=4646 |pages=161–176 |doi=10.1007/978-3-540-74915-8_15|isbn=978-3-540-74914-1 |s2cid=14580598 }}</ref> और समझ स्कीमों को सामान्यतः विकल्प के सिद्धांत के विभिन्न रूपों के साथ संवर्धित किया जाता है। यघपि, (1)-(4) कुछ [[समता खेल|समानता का खेलों]] के लिए निर्धारण स्कीमा के साथ विस्तारित होने पर पूर्ण हो जाता है।<ref>{{Cite journal |title=अनंत पेड़ों का एक कार्यात्मक (मोनैडिक) दूसरे क्रम का सिद्धांत|last1=Das |first=Anupam |last2=Riba |first2=Colin |journal=Logical Methods in Computer Science |volume=16|issue=4 |date=2020 |doi=10.23638/LMCS-16(4:6)2020 |arxiv=1903.05878}} (A preliminary 2015 version erroneously claimed proof of completeness without the determinacy schema.)</ref>

S2S को Π¹₃ सूत्रों द्वारा भी स्वयंसिद्ध किया जा सकता है (स्ट्रिंग्स पर उपसर्ग संबंध को प्राथमिक के रूप में उपयोग करके)। यघपि, यह अंतिम रूप से स्वयंसिद्ध नहीं होता है, न ही इसे Σ¹₃ सूत्रों द्वारा स्वयंसिद्ध किया जा सकता है, तथापि हम प्रेरण स्कीमा और अन्य सूत्रों का एक सीमित समुच्चय जोड़ दें (यह Π¹₂-CA₀ से सम्बन्धित होता है)।

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

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

S2S में कमी करके, गणनीय आदेशों का MSO सिद्धांत निर्णायक होता है, जैसा कि उनके क्लेन-ब्रौवर आदेशों के साथ गणनीय ट्री का MSO सिद्धांत होता है। यघपि, MSO सिद्धांत (<math>\mathbb{R}</math>, <) अनिर्णीत होता है।<ref>{{Cite journal |first1=Yuri |last1=Gurevich |first2=Saharon |last2=Shelah | authorlink2=Saharon Shelah |title=अद्वैतवादी सिद्धांत और "अगली दुनिया"|journal=[[Israel Journal of Mathematics]] |date=1984 |volume=49 |issue=1–3 |pages=55–68 |doi=10.1007/BF02760646 | doi-access=free |s2cid=15807840 }}</ref><ref>{{Cite web |url=https://mathoverflow.net/questions/385530/what-is-the-turing-degree-of-the-monadic-theory-of-the-real-line |title=What is the Turing degree of the monadic theory of the real line? |publisher=MathOverflow |access-date=November 14, 2022}}</ref> इस प्रकार क्रमवाचक संख्या का MSO सिद्धांत <ω₂ निर्णय योग्य होता है; इस प्रकार ω₂ के लिए निर्णायकता ZFC से स्वतंत्र होता है (Con(ZFC + [[कमजोर रूप से कॉम्पैक्ट कार्डिनल]] मानते हुए)) ।<ref>{{Cite journal |first1=Yuri |last1=Gurevich |first2=Menachem |last2=Magidor |first3=Saharon |last3=Shelah |date=1993 |title=The monadic theory of ω₂ |journal=The Journal of Symbolic Logic |volume=48 |issue=2 |pages=387–398 |doi=10.2307/2273556 |jstor=2273556 |s2cid=120260712 |url=https://shelah.logic.at/files/95215/141.pdf }}</ref> इसके अतिरिक्त, एक क्रमवाचक संख्या को क्रमवाचक संख्या पर मोनैडिक सेकेंड क्रम युक्ति का उपयोग करके परिभाषित किया जा सकता है यदि इसे क्रमवाचक संख्या जोड़ और गुणा द्वारा निश्चित नियमित क्रमवाचक संख्या से प्राप्त किया जा सकता है।<ref>{{Citation |chapter=Monadic definability of ordinals |first=Itay |last=Neeman|title=Computational Prospects of Infinity |series=Lecture Notes Series, Institute for Mathematical Sciences, National University of Singapore |chapter-url=https://www.math.ucla.edu/~ineeman/monadic-def.pdf |date=2008 |volume=15 |pages=193–205 |doi=10.1142/9789812796554_0010|isbn=978-981-279-654-7 }}</ref>

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

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

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

यघपि , मुक्त दूसरे क्रम के चर के साथ, प्रत्येक S2S सूत्र को मात्र Π¹₁ के माध्यम से दूसरे क्रम के अंकगणित में व्यक्त नहीं किया जा सकता है (रिवर्स गणित देखें)। RCA₀ + (स्कीमा) {τ: τ एक सत्य S2S सूत्र } (स्कीमा) के बराबर होता है {τ: τ एक Π¹₃ सूत्र है जिसे Π¹₂-CA₀ } में सिद्ध किया जा सकता है।<ref name="S2S--Pi-1-2-CA_0">{{Cite conference |conference=LICS '16: 31st Annual ACM/IEEE Symposium on Logic in Computer Science |date=2016  |title=राबिन की निर्णायकता प्रमेय कितनी अप्रमाणित है?|first1=Leszek |last1=Kołodziejczyk |first2=Henryk |last2=Michalewski |arxiv=1508.06780 }}</ref><ref>{{Cite web |last=Kołodziejczyk |first=Leszek |url = https://cs.nyu.edu/pipermail/fom/2015-October/019257.html |title=Question on Decidability of S2S |publisher=FOM |date=October 19, 2015}}</ref> आधार सिद्धांत पर, स्कीमा (k पर स्कीमा) ∀S⊆ω ∃α₁<....<α_''k'' ''L''_α1(''S'') ≺_Σ1 ... ≺_Σ1 ''L''_α''k''(S) के समतुल्य होती है। जहां L रचनात्मक ब्रह्मांड होता है ([[बड़े गणनीय क्रमसूचक]] भी देखें)। सीमित प्रेरण के कारण, Π¹₂-CA₀ यह सिद्ध नहीं करता कि सब सत्य है (मानक निर्णय प्रक्रिया के अंतर्गत) Π¹₃ S2S कथन वास्तव में सत्य होते हैं, तथापि ऐसा प्रत्येक सूत्र Π¹₂-CA₀ सिद्ध करने योग्य होता है।

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

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

प्रत्येक S⊆ω के लिए, S में पुनरावर्ती समुच्चय मानक S1S प्रतिरूप का एक प्राथमिक उपप्रतिरूप बनाते हैं, और ट्यूरिंग जॉइन और ट्यूरिंग रिड्यूसिबिलिटी के अनुसार बंद किए गए ω के प्रत्येक गैर-रिक्त संग्रह के लिए समान होते हैं।<ref>{{Cite journal |last1=Kołodziejczyk |first1=Leszek |last2=Michalewski |first2=Henryk |last3=Pradic |first3=Pierre |last4=Skrzypczak |first4=Michał |title=The logical strength of Büchi's decidability theorem |journal=Logical Methods in Computer Science |volume=15 |issue=2 |date=2019 |pages=16:1–16:31 |url=https://lmcs.episciences.org/5503/}}</ref>

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

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

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