प्राकृतिक निगमन और सीक्वेंट कैलकुलस

प्राकृतिक निगमन और सीक्वेंट कैलकुलस दो जेंट्ज़ेन-शैली की औपचारिक प्रणालियाँ हैं जो तार्किक संयोजकों के लिए परिचय और उन्मूलन नियमों के माध्यम से प्रमाणों का प्रतिनिधित्व करती हैं, जो संरचनात्मक प्रमाण सिद्धांत की मूल कार्यप्रणाली का निर्माण करती हैं।

Definition

प्राकृतिक निगमन अनौपचारिक तर्क को दर्शाने वाले परिचय और उन्मूलन नियमों का उपयोग करके मान्यताओं से सूत्रों को व्युत्पन्न करता है, जबकि सीक्वेंट कैलकुलस सीक्वेंट्स (यह दावा कि सूत्रों की एक सूची दूसरे को समाहित करती है) को एक निहितार्थ के बाईं और दाईं ओर कार्य करने वाले नियमों के माध्यम से हेरफेर करता है।

Scope

यह विषय प्राकृतिक निगमन के नियमों को उनके परिचय और उन्मूलन युग्मों के साथ, सीक्वेंट कैलकुलस की संरचना को उसके बाएँ और दाएँ नियमों तथा संरचनात्मक नियमों के साथ, प्राकृतिक निगमन के लिए सामान्यीकरण, दोनों प्रणालियों के बीच संबंध, और उनके अंतर्ज्ञानवादी तथा शास्त्रीय रूपों को शामिल करता है।

Core questions

• परिचय और उन्मूलन नियम तार्किक संयोजकों को अर्थ कैसे प्रदान करते हैं?
• सीक्वेंट क्या है और इसके नियम प्राकृतिक निगमन के नियमों से कैसे भिन्न हैं?
• सामान्यीकरण प्राकृतिक निगमन प्रमाणों को कैसे सरल बनाता है?
• इन कैलकुलस के शास्त्रीय और अंतर्ज्ञानवादी संस्करण कैसे संबंधित हैं?

Key theories

परिचय और उन्मूलन नियम

प्रत्येक संयोजक उन नियमों द्वारा शासित होता है जो इसे प्रस्तुत करते हैं और उन नियमों द्वारा जो इसका शोषण करते हैं, और उनकी समरसता, कि उन्मूलन ठीक वही पुनर्प्राप्त करता है जो परिचय डालता है, संयोजक के अर्थ को व्यक्त करता है।

सामान्यीकरण प्रमेय

प्राविट्ज़ ने दिखाया कि प्राकृतिक निगमन प्रमाणों को एक सामान्य रूप में कम किया जा सकता है जो उन चक्करों से मुक्त होता है जहाँ एक परिचय को तुरंत एक उन्मूलन द्वारा पूर्ववत किया जाता है, जो कट-उन्मूलन के प्राकृतिक निगमन का अनुरूप है।

दो कैलकुलस का पत्राचार

प्राकृतिक निगमन और सीक्वेंट कैलकुलस समान प्रमेयों को सिद्ध करते हैं और एक दूसरे में अनुवादित किए जा सकते हैं, जिसमें सीक्वेंट बाएँ नियम प्राकृतिक निगमन उन्मूलन नियमों के अनुरूप होते हैं।

Clinical relevance

ये कैलकुलस प्रमाणों का संरचनात्मक रूप से अध्ययन करने के लिए मानक प्रारूप हैं: प्राकृतिक निगमन प्रकार सिद्धांत (type theory) और प्रमाण सहायकों (proof assistants) को प्रमाण-के-रूप-में-कार्यक्रम (proofs-as-programs) पत्राचार के माध्यम से रेखांकित करता है, जबकि सीक्वेंट कैलकुलस, कट-उन्मूलन (cut-elimination) के बाद अपने उपसूत्र गुण (subformula property) के साथ, स्वचालित प्रमाण खोज और विश्लेषणात्मक सारणियों का आधार है।

History

जेंट्ज़ेन ने 1934 और 1935 में प्राकृतिक निगमन और सीक्वेंट कैलकुलस दोनों को प्रस्तुत किया, प्राकृतिक निगमन का विश्लेषण करना कठिन लगने के बाद अपने कट-उन्मूलन प्रमेय को प्राप्त करने के लिए सीक्वेंट कैलकुलस तैयार किया। प्राविट्ज़ ने 1965 में एक गहन सामान्यीकरण अध्ययन के साथ प्राकृतिक निगमन को पुनर्जीवित किया, और ये प्रणालियाँ बाद के प्रमाण-के-रूप-में-कार्यक्रम विकास के लिए केंद्रीय बन गईं।

Key figures

• Gerhard Gentzen
• Dag Prawitz
• Stanislaw Jaskowski
• Jan von Plato

Seminal works

• troelstra2000
• prawitz1965
• negri2001

Frequently asked questions

प्राकृतिक निगमन और सीक्वेंट कैलकुलस में क्या अंतर है?

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

सामान्यीकरण क्यों महत्वपूर्ण है?

एक सामान्य प्रमाण में कोई चक्कर नहीं होता है और इसमें उपसूत्र गुण होता है, इसलिए इसमें प्रत्येक सूत्र निष्कर्ष या आधार का एक उपसूत्र होता है। यह प्रमाणों के आकार को बाधित करता है, संगति परिणाम देता है, और, प्रमाण-के-रूप-में-कार्यक्रम पत्राचार के माध्यम से, एक कार्यक्रम को एक मान में मूल्यांकन करने के अनुरूप होता है।