वास्तविक संख्याओं के प्रथम-क्रम सिद्धांतों की निर्णायकता
This article needs additional citations for verification. (September 2014) (Learn how and when to remove this template message) |
गणितीय तर्क में, वास्तविक संख्याओं की प्रथम-क्रम वाली भाषा सभी सुगठित फ़ॉर्मूला|प्रथम-क्रम तर्क के सुगठित वाक्यों का समुच्चय है, जिसमें सार्वभौमिक परिमाणक और अस्तित्वगत परिमाणक और वास्तविक चरों पर अभिव्यक्ति की समानता और असमानताओं के तार्किक संयोजन शामिल होते हैं। . संबंधित प्रथम-क्रम सिद्धांत (गणितीय तर्क) वाक्यों का समूह है जो वास्तव में वास्तविक संख्याओं के लिए सत्य है। ऐसे कई अलग-अलग सिद्धांत हैं, जिनमें अलग-अलग अभिव्यंजक शक्ति होती है, जो अभिव्यक्ति में उपयोग करने की अनुमति वाले आदिम संचालन पर निर्भर करता है। इन सिद्धांतों के अध्ययन में एक बुनियादी सवाल यह है कि क्या वे निर्णायकता (तर्क) हैं: यानी, क्या कोई कलन विधि है जो एक वाक्य को इनपुट के रूप में ले सकता है और आउटपुट के रूप में इस सवाल का उत्तर हां या ना में दे सकता है कि वाक्य सच है या नहीं सिद्धांत में.
वास्तविक बंद क्षेत्रों का सिद्धांत वह सिद्धांत है जिसमें आदिम संक्रियाएँ गुणन और जोड़ हैं; इसका तात्पर्य यह है कि, इस सिद्धांत में, केवल वही संख्याएँ परिभाषित की जा सकती हैं जो वास्तविक बीजगणितीय संख्याएँ हैं। जैसा कि अल्फ्रेड टार्स्की ने सिद्ध किया है, यह सिद्धांत निर्णायक है; टार्स्की-सीडेनबर्ग प्रमेय और क्वांटिफ़ायर उन्मूलन देखें। वास्तविक बंद क्षेत्रों के सिद्धांत के लिए निर्णय प्रक्रियाओं का वर्तमान कार्यान्वयन अक्सर बेलनाकार बीजगणितीय अपघटन द्वारा क्वांटिफायर उन्मूलन पर आधारित होता है।
टार्स्की की घातीय फ़ंक्शन समस्या इस सिद्धांत के एक अन्य आदिम ऑपरेशन, घातीय फ़ंक्शन के विस्तार से संबंधित है। यह एक खुली समस्या है कि क्या यह सिद्धांत निर्णायक है, लेकिन यदि शैनुएल का अनुमान सही बैठता है तो इस सिद्धांत की निर्णायकता का पालन होगा।[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.