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

कट-उन्मूलन प्रमेय (या जेंटज़ेन का हौप्त्सत्ज़) अनुक्रमिक कलन के महत्व को स्थापित करने वाला केंद्रीय परिणाम है। इसे मूल रूप से गेरहार्ड जेंटज़न ने अपने ऐतिहासिक 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}$ …)।" ध्यान दें कि बाएं हाथ की ओर (एलएचएस) एक संयोजन (और) है और दाईं ओर (आरएचएस) एक विच्छेदन (या) है।

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

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

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