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>

== मूल गुण ==

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

* डिफ़ॉल्ट रूप से, लोअरकेस अक्षर पहले क्रम की वस्तुओं को संदर्भित करते हैं, और अपरकेस दूसरे क्रम की वस्तुओं को संदर्भित करते हैं।

* स्ट्रिंग्स 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}^* एक पूर्ण अनंत बाइनरी ट्री बनाता है।

* सूत्र जटिलता के लिए, स्ट्रिंग्स पर उपसर्ग संबंध को आम तौर पर पहले क्रम के रूप में माना जाता है। इसके बिना, सभी सूत्र Δ के समतुल्य नहीं होंगे¹₂ सूत्र.<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>

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

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

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

S2S में कमी करके, गणनीय आदेशों का 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> ऑर्डिनल्स का एमएसओ सिद्धांत <ω₂ निर्णययोग्य है; ω के लिए निर्णायकता₂ 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+U (या सिर्फ S1S+U) अनिर्णीत है यदि U अनबाउंडिंग क्वांटिफायर है - UX Φ(X) यदि Φ(X) कुछ मनमाने ढंग से बड़े परिमित X के लिए है।<ref>{{Citation |title=The MSO+U theory of (N, &lt;) is undecidable |first1=Mikołaj |last1=Bojańczyk |first2=Paweł |last2=Parys |first3=Szymon |last3=Toruńczyk |arxiv=1502.04578 |date=2015}}</ref> हालाँकि, WS2S+U, अनंत पथों पर परिमाणीकरण के साथ भी, निर्णय लेने योग्य है, यहां तक ​​कि S2S उपसूत्रों के साथ भी, जिनमें U शामिल नहीं है।<ref>{{Citation |title=Weak MSO+U with path quantifiers over infinite trees |first1=Mikołaj |last1=Bojańczyk |arxiv=1404.7278 |date=2014}}</ref>

== सूत्र जटिलता ==

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

हालाँकि, मुक्त दूसरे क्रम के चर के साथ, प्रत्येक S2S सूत्र को केवल Π के माध्यम से दूसरे क्रम के अंकगणित में व्यक्त नहीं किया जा सकता है¹₁ ट्रांसफ़िनिट रिकर्सन (रिवर्स गणित देखें)। आरसीए₀ + (स्कीमा) {τ: τ एक सच्चा S2S वाक्य है} (स्कीमा) के बराबर है {τ: τ एक Π है¹₃ Π में सिद्ध वाक्य¹₂-वह₀ }.<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_{α₁</उप>(एस) ≺_Σ₁... ≺ उप>एस₁</उप>एल उप>ए_''k''}(एस) जहां एल रचनात्मक ब्रह्मांड है ([[बड़े गणनीय क्रमसूचक]] भी देखें)। सीमित प्रेरण के कारण, Π¹₂-वह₀ यह सिद्ध नहीं करता कि सब सत्य है (मानक निर्णय प्रक्रिया के अंतर्गत) Π¹₃ S2S कथन वास्तव में सत्य हैं, भले ही ऐसा प्रत्येक वाक्य सिद्ध करने योग्य हो¹₂-वह₀.

(3) टी को अंकगणित μ-कैलकुलस में एस से परिभाषित किया जा सकता है (अंकगणित सूत्र + निश्चित-बिंदु तर्क | कम से कम निश्चित-बिंदु तर्क)<br />

== S1S और S2S के मॉडल ==

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

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

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

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