कट-उन्मूलन प्रमेय

कट-उन्मूलन प्रमेय (या जेंटज़ेन का हौप्त्सत्ज़) अनुक्रमिक कलन के महत्व को स्थापित करने वाला केंद्रीय परिणाम है। इसे मूल रूप से गेरहार्ड जेंटज़न ने अपने ऐतिहासिक 1934 के पेपर इन्वेस्टिगेशंस इन लॉजिकल डिडक्शन में सिस्टम सिस्टम एल.जे और सिस्टम एलके के लिए क्रमशः अंतर्ज्ञानवादी तर्क और शास्त्रीय तर्क को औपचारिक रूप से साबित किया था। कट-उन्मूलन प्रमेय में कहा गया है कि कोई भी निर्णय जिसमें कट नियम का उपयोग करते हुए अनुक्रमिक कलन में प्रमाण होता है, उसके पास कट-मुक्त प्रमाण भी होता है, अर्थात ऐसा प्रमाण जो कट नियम का उपयोग नहीं करता है।

कटौती नियम

अनुक्रम एक तार्किक अभिव्यक्ति है जो कई सूत्रों से संबंधित होती है "$A_{1},A_{2},A_{3},\ldots \vdash B_{1},B_{2},B_{3},\ldots$", जिसे इस प्रकार पढ़ा जाना चाहिए "$A_{1},A_{2},A_{3},\ldots$ सिद्ध होता है $B_{1},B_{2},B_{3},\ldots$", और (जैसा कि जेंटज़ेन द्वारा स्पष्ट किया गया है) को सत्य-कार्य के समतुल्य समझा जाना चाहिए यदि ($A_{1}$ और $A_{2}$ और $A_{3}$ …) तब ($B_{1}$ या $B_{2}$ या $B_{3}$ …). ध्यान दें कि बाईं ओर (LHS) एक संयोजन (और) है और दाईं ओर (RHS) एक वियोजन (या) है।

एलएचएस में मनमाने ढंग से कई या कुछ सूत्र हो सकते हैं; जब एलएचएस खाली होता है, तो आरएचएस एक टॉटोलॉजी (तर्क) है। एलके में, आरएचएस में किसी भी संख्या में सूत्र हो सकते हैं - यदि इसमें कोई भी नहीं है, तो एलएचएस एक विरोधाभास है, जबकि एलजे में आरएचएस में केवल एक सूत्र हो सकता है या कोई भी नहीं: यहां हम देखते हैं कि आरएचएस में एक से अधिक सूत्र की अनुमति देना है समतुल्य, सही संकुचन नियम की उपस्थिति में, बहिष्कृत मध्य के कानून की स्वीकार्यता के लिए। हालाँकि, अनुक्रमिक कैलकुलस एक काफी अभिव्यंजक रूपरेखा है, और प्रस्तावित अंतर्ज्ञानवादी तर्क के लिए अनुक्रमिक कैलकुली हैं जो आरएचएस में कई सूत्रों की अनुमति देते हैं। जीन-यवेस गिरार्ड के तर्क एलसी से शास्त्रीय तर्क की एक प्राकृतिक औपचारिकता प्राप्त करना आसान है जहां आरएचएस में अधिकतम एक सूत्र होता है; यह तार्किक और संरचनात्मक नियमों की परस्पर क्रिया है जो यहां की कुंजी है।

अनुक्रमिक कैलकुलस के सामान्य कथन में कट एक नियम है, और अन्य प्रमाण सिद्धांत में विभिन्न नियमों के बराबर है, जो दिया गया है

1. $\Gamma \vdash A,\Delta$

और

1. $\Pi ,A\vdash \Lambda$

किसी को अनुमान लगाने की अनुमति देता है

1. $\Gamma ,\Pi \vdash \Delta ,\Lambda$

अर्थात् यह सूत्र की घटनाओं को काट देता है $A$ अनुमानित संबंध से बाहर.

कटौती उन्मूलन

कट-उन्मूलन प्रमेय में कहा गया है कि (किसी दिए गए सिस्टम के लिए) कट नियम का उपयोग करके सिद्ध किए जाने वाले किसी भी अनुक्रम को इस नियम के उपयोग के बिना सिद्ध किया जा सकता है।

अनुक्रमिक गणनाओं के लिए जिनका आरएचएस में केवल एक सूत्र है, कट नियम दिया गया है

1. $\Gamma \vdash A$

और

1. $\Pi ,A\vdash B$

किसी को अनुमान लगाने की अनुमति देता है

1. $\Gamma ,\Pi \vdash B$

अगर हम सोचें $B$ एक प्रमेय के रूप में, तो इस मामले में कट-उन्मूलन केवल एक लेम्मा कहता है $A$ इस प्रमेय को सिद्ध करने के लिए इनलाइन किया जा सकता है। जब भी प्रमेय के प्रमाण में लेम्मा (गणित) का उल्लेख होता है $A$, हम प्रमाण के स्थान पर घटनाओं को प्रतिस्थापित कर सकते हैं $A$. फलस्वरूप, कटौती नियम स्वीकार्य नियम है।

प्रमेय के परिणाम

अनुक्रमिक कलन में तैयार की गई प्रणालियों के लिए, विश्लेषणात्मक प्रमाण वे प्रमाण हैं जो कट का उपयोग नहीं करते हैं। आमतौर पर ऐसा प्रमाण निश्चित रूप से लंबा होगा, और जरूरी नहीं कि यह तुच्छ हो। अपने निबंध डोंट एलिमिनेट कट में! जॉर्ज बूलोस ने प्रदर्शित किया कि एक व्युत्पत्ति थी जिसे कट का उपयोग करके एक पृष्ठ में पूरा किया जा सकता था, लेकिन जिसका विश्लेषणात्मक प्रमाण ब्रह्मांड के जीवनकाल में पूरा नहीं किया जा सकता था।

इस प्रमेय के कई, समृद्ध परिणाम हैं:

• एक प्रणाली निरंतरता प्रमाण है यदि वह बेतुके प्रमाण को स्वीकार करती है। यदि सिस्टम में कट उन्मूलन प्रमेय है, तो यदि उसके पास बेतुके, या खाली अनुक्रम का प्रमाण है, तो उसके पास बिना कटौती के, बेतुके (या खाली अनुक्रम) का प्रमाण भी होना चाहिए। आमतौर पर यह जांचना बहुत आसान है कि ऐसा कोई सबूत तो नहीं है। इस प्रकार, एक बार जब किसी सिस्टम में कट एलिमिनेशन प्रमेय दिखाया जाता है, तो यह आमतौर पर तत्काल होता है कि सिस्टम सुसंगत है।
• आम तौर पर सिस्टम में, कम से कम प्रथम क्रम तर्क में, उप-सूत्र संपत्ति, प्रमाण-सैद्धांतिक शब्दार्थ के कई दृष्टिकोणों में एक महत्वपूर्ण संपत्ति होती है।

क्रेग प्रक्षेप को साबित करने के लिए कट एलिमिनेशन सबसे शक्तिशाली उपकरणों में से एक है। प्रथम-क्रम रिज़ॉल्यूशन के आधार पर प्रमाण खोज करने की संभावना, प्रोलॉग प्रोग्रामिंग भाषा के लिए आवश्यक अंतर्दृष्टि, उपयुक्त प्रणाली में कट की स्वीकार्यता पर निर्भर करती है।

करी-हावर्ड समरूपता के माध्यम से उच्च-क्रम टाइप किए गए लैम्ब्डा कैलकुलस पर आधारित प्रूफ सिस्टम के लिए, कट एलिमिनेशन एल्गोरिदम सामान्यीकरण संपत्ति (सार पुनर्लेखन) के अनुरूप होते हैं (प्रत्येक प्रूफ शब्द चरणों की एक सीमित संख्या में एक सामान्य रूप (शब्द पुनर्लेखन) में कम हो जाता है)।

यह भी देखें

• कटौती प्रमेय
• पीनो के सिद्धांतों के लिए जेंटज़ेन की संगति प्रमाण

संदर्भ

• Gentzen, Gerhard (1935). "Untersuchungen über das logische Schließen. I.". Mathematische Zeitschrift. 39: 176–210. doi:10.1007/BF01201353.
  • Untersuchungen über das logische Schließen I (Archive.org)
  • Gentzen, Gerhard (1964). "Investigations into logical deduction". American Philosophical Quarterly. 1 (4): 249–287.
• Gentzen, Gerhard (1935). "Untersuchungen über das logische Schließen. II". Mathematische Zeitschrift. 39: 405–431. doi:10.1007/BF01201363.
  • Untersuchungen über das logische Schließen II (Archive.org)
  • Gentzen, Gerhard (1965). "Investigations into logical deduction". American Philosophical Quarterly. 2 (3): 204–218.
• Curry, Haskell Brooks (1977) [1963]. Foundations of mathematical logic. New York: Dover Publications Inc. ISBN 978-0-486-63462-3.
• Kleene, Stephen Cole (2009) [1952]. Introduction to metamathematics. Ishi Press International. ISBN 978-0-923891-57-2.
• Boolos, George (1984). "Don't eliminate cut". Journal of Philosophical Logic. 13 (4): 373–378.

बाहरी संबंध

• Alex Sakharov. "Cut Elimination Theorem". MathWorld.
• Dragalin, A.G. (2001) [1994], "Sequent calculus", Encyclopedia of Mathematics, EMS Press