वास्तविक संख्याओं के प्रथम-क्रम सिद्धांतों की निर्णायकता
गणितीय तर्क में, वास्तविक संख्याओं की प्रथम-क्रम वाली भाषा प्रथम-क्रम तर्क के सुव्यवस्थित वाक्यों का समुच्चय है, जिसमें सार्वभौमिक और अस्तित्वगत परिमाणक और वास्तविक चरों पर अभिव्यक्तियों की समानता और असमानताओं के तार्किक संयोजन सम्मिलित होते हैं। तदनुरूपी प्रथम-क्रम सिद्धांत वाक्यों का वह समूह है जो वास्तव में वास्तविक संख्याओं के लिए सत्य है। ऐसे कई अलग-अलग सिद्धांत हैं, जिनमें अलग-अलग अभिव्यंजक शक्ति होती है, जो व्यंजक में उपयोग करने की अनुमति वाले अभाज्य संचालन पर निर्भर करता है। इन सिद्धांतों के अध्ययन में एक बुनियादी सवाल यह है कि क्या वे निर्णय लेने योग्य हैं: यानी, क्या कोई एल्गोरिदम है जो एक वाक्य को इनपुट के रूप में ले सकता है और आउटपुट के रूप में इस सवाल का उत्तर "हां" या "नहीं" दे सकता है कि वाक्य सिद्धांत में सत्य है या नहीं है।
वास्तविक बंद क्षेत्रों का सिद्धांत वह सिद्धांत है जिसमें अभाज्य संक्रियाएँ गुणन और जोड़ हैं; इसका तात्पर्य यह है कि, इस सिद्धांत में, केवल वही संख्याएँ परिभाषित की जा सकती हैं जो वास्तविक बीजगणितीय संख्याएँ हैं। जैसा कि टार्स्की ने सिद्ध किया है, यह सिद्धांत निर्णायक है; टार्स्की-सीडेनबर्ग प्रमेय और क्वांटिफ़ायर उन्मूलन देखें। वास्तविक बंद क्षेत्रों के सिद्धांत के लिए निर्णय प्रक्रियाओं का वर्तमान कार्यान्वयन प्रायः बेलनाकार बीजगणितीय अपघटन द्वारा क्वांटिफायर उन्मूलन पर आधारित होता है।
टार्स्की की घातीय फ़ंक्शन समस्या इस सिद्धांत के एक अन्य अभाज्य संक्रिया, घातीय फ़ंक्शन के विस्तार से संबंधित है। यह एक खुली समस्या है कि क्या यह सिद्धांत निर्णायक है, लेकिन यदि शैनुएल का अनुमान सही बैठता है तो इस सिद्धांत की निर्णायकता का पालन होगा।[1][2] इसके विपरीत, साइन फ़ंक्शन के साथ वास्तविक बंद फ़ील्ड के सिद्धांत का विस्तार अनिर्णीत है क्योंकि यह पूर्णांकों के अनिर्णीत सिद्धांत के एन्कोडिंग की अनुमति देता है (रिचर्डसन का प्रमेय देखें)।
फिर भी, कोई भी एल्गोरिदम का उपयोग करके साइन जैसे फंक्शन्स के साथ अनिर्णीत स्थिति को संभाल सकता है जो जरूरी नहीं कि हमेशा समाप्त हो। विशेष रूप से, कोई ऐसे एल्गोरिदम डिज़ाइन कर सकता है जिन्हें केवल उन इनपुट फ़ार्मुलों के लिए समाप्त करने की आवश्यकता होती है जो रोबस्ट हैं, अर्थात, ऐसे सूत्र जिनकी संतोषणीयता सूत्र में थोड़ी गड़बड़ी होने पर नहीं बदलती।[3] वैकल्पिक रूप से, विशुद्ध रूप से अनुमानी दृष्टिकोण का उपयोग करना भी संभव है।[4]
यह भी देखें
- वास्तविक संख्याओं का निर्माण - वास्तविक संख्याओं की स्वयंसिद्ध परिभाषाएँ
- टार्स्की का वास्तविक संख्याओं का स्वयंसिद्धीकरण
संदर्भ
- ↑ Macintyre, A.J.; Wilkie, A.J. (1995), "On the decidability of the real exponential field", in Odifreddi, P.G. (ed.), Kreisel 70th Birthday Volume, CLSI
- ↑ Kuhlmann, S. (2001) [1994], "Model theory of the real exponential function", Encyclopedia of Mathematics, EMS Press
- ↑ Ratschan, Stefan (2006). "वास्तविक संख्याओं पर परिमाणित असमानता बाधाओं का कुशल समाधान". ACM Transactions on Computational Logic. 7 (4).
- ↑ Akbarpour, Behzad; Paulson, Lawrence Charles (2010). "MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions". Journal of Automated Reasoning. 44.