क्वांटिफायर उन्मूलन

क्वांटिफायर उन्मूलन गणितीय तर्क, मॉडल सिद्धांत और सैद्धांतिक कंप्यूटर विज्ञान में प्रयुक्त सरलीकरण की एक अवधारणा है। अनौपचारिक रूप से, एक मात्रात्मक कथन "$\exists x$ ऐसा है कि …" को एक प्रश्न के रूप में देखा जा सकता है "कब कोई $x$ ऐसा है कि $\ldots$?", और क्वांटिफायर के बिना कथन को उस प्रश्न के उत्तर के रूप में देखा जा सकता है।

फ़ार्मुलों को वर्गीकृत करने का एक तरीका परिमाणीकरण की मात्रा है। क्वांटिफायर प्रत्यावर्तन की कम गहराई वाले फ़ार्मुलों को सरल माना जाता है, क्वांटिफ़ायर-मुक्त फ़ार्मुलों को सबसे सरल माना जाता है। एक सिद्धांत में क्वांटिफायर उन्मूलन होता है यदि प्रत्येक सूत्र $\alpha$ के लिए क्वांटिफायर के बिना एक और सूत्र $\alpha _{QF}$ मौजूद होता है जो इसके बराबर होता है (मॉड्यूलो यह सिद्धांत)।

उदाहरण

हाई स्कूल गणित से एक उदाहरण कहता है कि एक एकल-चर द्विघात बहुपद का एक वास्तविक मूल होता है यदि और केवल यदि इसका विभेदक गैर-ऋणात्मक है:

$\exists x\in \mathbb {R} .(a\neq 0\wedge ax^{2}+bx+c=0)\ \ \Longleftrightarrow \ \ a\neq 0\wedge b^{2}-4ac\geq 0$

यहाँ बाईं ओर के वाक्य में क्वांटिफायर $\exists x\in \mathbb {R}$ सम्मिलित है, जबकि दाईं ओर के समकक्ष वाक्य में नहीं है।

प्रमात्रक विलोपन का उपयोग करके निर्णायक साबित होने वाले सिद्धांतों के उदाहरण प्रेस्बर्गर अंकगणित हैं, बीजगणितीय रूप से बंद क्षेत्र, वास्तविक बंद क्षेत्र, परमाणु (आदेश सिद्धांत) बूलियन बीजगणित, शब्द बीजगणित , घने रेखीय क्रम, एबेलियन समूह, यादृच्छिक रेखांकन, साथ ही साथ उनके कई संयोजन जैसे प्रेस्बर्गर अंकगणित के साथ बूलियन बीजगणित, और क्यू (गणित) के साथ शब्द बीजगणित।

एक आदेशित योगात्मक समूह के रूप में वास्तविक संख्या के सिद्धांत के लिए क्वांटिफायर एलिमिनेटर फूरियर-मोट्ज़किन उन्मूलन है; वास्तविक संख्या के क्षेत्र के सिद्धांत के लिए यह टार्स्की-सीडेनबर्ग प्रमेय है।

क्वांटिफायर एलिमिनेशन का उपयोग यह दिखाने के लिए भी किया जा सकता है कि निर्णायक सिद्धांतों का "संयोजन" नए निर्णायक सिद्धांतों की ओर जाता है (देखें फेफरमैन-वॉट प्रमेय)।

एल्गोरिदम और निर्णायकता

यदि किसी सिद्धांत में क्वांटिफायर एलिमिनेशन है, तो एक विशिष्ट प्रश्न को संबोधित किया जा सकता है: क्या निर्धारण की कोई विधि है $\alpha _{QF}$ प्रत्येक के लिए $\alpha$? अगर ऐसी कोई विधि है तो हम इसे क्वांटिफायर एलिमिनेशन कलन विधि कहते हैं। यदि ऐसा कोई एल्गोरिथम है, तो डिसिडेबिलिटी (तर्क) # थ्योरी के लिए एक थ्योरी की डेसिडेबिलिटी क्वांटिफायर-फ्री सेंटेंस (गणितीय तर्क) की सच्चाई तय करने के लिए कम हो जाती है। क्वांटिफायर-मुक्त वाक्यों में कोई चर नहीं है, इसलिए किसी दिए गए सिद्धांत में उनकी वैधता की गणना अक्सर की जा सकती है, जो वाक्यों की वैधता तय करने के लिए क्वांटिफायर एलिमिनेशन एल्गोरिदम के उपयोग को सक्षम बनाता है।

संबंधित अवधारणाएँ

विभिन्न मॉडल-सैद्धांतिक विचार क्वांटिफायर उन्मूलन से संबंधित हैं, और विभिन्न समतुल्य स्थितियां हैं।

प्रमात्रक विलोपन के साथ प्रत्येक प्रथम-क्रम सिद्धांत मॉडल पूर्ण है। इसके विपरीत, एक मॉडल-पूर्ण सिद्धांत, जिसके सार्वभौमिक परिणामों के सिद्धांत में समामेलन संपत्ति है, में क्वांटिफायर उन्मूलन है।

एक सिद्धांत के सार्वभौमिक परिणामों के सिद्धांत के मॉडल $T$ के मॉडल के ठीक उपसंरचना (गणित) हैं $T$. रेखीय क्रम के सिद्धांत में परिमाणक विलोपन नहीं है। हालाँकि इसके सार्वभौमिक परिणामों के सिद्धांत में समामेलन गुण है।

मूल विचार

रचनात्मक रूप से यह दिखाने के लिए कि एक सिद्धांत में क्वांटिफायर एलिमिनेशन है, यह दिखाने के लिए पर्याप्त है कि हम शाब्दिक (गणितीय तर्क) के संयोजन के लिए लागू एक अस्तित्वगत क्वांटिफायर को समाप्त कर सकते हैं, जो कि फॉर्म के प्रत्येक सूत्र को दर्शाता है:

$\exists x.\bigwedge _{i=1}^{n}L_{i}$

जहां प्रत्येक $L_{i}$ एक शाब्दिक है, एक परिमाणक मुक्त सूत्र के बराबर है। दरअसल, मान लीजिए कि हम जानते हैं कि क्वांटिफायर को शाब्दिक संयोजन से कैसे खत्म किया जाए, तो यदि $F$ क्वांटिफायर-फ्री फॉर्मूला है, हम इसे असंबद्ध सामान्य रूप में लिख सकते हैं

$\bigvee _{j=1}^{m}\bigwedge _{i=1}^{n}L_{ij},$

और इस तथ्य का उपयोग करें कि

$\exists x.\bigvee _{j=1}^{m}\bigwedge _{i=1}^{n}L_{ij}$

के बराबर है

$\bigvee _{j=1}^{m}\exists x.\bigwedge _{i=1}^{n}L_{ij}.$

अंत में, एक सार्वभौमिक क्वांटिफायर को खत्म करने के लिए

$\forall x.F$

कहाँ $F$ क्वांटिफायर-फ्री है, हम ट्रांसफॉर्म करते हैं

$\lnot F$ वियोगात्मक सामान्य रूप में, और इस तथ्य का उपयोग करें कि $\forall x.F$

के बराबर है $\lnot \exists x.\lnot F.$

निर्णायकता के साथ संबंध

प्रारंभिक मॉडल सिद्धांत में, क्वांटिफायर एलिमिनेशन का उपयोग यह प्रदर्शित करने के लिए किया गया था कि विभिन्न सिद्धांतों में निर्णायकता (तर्क) और पूर्ण सिद्धांत जैसे गुण होते हैं। एक सामान्य तकनीक पहले यह दिखाना था कि एक सिद्धांत क्वांटिफायर के उन्मूलन को स्वीकार करता है और उसके बाद केवल क्वांटिफायर मुक्त सूत्रों पर विचार करके निर्णायकता या पूर्णता साबित करता है। इस तकनीक का उपयोग यह दिखाने के लिए किया जा सकता है कि प्रेस्बर्गर अंकगणित निर्णायक है।

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

उदाहरण: Nullstellensatz बीजगणितीय रूप से बंद क्षेत्रों के लिए और भिन्न रूप से बंद क्षेत्रों के लिए।

यह भी देखें

• बेलनाकार बीजगणितीय अपघटन
• उन्मूलन सिद्धांत
• संधि विलोपन

संदर्भ

• Brown, Christopher W. (July 31, 2002). "What is Quantifier Elimination". Retrieved Aug 30, 2018.

• Enderton, Herbert (2001). A mathematical introduction to logic (2nd ed.). Boston, MA: Academic Press. ISBN 978-0-12-238452-3.

• Fried, Michael D.; Jarden, Moshe (2008). Field arithmetic. Ergebnisse der Mathematik und ihrer Grenzgebiete. 3. Folge. Vol. 11 (3rd revised ed.). Springer-Verlag. ISBN 978-3-540-77269-9. Zbl 1145.12001.

• Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid; Maarten, Marx; Spencer, Joel; Vardi, Moshe Y.; Venema, Yde; Weinstein, Scott (2007). Finite model theory and its applications. Texts in Theoretical Computer Science. An EATCS Series. Berlin: Springer-Verlag. ISBN 978-3-540-00428-8. Zbl 1133.03001.

• Hodges, Wilfrid (1993). Model Theory. Encyclopedia of Mathematics and its Applications. Vol. 42. Cambridge University Press. doi:10.1017/CBO9780511551574. ISBN 9780521304429.

• Kuncak, Viktor; Rinard, Martin (2003). "Structural Subtyping of Non-Recursive Types is Decidable" (PDF). 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings. doi:10.1109/LICS.2003.1210049. ISBN 0-7695-1884-2.

• Monk, J. Donald Monk (2012). Mathematical Logic (Graduate Texts in Mathematics (37)) (Softcover reprint of the original 1st ed. 1976 ed.). Springer. ISBN 9781468494549.

• Nipkow, T (2010). "Linear Quantifier Elimination" (PDF). Journal of Automated Reasoning. 45 (2): 189–212. doi:10.1007/s10817-010-9183-0. S2CID 14279141. Retrieved 2022-11-12.

• Presburger, Mojżesz (1929). "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt". Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, Warszawa: 92–101., see Stansifer (1984) for an English translation

• Szmielew, Wanda (1955). "Elementary properties of Abelian groups". Fundamenta Mathematicae. 41 (2): 203–271. doi:10.4064/fm-41-2-203-271. MR 0072131.

• Jeannerod, Nicolas; Treinen, Ralf. Deciding the First-Order Theory of an Algebra of Feature Trees with Updates. International Joint Conference on Automated Reasoning (IJCAR). doi:10.1007/978-3-319-94205-6_29.

• Sturm, Thomas (2017). "A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications". Mathematics in Computer Science. 11: 483–502. doi:10.1007/s11786-017-0319-z.