उच्च-क्रम तर्क
अंक शास्त्र और तर्क में, उच्च-क्रम तर्क विधेय तर्क का एक रूप है जो अतिरिक्त परिमाणीकरण और कभी-कभी, तर्क के सुदृढ़ शब्दार्थ द्वारा प्रथम-क्रम तर्क से अलग होता है। अपने मानक शब्दार्थ के साथ उच्च-क्रम तर्क अधिक अभिव्यंजक हैं, परंतु उनके मॉडल सैद्धांतिक गुण पहले-क्रम तर्क की तुलना में कम अच्छे व्यवहार वाले हैं।
शब्द "उच्च-क्रम तर्क" का प्रयोग सामान्यतः उच्च-क्रम सरल विधेय तर्क के लिए किया जाता है। यहां "सरल" इंगित करता है कि अंतर्निहित प्रकार का सिद्धांत सरल प्रकारों का सिद्धांत है, जिसे प्रकारों का सरल सिद्धांत भी कहा जाता है। लियोन च्विस्टेक और फ्रैंक पी. रैमसे ने इसे अल्फ्रेड नॉर्थ व्हाइटहेड और बर्ट्रेंड रसेल द्वारा अंक शास्त्र सिद्धांत में निर्दिष्ट प्रकारों के सम्मिश्र और अकृत्रिम व्यापक सिद्धांत के सरलीकरण के रूप में प्रस्तावित किया है। सरल प्रकार का अर्थ कभी-कभी बहुरूपी और आश्रित प्रकारों को बाहर करना भी होता है।[1]
परिमाणीकरण का क्षेत्र
प्रथम-क्रम तर्क केवल उन चरों की मात्रा निर्धारित करता है जो व्यक्तियों से भिन्न होते हैं; इसके अतिरिक्त, दूसरे क्रम का तर्क, सेटों की मात्रा भी निर्धारित करता है; तीसरे क्रम का तर्क भी सेटों के सेट आदि की मात्रा निर्धारित करता है।
उच्च-क्रम तर्क पहले-, दूसरे-, तीसरे-, ..., नथ-क्रम तर्क का मिलन है; अर्थात्, उच्च-क्रम तर्क उन सेटों पर परिमाणीकरण को स्वीकार करता है जो मनमाने ढंग से गहराई से निहित होते हैं।
शब्दार्थ
उच्च-क्रम तर्क के लिए दो संभावित शब्दार्थ हैं।
मानक या पूर्ण शब्दार्थ में, उच्च-प्रकार की वस्तुओं पर परिमाणवाचक उस प्रकार की सभी संभावित वस्तुओं पर आधारित होते हैं। उदाहरण के लिए, व्यक्तियों के समूह पर एक परिमाणक व्यक्तियों के समूह की संपूर्ण शक्ति समूह पर निर्भर करता है। इस प्रकार, मानक शब्दार्थ में, एक बार व्यक्तियों का सेट निर्दिष्ट हो जाने पर, यह सभी परिमाणकों को निर्दिष्ट करने के लिए पर्याप्त है। मानक शब्दार्थ के साथ HOL प्रथम-क्रम तर्क की तुलना में अधिक अभिव्यंजक है। उदाहरण के लिए, HOL प्राकृतिक संख्याओं और वास्तविक संख्याओं के श्रेणीबद्ध स्वयंसिद्धीकरण को स्वीकार करता है, जो प्रथम-क्रम तर्क के साथ असंभव है। चूंकि, कर्ट गोडेल के परिणाम के अनुसार, मानक शब्दार्थ के साथ HOL एक प्रभावी, ठोस और पूर्ण प्रमाण कलन को स्वीकार नहीं करता है।[2] मानक शब्दार्थ के साथ HOL के मॉडल-सैद्धांतिक गुण भी प्रथम-क्रम तर्क की तुलना में अधिक सम्मिश्र हैं। उदाहरण के लिए, दूसरे क्रम के तर्क की लोवेनहेम संख्या पहले मापने योग्य कार्डिनल से पहले से ही बड़ी है, यदि ऐसा कोई प्रमुख सम्मलित है।[3] इसके विपरीत, प्रथम-क्रम तर्क की लोवेनहेम संख्या ℵ0 है, जो सबसे छोटा अनंत प्रमुख है।
हेनकिन शब्दार्थ में, प्रत्येक उच्च-क्रम प्रकार के लिए प्रत्येक व्याख्या में एक अलग डोमेन सम्मलित किया गया है। इस प्रकार, उदाहरण के लिए, व्यक्तियों के समूह पर परिमाणक व्यक्तियों के समूह की शक्तियों के केवल एक उपसमूह तक ही सीमित हो सकते हैं। इन शब्दार्थों के साथ HOL प्रथम-क्रम तर्क से अधिक ठोस होने के अतिरिक्त, कई-क्रमबद्ध प्रथम-क्रम तर्क के बराबर है। विशेष रूप से, हेनकिन शब्दार्थ के साथ HOL में प्रथम-क्रम तर्क के सभी मॉडल-सैद्धांतिक गुण हैं, और प्रथम-क्रम तर्क से विरासत में मिली एक पूर्ण, ठोस, प्रभावी प्रमाण प्रणाली है।
गुण
उच्च-क्रम तर्कशास्त्र में चर्च के प्रकार के सरल सिद्धांत की शाखाएं[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.
