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

क्वांटिफायर एलिमिनेशन गणितीय तर्क, मॉडल सिद्धांत और सैद्धांतिक कंप्यूटर विज्ञान में प्रयुक्त सरलीकरण की एक अवधारणा है। अनौपचारिक रूप से, एक मात्रात्मक कथन "$\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$ के लिए $\alpha _{QF}$ निर्धारित करने का कोई तरीका है? यदि ऐसी कोई विधि है, तो हम इसे क्वांटिफायर एलिमिनेशन कलन विधि कहते हैं। यदि ऐसा कोई एल्गोरिदम है, तो सिद्धांत के लिए निर्णायकता क्वांटिफायर-मुक्त वाक्यों की सच्चाई तय करने के लिए कम हो जाती है। क्वांटिफायर-मुक्त वाक्यों में कोई चर नहीं है, इसलिए किसी दिए गए सिद्धांत में उनकी वैधता की गणना अक्सर की जा सकती है, जो वाक्यों की वैधता तय करने के लिए क्वांटिफायर एलिमिनेशन एल्गोरिदम के उपयोग को सक्षम बनाता है।

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

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

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

एक सिद्धांत $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.