उच्च-क्रम तर्क
गणित और तर्क में, उच्च-क्रम तर्क (संक्षिप्त एचओएल) विधेय तर्क का एक रूप है जो अतिरिक्त परिमाणीकरण (तर्क) और कभी-कभी, तर्क के मजबूत शब्दार्थ द्वारा प्रथम-क्रम तर्क से अलग होता है। अपने मानक शब्दार्थ के साथ उच्च-क्रम तर्क अधिक अभिव्यंजक हैं, लेकिन उनके मॉडल सिद्धांत|मॉडल-सैद्धांतिक गुण प्रथम-क्रम तर्क की तुलना में कम अच्छे व्यवहार वाले हैं।
उच्च-क्रम तर्क शब्द का प्रयोग आमतौर पर उच्च-क्रम सरल विधेय तर्क के लिए किया जाता है। यहां सरल इंगित करता है कि अंतर्निहित प्रकार का सिद्धांत सरल प्रकार का सिद्धांत है, जिसे सरल प्रकार का सिद्धांत भी कहा जाता है। लियोन च्विस्टेक और फ्रैंक पी. रैमसे ने इसे अल्फ्रेड नॉर्थ व्हाइटहेड और बर्ट्रेंड रसेल द्वारा गणितीय सिद्धांत में निर्दिष्ट जटिल और अनाड़ी प्रकार के जटिल सिद्धांत के सरलीकरण के रूप में प्रस्तावित किया। सरल प्रकार का अर्थ कभी-कभी प्रकार की बहुरूपता और आश्रित प्रकार के प्रकारों को बाहर करना भी होता है।[1]
परिमाणीकरण का दायरा
प्रथम-क्रम तर्क केवल उन चरों की मात्रा निर्धारित करता है जो व्यक्तियों से भिन्न होते हैं; इसके अलावा, दूसरे क्रम का तर्क, सेटों की मात्रा भी निर्धारित करता है; तीसरे क्रम का तर्क भी सेटों के सेट आदि की मात्रा निर्धारित करता है।
उच्च-क्रम तर्क पहले-, दूसरे-, तीसरे-, ..., एनवें-क्रम तर्क का मिलन है; यानी, उच्च-क्रम तर्क उन सेटों पर परिमाणीकरण को स्वीकार करता है जो मनमाने ढंग से गहराई से निहित होते हैं।
शब्दार्थ
उच्च-क्रम तर्क के लिए दो संभावित शब्दार्थ हैं।
मानक या पूर्ण शब्दार्थ में, उच्च-प्रकार की वस्तुओं पर क्वांटिफायर उस प्रकार की सभी संभावित वस्तुओं पर आधारित होते हैं। उदाहरण के लिए, व्यक्तियों के समूह पर एक परिमाणक व्यक्तियों के समूह की संपूर्ण शक्ति समूह पर निर्भर करता है। इस प्रकार, मानक शब्दार्थ में, एक बार व्यक्तियों का सेट निर्दिष्ट हो जाने पर, यह सभी परिमाणकों को निर्दिष्ट करने के लिए पर्याप्त है। मानक शब्दार्थ के साथ एचओएल प्रथम-क्रम तर्क की तुलना में अधिक अभिव्यंजक है। उदाहरण के लिए, एचओएल प्राकृतिक संख्याओं और वास्तविक संख्याओं के मॉर्ले के श्रेणीबद्धता प्रमेय स्वयंसिद्धीकरण को स्वीकार करता है, जो प्रथम-क्रम तर्क के साथ असंभव है। हालाँकि, कर्ट गोडेल के परिणामस्वरूप, मानक शब्दार्थ के साथ एचओएल एक गणना योग्य फ़ंक्शन, ध्वनि और गोडेल की पूर्णता प्रमेय प्रमाण कलन को स्वीकार नहीं करता है।[2] मानक शब्दार्थ के साथ एचओएल के मॉडल-सैद्धांतिक गुण भी प्रथम-क्रम तर्क की तुलना में अधिक जटिल हैं। उदाहरण के लिए, दूसरे क्रम के तर्क की लोवेनहेम संख्या पहले मापने योग्य कार्डिनल से पहले से ही बड़ी है, यदि ऐसा कोई कार्डिनल मौजूद है।[3] इसके विपरीत, प्रथम-क्रम तर्क की लोवेनहेम संख्या एलेफ़ नॉट|ℵ है0, सबसे छोटा अनंत कार्डिनल।
हेनकिन शब्दार्थ में, प्रत्येक उच्च-क्रम प्रकार के लिए प्रत्येक व्याख्या में एक अलग डोमेन शामिल किया गया है। इस प्रकार, उदाहरण के लिए, व्यक्तियों के समूह पर परिमाणक व्यक्तियों के समूह की शक्तियों के केवल एक उपसमूह तक ही सीमित हो सकते हैं। इन शब्दार्थों के साथ एचओएल प्रथम-क्रम तर्क से अधिक मजबूत होने के बजाय, कई-क्रमबद्ध प्रथम-क्रम तर्क के बराबर है। विशेष रूप से, हेनकिन शब्दार्थ के साथ एचओएल में प्रथम-क्रम तर्क के सभी मॉडल-सैद्धांतिक गुण हैं, और प्रथम-क्रम तर्क से विरासत में मिली एक पूर्ण, ठोस, प्रभावी प्रमाण प्रणाली है।
गुण
उच्च-क्रम तर्कशास्त्र में अलोंजो चर्च के प्रकार के सरल सिद्धांत की शाखाएं शामिल हैं[4] और अंतर्ज्ञानवादी प्रकार के सिद्धांत के विभिन्न रूप। जेरार्ड ह्यूएट ने दिखाया है कि एकीकरण (कंप्यूटर विज्ञान)#उच्च-क्रम एकीकरण अंतर्ज्ञानवादी प्रकार के सिद्धांत में अनिर्णीत समस्या है|तीसरे क्रम के तर्क का प्रकार-सैद्धांतिक स्वाद,[5][6][7][8] यानी, यह तय करने के लिए कोई एल्गोरिदम नहीं हो सकता है कि दूसरे क्रम (उच्च क्रम के मनमाने ढंग से) शब्दों के बीच एक मनमाना समीकरण का कोई समाधान है या नहीं।
समरूपता की एक निश्चित धारणा तक, पावरसेट ऑपरेशन दूसरे क्रम के तर्क में निश्चित है। इस अवलोकन का उपयोग करते हुए, जाक्को हिन्तिक्का ने 1955 में स्थापित किया कि दूसरे क्रम का तर्क इस अर्थ में उच्च-क्रम तर्क का अनुकरण कर सकता है कि उच्च-क्रम तर्क के प्रत्येक सूत्र के लिए, दूसरे क्रम के तर्क में इसके लिए एक समतुल्यता सूत्र पाया जा सकता है।[9] उच्च-क्रम तर्क शब्द को कुछ संदर्भों में शास्त्रीय तर्क उच्च-क्रम तर्क के संदर्भ में ग्रहण किया जाता है। हालाँकि, मोडल तर्क उच्च-क्रम लॉजिक का भी अध्ययन किया गया है। कई तर्कशास्त्रियों के अनुसार, गोडेल के ऑन्टोलॉजिकल प्रमाण का ऐसे संदर्भ में (तकनीकी दृष्टिकोण से) सबसे अच्छा अध्ययन किया जाता है।[10]
यह भी देखें
- शून्य-क्रम तर्क (प्रस्तावात्मक तर्क)
- प्रथम-क्रम तर्क
- दूसरे क्रम का तर्क
- प्रकार सिद्धांत
- उच्च कोटि का व्याकरण
- उच्च-क्रम तर्क प्रोग्रामिंग
- एचओएल (प्रमाण सहायक)
- अनेक प्रकार के तर्क
- टाइप किया गया लैम्ब्डा कैलकुलस
- मोडल लॉजिक
टिप्पणियाँ
- ↑ Jacobs, 1999, chapter 5
- ↑ Shapiro 1991, p. 87.
- ↑ Menachem Magidor and Jouko Väänänen. "On Löwenheim-Skolem-Tarski numbers for extensions of first order logic", Report No. 15 (2009/2010) of the Mittag-Leffler Institute.
- ↑ Alonzo Church, A formulation of the simple theory of types, The Journal of Symbolic Logic 5(2):56–68 (1940)
- ↑ Huet, Gérard P. (1973). "तीसरे क्रम के तर्क में एकीकरण की अनिश्चितता". Information and Control. 22 (3): 257–267. doi:10.1016/s0019-9958(73)90301-x.
- ↑ Huet, Gérard (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (Ph.D.) (in French). Universite de Paris VII.
{{cite thesis}}: CS1 maint: unrecognized language (link) - ↑ Warren D. Goldfarb (1981). "द्वितीय-क्रम एकीकरण समस्या की अनिर्णयता" (PDF). Theoretical Computer Science. 13: 225–230.
- ↑ Huet, Gérard (2002). "Higher Order Unification 30 years later" (PDF). In Carreño, V.; Muñoz, C.; Tahar, S. (eds.). Proceedings, 15th International Conference TPHOL. LNCS. Vol. 2410. Springer. pp. 3–12.
- ↑ entry on HOL
- ↑ Fitting, Melvin (2002). Types, Tableaus, and Gödel's God. Springer Science & Business Media. p. 139. ISBN 978-1-4020-0604-3.
Godel's argument is modal and at least second-order, since in his definition of God there is an explicit quantification over properties. [...] [AG96] showed that one could view a part of the argument not as second-order, but as third-order.
संदर्भ
- Andrews, Peter B. (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed, Kluwer Academic Publishers, ISBN 1-4020-0763-9
- Stewart Shapiro, 1991, "Foundations Without Foundationalism: A Case for Second-Order Logic". Oxford University Press., ISBN 0-19-825029-0
- Stewart Shapiro, 2001, "Classical Logic II: Higher Order Logic," in Lou Goble, ed., The Blackwell Guide to Philosophical Logic. Blackwell, ISBN 0-631-20693-0
- Lambek, J. and Scott, P. J., 1986. Introduction to Higher Order Categorical Logic, Cambridge University Press, ISBN 0-521-35653-9
- Jacobs, Bart (1999). Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141. North Holland, Elsevier. ISBN 0-444-50170-3.
- Benzmüller, Christoph; Miller, Dale (2014). "Automation of Higher-Order Logic". In Gabbay, Dov M.; Siekmann, Jörg H.; Woods, John (eds.). Handbook of the History of Logic, Volume 9: Computational Logic. Elsevier. ISBN 978-0-08-093067-1.
बाहरी संबंध
- Andrews, Peter B, Church's Type Theory in Stanford Encyclopedia of Philosophy.
- Miller, Dale, 1991, "Logic: Higher-order," Encyclopedia of Artificial Intelligence, 2nd ed.
- Herbert B. Enderton, Second-order and Higher-order Logic in Stanford Encyclopedia of Philosophy, published Dec 20, 2007; substantive revision Mar 4, 2009.
