प्रमाण में कट क्या होता है?

कट नियम किसी को एक लेम्मा सिद्ध करने और फिर उसका उपयोग करने की अनुमति देता है: एक सूत्र को स्थापित करने वाली व्युत्पत्ति से और उस सूत्र को एक आधार के रूप में उपयोग करने वाली दूसरी व्युत्पत्ति से, यह संयुक्त परिणाम का निष्कर्ष निकालता है। कट-एलिमिनेशन दर्शाता है कि ऐसे मध्यवर्ती लेम्मा को सिद्धांत रूप में हमेशा हटाया जा सकता है।

कट को समाप्त करने से प्रमाण बहुत लंबे क्यों हो सकते हैं?

कट को हटाने के लिए व्युत्पत्ति के बड़े हिस्सों को दोहराने की आवश्यकता हो सकती है, और इसे दोहराने से प्रमाण का आकार घातांकों के एक टावर (tower of exponentials) तक बढ़ सकता है। इसलिए कट-मुक्त प्रमाण वैचारिक रूप से सरल होते हैं लेकिन कट वाले मूल प्रमाणों की तुलना में बहुत बड़े हो सकते हैं।

कट-एलिमिनेशन (Cut-Elimination)

कट-एलिमिनेशन (Cut-elimination) जेंट्ज़ेन का प्रमेय है कि कट नियम (cut rule), जो लेम्मा (lemmas) के उपयोग को औपचारिक रूप देता है, को किसी भी सीक्वेंट कैलकुलस (sequent calculus) प्रमाण से हटाया जा सकता है, जिससे केवल उन सूत्रों से बना प्रमाण शेष रहता है जिनसे वह संबंधित है।

PaperMind से विषय खोजेंजल्द हीFind papers & topics

Tools & resources

स्लाइड डाउनलोड करें

Learn & explore

वीडियोजल्द ही

Definition

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

Scope

यह विषय कट नियम और सीक्वेंट कैलकुलस में इसकी भूमिका, कट-एलिमिनेशन प्रक्रिया और इसकी समाप्ति, कट-मुक्त प्रमाणों की सबफॉर्मूला प्रॉपर्टी (subformula property), परिणामी सुसंगति (consistency) और निर्णयक्षमता (decidability) के परिणाम, और प्रमाण के आकार पर एलिमिनेशन के कारण लगने वाली सीमाएं शामिल करता है।

Core questions

कट नियम क्या व्यक्त करता है और इसका निष्कासन क्यों महत्वपूर्ण है?
कट-एलिमिनेशन प्रक्रिया कैसे समाप्त होती है?
सबफॉर्मूला प्रॉपर्टी क्या है और यह प्रमाण खोज के लिए क्या निहितार्थ रखती है?
कट को समाप्त करने की कम्प्यूटेशनल लागत क्या है?

Key theories

जेंट्ज़ेन हौप्टसत्ज़ (Gentzen Hauptsatz): जेंट्ज़ेन का मुख्य प्रमेय बताता है कि कट नियम सीक्वेंट कैलकुलस में स्वीकार्य है, इसलिए कट का उपयोग करने वाले किसी भी प्रमाण को उसी अंतिम सीक्वेंट के कट-मुक्त प्रमाण में परिवर्तित किया जा सकता है।
सबफॉर्मूला प्रॉपर्टी (Subformula property): कट-मुक्त प्रमाण में होने वाला प्रत्येक सूत्र अंतिम सीक्वेंट का एक सबफॉर्मूला होता है, जो प्रमाण के आकार को सीमित करता है और निर्णय प्रक्रियाओं तथा सुसंगति तर्कों का आधार बनता है।
कट-एलिमिनेशन के माध्यम से सुसंगति (Consistency via cut-elimination): चूंकि खाली सीक्वेंट का कट-मुक्त प्रमाण असंभव है, कट-एलिमिनेशन एक सीधा प्रमाण प्रदान करता है कि कैलकुलस, और इसलिए वह सिद्धांत जिसे यह औपचारिक रूप देता है, सुसंगत है।

Clinical relevance

कट-एलिमिनेशन व्यापक परिणामों वाला एक मूलभूत परिणाम है: यह सुसंगति प्रमाण (consistency proofs), स्वचालित प्रमेय सिद्धिकरण (automated theorem proving) और झांकी विधियों (tableau methods) के लिए आवश्यक सबफॉर्मूला प्रॉपर्टी (subformula property), इंटरपोलेशन प्रमेय (interpolation theorems), और, प्रमाण-के-रूप-में-प्रोग्राम (proofs-as-programs) पत्राचार के माध्यम से, टाइप किए गए प्रोग्रामों का सामान्यीकरण (normalization) प्रदान करता है।

History

जेंट्ज़ेन ने 1934 में प्रथम-क्रम तर्क (first-order logic) के लिए कट-एलिमिनेशन, अपने हौप्टसत्ज़ (Hauptsatz) को सिद्ध किया, और यह विधि संरचनात्मक प्रमाण सिद्धांत (structural proof theory) की आधारशिला बन गई। टैट (Tait) और गिरार्ड (Girard) ने इस तकनीक को मजबूत प्रणालियों और उच्च-क्रम तर्क (higher-order logic) तक बढ़ाया, और कट-एलिमिनेशन के तहत प्रमाण के आकार में वृद्धि की सीमाएं अपने आप में अध्ययन का विषय बन गईं।

Key figures

Gerhard Gentzen
William Tait
Jean-Yves Girard
Gaisi Takeuti

Seminal works

takeuti1987
troelstra2000
negri2001

Frequently asked questions

प्रमाण में कट क्या होता है?: कट नियम किसी को एक लेम्मा सिद्ध करने और फिर उसका उपयोग करने की अनुमति देता है: एक सूत्र को स्थापित करने वाली व्युत्पत्ति से और उस सूत्र को एक आधार के रूप में उपयोग करने वाली दूसरी व्युत्पत्ति से, यह संयुक्त परिणाम का निष्कर्ष निकालता है। कट-एलिमिनेशन दर्शाता है कि ऐसे मध्यवर्ती लेम्मा को सिद्धांत रूप में हमेशा हटाया जा सकता है।
कट को समाप्त करने से प्रमाण बहुत लंबे क्यों हो सकते हैं?: कट को हटाने के लिए व्युत्पत्ति के बड़े हिस्सों को दोहराने की आवश्यकता हो सकती है, और इसे दोहराने से प्रमाण का आकार घातांकों के एक टावर (tower of exponentials) तक बढ़ सकता है। इसलिए कट-मुक्त प्रमाण वैचारिक रूप से सरल होते हैं लेकिन कट वाले मूल प्रमाणों की तुलना में बहुत बड़े हो सकते हैं।