अनुक्रमिक गणना: Difference between revisions

Latest revision as of 16:56, 12 June 2023

गणितीय तर्क में अनुक्रमिक कलन औपचारिक तार्किक तर्क की एक शैली है। जिसमें औपचारिक प्रमाण की प्रत्येक पंक्ति एक अप्रतिबन्ध पुनरुक्ति के अतिरिक्त एक नियमबद्ध पुनरुक्ति (तर्क) (गेरहार्ड जेंटजन के अनुसार अनुक्रम कहा जाता है) है। नियमों और अनुमान की प्रक्रियाओं के अनुसार औपचारिक तर्क में पूर्व की पंक्तियों पर अन्य नियमबद्ध पुनरुक्ति से प्रत्येक नियमबद्ध पुनरुक्ति का अनुमान लगाया जाता है जो गणितज्ञों के अनुसार डेविड हिल्बर्ट की तुलना में निगमन की प्राकृतिक शैली के लिए एक श्रेष्ठतर सन्निकटन देता है। डेविड हिल्बर्ट की औपचारिक तर्क की पूर्व की शैली जिसमें प्रत्येक पंक्ति एक नियमबद्ध पुनरुक्ति थी। जिसमे अधिक सूक्ष्म मुख्यता उपस्थित हो सकते हैं। उदाहरण के रूप मे प्रस्ताव अंतर्निहित रूप से अतार्किक सिद्धांतों पर निर्भर हो सकते हैं। उस स्थितियों में अनुक्रम पूर्व क्रम के तर्क में नियमबद्ध प्रमेय को प्रकट करते हैं | नियमबद्ध पुनरुक्ति के अतिरिक्त प्रथम-क्रम की भाषा है।

पंक्ति-दर-पंक्ति तार्किक तर्कों को व्यक्त करने के लिए अनुक्रम कलन, प्रमाण कलन की अनेक वर्तमान शैलियों में से एक है।

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

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

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

अवलोकन

प्रमाण सिद्धांत और गणितीय तर्क में अनुक्रमिक कलन औपचारिक प्रणालियों का एक संतति है जो अनुमान की निश्चित शैली और कुछ औपचारिक गुणों को साझा करता है। प्रथम अनुक्रमिक गणना प्रणाली LK और LJ 1934/1935 में गेरहार्ड जेंटजन के अनुसार प्रस्तुत की गई थी।^[1] प्रथम-क्रम तर्क (क्रमशः मौलिक तर्क और अंतर्ज्ञानवादी तर्क संस्करणों में) में प्राकृतिक निगमन का अध्ययन करने के लिए उपकरण के रूप में थी। LK और LJ के संबंध में जेंटजन का तथाकथित मुख्य प्रमेय (हॉपट॒सत्ज़) परिवर्तन -उन्मूलन प्रमेय था।^[2]^[3] दूरगामी मेटा-सैद्धांतिक परिणामों के साथ संगति संयुक्त एक परिणाम है। जेंटजन ने कुछ साल उपरांत इस प्रविधि की शक्ति और लचीलेपन का प्रदर्शन किया। गोडेल के अपूर्णता प्रमेय के आश्चर्यजनक उत्तर में (परिमित) जेंटजेन की स्थिरता प्रमाण देने के लिए एक परिवर्तन -उन्मूलन तर्क प्रयुक्त किया। इस प्रारंभिक कार्य के उपरांत से अनुक्रमिक गणना, जिसे जेंटजेन प्रणाली भी कहा जाता है,^[4]^[5]^[6]^[7] और उनसे संबंधित सामान्य अवधारणाओं को प्रमाण सिद्धांत गणितीय तर्क और स्वचालित निगमन के क्षेत्र में व्यापक रूप से प्रयुक्त किया गया है।

हिल्बर्ट-शैली निगमन प्रणाली

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

B

$B$ प्रथम-क्रम तर्क ( अथवा जो भी तर्क निगमन प्रणाली पर प्रयुक्त होता है। उदाहरण के रूप मे प्रस्तावपरक कलन अथवा उच्च-क्रम तर्क अथवा एक प्रतिरूप तर्क) का कोई भी सुव्यवस्थित सूत्र है। प्रमेय वह सूत्र हैं जो एक वैध प्रमाण में अंतिम निर्णय के रूप में प्रकट होते हैं। हिल्बर्ट-शैली प्रणाली को सूत्रों और निर्णयों के बीच कोई अंतर करने की आवश्यकता नहीं है। हम यहां मात्र उपरांत के स्थितियों की तुलना के लिए बनाते हैं।

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

प्राकृतिक निगमन प्रणाली

प्राकृतिक निगमन में निर्णयों का आकार होता है।

A_{1},A_{2},\ldots ,A_{n}\vdash B

जिस स्थान पर $A_{i}$ और $B$ पुनः सूत्र हैं, और $n\geq 0$ . के क्रमपरिवर्तन $A_{i}$ सारहीन हैं। दूसरे शब्दों में निर्णय में टर्नस्टाइल (प्रतीक) $\vdash$ के बाएं ओर सूत्रों की सूची (संभवतः रिक्त ) होती है, जिसमे दाईं ओर सूत्र होता है।^[8]^[9]^[10] प्रमेय वह सूत्र $B$ हैं जैसे कि $\vdash B$ ( रिक्त बायीं ओर) वैध प्रमाण का निष्कर्ष है। (प्राकृतिक निगमन की कुछ प्रस्तुतियों में $A_{i}$ s और टर्नस्टाइल स्पष्ट रूप से नहीं लिखा गया है। इसके अतरिक्त द्वि-आयामी संकेतन का उपयोग किया जाता है, जिससे उनका अनुमान लगाया जा सकता है।)

प्राकृतिक निगमन में निर्णय का मानक शब्दार्थ यह है कि यह अनुरोध करता है कि जब भी^[11] $A_{1}$ , $A_{2}$ आदि सब सत्य हैं तो $B$ भी सत्य होगा। निर्णय

A_{1},\ldots ,A_{n}\vdash B

और

\vdash (A_{1}\land \cdots \land A_{n})\rightarrow B

दृढ़ अर्थों में समतुल्य हैं, कि किसी एक के प्रमाण को दूसरे के प्रमाण तक बढ़ाया जा सकता है।

अनुक्रमिक कैलकुलस सिस्टम

अंत में अनुक्रमिक कैलकुलस प्राकृतिक निगमन निर्णय के रूप को सामान्यीकृत करता है

A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k},

एक वाक्यात्मक प्रदर्शन जिसे अनुक्रम कहा जाता है। टर्नस्टाइल (प्रतीक) के बायीं ओर के सूत्रों को पूर्ववर्ती कहा जाता है, और दायीं ओर के सूत्रों को क्रमिक अथवा परिणामी कहा जाता है। साथ में उन्हें विनम्र अथवा अनुक्रम कहा जाता है।^[12] पुनः , $A_{i}$ और $B_{i}$ सूत्र हैं, और $n$ और $k$ अनकारात्मक पूर्णांक हैं, अर्थात बाएँ ओर अथवा दाईं ओर ( अथवा दोनों में से कोई भी) रिक्त हो सकता है। प्राकृतिक निगमन के रूप में प्रमेय वह हैं $B$ जहाँ $\vdash B$ वैध प्रमाण का निष्कर्ष है।

एक अनुक्रम का मानक शब्दार्थ एक अनुरोध है कि जब भी प्रत्येक $A_{i}$ सत्य है एवं कम से कम एक $B_{i}$ भी सत्य होगा।^[13] इस प्रकार रिक्त अनुक्रम अवास्तविक है, जिसमें दोनों विनम्र रिक्त हैं।^[14] इसे व्यक्त करने का विधि यह है कि, टर्नस्टाइल को बाएं ओर के अल्पविराम को और के रूप में उल्लिखित होना चाहिए, और टर्नस्टाइल दाईं ओर के अल्पविराम को (सम्मिलित) अथवा के रूप में माना उल्लिखित होना चाहिए। अनुक्रम

A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k}

और

\vdash (A_{1}\land \cdots \land A_{n})\rightarrow (B_{1}\lor \cdots \lor B_{k})

दृढ़ अर्थों में समतुल्य हैं कि किसी भी क्रम के प्रमाण को दूसरे अनुक्रम के प्रमाण तक बढ़ाया जा सकता है।

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

\vdash \neg A_{1}\lor \neg A_{2}\lor \cdots \lor \neg A_{n}\lor B_{1}\lor B_{2}\lor \cdots \lor B_{k}

(कम से कम एक As असत्य है, अथवा Bs में से एक सत्य है)

अथवा रूप में

\vdash \neg (A_{1}\land A_{2}\land \cdots \land A_{n}\land \neg B_{1}\land \neg B_{2}\land \cdots \land \neg B_{k})

(ऐसा नहीं हो सकता कि समस्त As सत्य हैं और समस्त Bs असत्य हैं)।

इन परिणाम में टर्नस्टाइल दोनों ओर के सूत्रों के बीच एकमात्र अंतर यह है कि एक पक्ष को अस्वीकार करा गया है। इस प्रकार एक क्रम में बाएं से दाएं की परिवर्तन समस्त घटक सूत्रों को अस्वीकार के अनुरूप है। इसका अर्थ यह है कि समरूपता जैसे डी मॉर्गन के नियम जो अर्थ स्तर पर खुद को तार्किक निषेध के रूप में प्रकट करते हैं, अनुक्रमों के बाएं-दाएं समरूपता में प्रत्यक्ष अनुवाद करते हैं और वास्तव में संयोजन (∧) से व्यवहार के लिए अनुक्रमिक कलन में निष्कर्ष नियम संयोजन (∨) से व्यवहार वालों की दर्पण छवियां है।

अनेक तर्कशास्त्री अनुभव करते हैं कि यह सममित प्रस्तुति प्रमाण प्रणाली की अन्य शैलियों की तुलना में तर्क की संरचना में गहन अंतर्दृष्टि प्रदान करती है जिस स्थान पर नियमों में नकारात्मकता का मौलिक द्वंद्व उतना स्पष्ट नहीं है।

प्राकृतिक निगमन और अनुक्रमिक कलन के बीच का अंतर

जेंटजन ने अपने एकल उत्पादन प्राकृतिक निगमन प्रणाली (NK और NJ) और उनके बहु- उत्पादन अनुक्रम कैलकुलस प्रणाली (LK और LJ) के बीच एक त्वरित्र अंतर पर बल दिया। उन्होंने लिखा है कि अंतर्ज्ञानवादी प्राकृतिक निगमन प्रणाली NJ कुछ कुरूप थी।^[15] उन्होंने कहा कि मौलिक प्राकृतिक निगमन प्रणाली NK में बहिष्कृत मध्य के नियम की विशेष भूमिका को मौलिक अनुक्रम कैलकुलस प्रणाली LK में पदच्युत दिया गया है।^[16] उन्होंने कहा कि अनुक्रमिक कलन LJ ने अंतर्ज्ञानवादी तर्क के स्थितियों में प्राकृतिक निगमन NJ की तुलना में अधिक समरूपता प्रदान की, और साथ ही मौलिक तर्क (LK विरुद्ध NK) के स्थितियों में भी प्राप्त की है।^[17] तब उन्होंने कहा कि इन कारणों के अतिरिक्त अनेक उत्तरवर्ती सूत्रों के साथ अनुक्रमिक कलन विशेष रूप से उनके प्रमुख प्रमेय (हॉपत्सत्ज़) के लिए अभिप्रेत है।^[18]

अनुक्रम शब्द की उत्पत्ति

अनुक्रम शब्द जेंटजन के 1934 के लेख्य में अनुक्रम शब्द से लिया गया है।^[1]स्टीफन कोल क्लेन अंग्रेजी में अनुवाद पर निम्नलिखित टिप्पणी करते हैं। जेंटजन ' अनुक्रम ' कहते हैं, जिसे हम 'अनुक्रम' के रूप में अनुवादित करते हैं क्योंकि हम ने पूर्व से ही वस्तुओं के अनुक्रम के लिए 'अनुक्रम' का उपयोग कर लिया हैं, जिस स्थान पर जर्मन 'फोल्गे' है।^[19]

तार्किक सूत्र प्रमाणन

अनुक्रमिक कलन के अनुसार एक प्रमाण प्रकट करने की प्रक्रिया का वर्णन करने वाला एक मूल वाला ट्री

रिडक्शन ट्री

अनुक्रमिक कलन को विश्लेषणात्मक दृश्य की विधि के समान प्रस्तावपरक तर्क में सूत्र सिद्ध करने के लिए उपकरण के रूप में देखा जा सकता है। यह चरणों की एक श्रृंखला देता है जो तार्किक सूत्र को सरल और सरल सूत्रों को प्रमाणन करने की उपपाद्य विषय को कम करने की अनुमति देता है जब तक कि कोई साधारण नहीं हो जाता।^[20] निम्नलिखित सूत्र पर विचार करें-

((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)

यह निम्नलिखित रूप में लिखा गया है, जिस स्थान पर सिद्ध करने की आवश्यकता वाले प्रस्ताव टर्नस्टाइल (प्रतीक) के दाईं ओर है $\vdash$ :

\vdash ((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)

अब इसे स्वयंसिद्धों से सिद्ध करने के अतिरिक्त तार्किक परिणाम के आधार को मान लेना और तब उसके निष्कर्ष को सिद्ध करने का प्रयास करना पर्याप्त है।^[21] इसलिए निम्नलिखित अनुक्रम में जाता है-

(p\rightarrow r)\lor (q\rightarrow r)\vdash (p\land q)\rightarrow r

पुनः दाहिने हाथ की ओर निहितार्थ सम्मिलित है जिसका आधार आगे माना जा सकता है जिससे मात्र इसके निष्कर्ष को सिद्ध करने की आवश्यकता हो-

(p\rightarrow r)\lor (q\rightarrow r),(p\land q)\vdash r

चूँकि बाएं ओर के तर्कों को तार्किक संयोजन के अनुसार संबंधित माना जाता है, इसे निम्नलिखित के अनुसार प्रतिस्थापित किया जा सकता है-

(p\rightarrow r)\lor (q\rightarrow r),p,q\vdash r

यह बाएं ओर के पूर्व तर्क पर संयोजन के दोनों स्थितियों में निष्कर्ष सिद्ध करने के बराबर है। इस प्रकार हम अनुक्रम को दो में विभाजित कर सकते हैं, जहाँ अब हमें प्रत्येक को प्रथक- प्रथक सिद्ध करना होगा-

p\rightarrow r,p,q\vdash r

q\rightarrow r,p,q\vdash r

पूर्व फैसले के स्थितियों में हम पुनः लिखते हैं $p\rightarrow r$ जैसा $\lnot p\lor r$ और अनुक्रम को पुनः विभाजित करके प्राप्त करें-

\lnot p,p,q\vdash r

r,p,q\vdash r

द्वितीय क्रम किया जाता है; पूर्व अनुक्रम को और सरल बनाया जा सकता है-

p,q\vdash p,r

इस प्रक्रिया को सदैव तब तक प्रचलित रखा जा सकता है जब तक कि प्रत्येक पक्ष में मात्र आणविक सूत्र न हों। इस प्रक्रिया को रेखांकन के रूप में ट्री ( रेखाचित्र सिद्धांत) के अनुसार वर्णित किया जा सकता है, जैसा कि दाईं ओर दर्शाया गया है। ट्री की मूल वह सूत्र है, जिसे हम सिद्ध करना चाहते हैं। पत्तियों में मात्र आणविक सूत्र होते हैं। ट्री को आभाव ट्री के रूप में उल्लिखित किया जाता है। ^[20]^[22] टर्नस्टाइल बायीं ओर की वस्तुओं को संयुग्मन के अनुसार जुड़ा हुआ समझा जाता है, और जो दायीं ओर विच्छेद के अनुसार जुड़ा हुआ है। इसलिए जब दोनों में मात्र आणविक प्रतीक होते हैं, तो अनुक्रम को स्वैच्छिक रूप से (और सदैव सत्य) स्वीकार किया जाता है यदि और मात्र दाईं ओर कम से कम एक प्रतीक भी बाएं ओर प्रदर्शित होता है।

निम्नलिखित नियम हैं, जिनके के अनुसार कोई एक ट्री के साथ आगे बढ़ता है। जब भी एक अनुक्रम को दो में विभाजित किया जाता है, ट्री वर्टेक्स में दो चाइल्ड वर्टिकल होते हैं, और ट्री शाखित होता है। इसके अतिरिक्त प्रत्येक पक्ष में तर्कों के क्रम को स्वतंत्र रूप से बदला जा सकता है। Γ और Δ संभावित अतिरिक्त तर्कों के लिए खंड हैं।^[20]

प्राकृतिक निगमन के लिए जेंटजन-शैली के विन्यास में उपयोग की जाने वाली क्षैतिज रेखा के लिए सामान्य शब्द अनुमान रेखा है। ^[23]

Left:	Right:
$L\land {\text{rule: }}\quad {\cfrac {\Gamma ,A\land B\vdash \Delta }{\Gamma ,A,B\vdash \Delta }}$	$R\land {\text{rule: }}{\cfrac {\Gamma \vdash \Delta ,A\land B}{\Gamma \vdash \Delta ,A\qquad \Gamma \vdash \Delta ,B}}$
$L\lor {\text{rule: }}{\cfrac {\Gamma ,A\lor B\vdash \Delta }{\Gamma ,A\vdash \Delta \qquad \Gamma ,B\vdash \Delta }}$	$R\lor {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,A\lor B}{\Gamma \vdash \Delta ,A,B}}$
$L\rightarrow {\text{rule: }}{\cfrac {\Gamma ,A\rightarrow B\vdash \Delta }{\Gamma \vdash \Delta ,A\qquad \Gamma ,B\vdash \Delta }}$	$R\rightarrow {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,A\rightarrow B}{\Gamma ,A\vdash \Delta ,B}}$
$L\lnot {\text{rule: }}\quad {\cfrac {\Gamma ,\lnot A\vdash \Delta }{\Gamma \vdash \Delta ,A}}$	$R\lnot {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,\lnot A}{\Gamma ,A\vdash \Delta }}$
Axiom:
$\Gamma ,A\vdash \Delta ,A$

वक्‍तव्‍य कथन तर्क में किसी भी सूत्र से प्रारंभ करके चरणों की श्रृंखला के अनुसार टर्नस्टाइल दाईं ओर संसाधित किया जा सकता है। जब तक कि इसमें मात्र आणविक प्रतीक सम्मिलित न हों। तब बाएं ओर के लिए भी ऐसा ही किया जाता है। चूँकि प्रत्येक तार्किक संकारक ऊपर दिए गए नियमों में से एक में प्रकट होता है और नियम के अनुसार पदच्युत दिया जाता है। जब कोई तार्किक संकारक नहीं रह जाता है तो प्रक्रिया समाप्त हो जाती है। अब सूत्र विघटित हो गया है।

इस प्रकार वृक्षों की पत्तियों में अनुक्रमों में मात्र आणविक प्रतीक सम्मिलित होते हैं जो स्वयंसिद्ध के अनुसार सिद्ध होते हैं अथवा नहीं। इसके अनुसार दाईं ओर के प्रतीकों में से एक बाएं ओर भी प्रदर्शित देता है।

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

मानक स्वयंसिद्धीकरणों से संबंध

अनुक्रम कैलकुलस वक्‍तव्‍य कथन कैलकुलस के अन्य स्वयंसिद्धों से संबंधित है जैसे कि स्थिर का प्रस्ताव कैलकुलस अथवा जान लुकासिविक्ज़ का स्वयंसिद्धीकरण (स्वयं मानक हिल्बर्ट प्रणाली का एक खंड ) है। प्रत्येक सूत्र जो इनमें सिद्ध किया जा सकता है में पराभव का ट्री है।

इसे निम्न प्रकार से दिखाया जा सकता है। तर्कवाक्य कलन में प्रत्येक उपपत्ति मात्र अभिगृहीतों और अनुमान नियमों का उपयोग करती है। स्वयंसिद्ध योजना का प्रत्येक उपयोग वास्तविक तार्किक सूत्र उत्पन्न करता है, और इस प्रकार अनुक्रमिक कलन में सिद्ध किया जा सकता है। इनके लिए उदाहरण अनुक्रमिक कैलकुलस व्युत्पन्न हैं। ऊपर वर्णित प्रणालियों में एकमात्र निष्कर्ष नियम विधानात्मक हेतु फलानुमान है। जिसे परिवर्तन नियम के अनुसार कार्यान्वित किया जाता है।

प्रणाली LK

यह खंड 1934 में जेंटजेन के अनुसार प्रस्तुत किए गए अनुक्रमिक कैलकुलस LK ( तार्किक कल्कुल स्थिति) के नियमों का परिचय देता है। ^[24] इस कैलकुलस में (औपचारिक) प्रमाण अनुक्रमों का क्रम है। जिस स्थान पर अनुक्रम में से प्रत्येक नीचे दिए गए अनुमान के नियम का उपयोग करके अनुक्रम में पूर्व प्रदर्शित अनुक्रमों से व्युत्पन्न होता है।

अनुमान नियम

निम्नलिखित टिप्पणी का उपयोग किया जाएगा-

$\vdash$ टर्नस्टाइल (प्रतीक) के रूप में उल्लिखित किया जाता है, और बाएं ओर की मान्यताओं को दाईं ओर के प्रस्तावों से प्रथक करता है।
$A$ और $B$ प्रथम-क्रम विधेय तर्क के सूत्रों को निरूपित करता है(कोई इसे प्रस्तावपरक तर्क तक सीमित भी कर सकता है)।
$\Gamma ,\Delta ,\Sigma$ $\Gamma ,\Delta ,\Sigma$ , और $\Pi$ $\Pi$ सूत्रों के परिमित (संभवतः रिक्त ) अनुक्रम हैं (वास्तव में सूत्रों का क्रम प्रयोजन नहीं रखता; देखें § संरचनात्मक नियम)। जिन्हें संदर्भ कहा जाता है।
- जब बाएं ओर $\vdash$ सूत्रों के अनुक्रम को संयोजन के रूप में माना जाता है ( समस्त को एक ही समय धारण करने के लिए माना जाता है)।
- यद्यपि दाईं ओर $\vdash$ सूत्रों के अनुक्रम को वियोगात्मक रूप से माना जाता है (चर के किसी भी कार्य के लिए कम से कम एक सूत्र को धारण करना चाहिए)।
$t$ इच्छानुसार अवधि प्रकट करता है।
$x$ और $y$ चरों को निरूपित करता है।
चर को एक सूत्र के अंतर्गत मुक्त होने के लिए कहा जाता है यदि यह परिमाणकों के अनुसार बाध्य नहीं है । $\forall$ अथवा $\exists$ अस्तित्व में है।
$A[t/x]$ उस सूत्र को प्रकट करता है, जो सूत्र $A$ में चर $x$ की प्रत्येक मुक्त घटना के लिए शब्द $t$ को प्रतिस्थापित करके प्राप्त किया जाता है, सूत्र में $A$ इस प्रतिबंध के साथ कि शब्द $t$ को $A$ मे चर $x$ के लिए मुक्त होना चाहिए ( अर्थात किसी भी चर की कोई घटना नहीं है) $t$ में कोई भी चर $A[t/x]$ ) में बाध्य हो जाता है।
$WL$ , $WR$ , $CL$ , $CR$ , $PL$ , $PR$ ये छह तीन संरचनात्मक नियमों में से प्रत्येक के दो संस्करणों के लिए खड़े हैं। एक a $\vdash$ के बाएं ओर ('L') उपयोग के लिए और द्वितीय इसके दाईं ओर ('R') है। नियमों को अशक्त करने के लिए 'W' (बाएं / दाएं), संकुचन के लिए 'C' और क्रमचय के लिए 'P' संक्षिप्त किया गया है।

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

स्वयंसिद्ध	आभाव
${\cfrac {\qquad }{A\vdash A}}\quad (I)$	${\cfrac {\Gamma \vdash \Delta ,A\qquad A,\Sigma \vdash \Pi }{\Gamma ,\Sigma \vdash \Delta ,\Pi }}\quad ({\mathit {Cut}})$
बाएं तार्किक नियम	दाएं तार्किक नियम
${\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{1})$	${\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{1})$
${\cfrac {\Gamma ,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{2})$	${\cfrac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{2})$
${\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\lor B\vdash \Delta ,\Pi }}\quad ({\lor }L)$	${\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma \vdash B,\Pi }{\Gamma ,\Sigma \vdash A\land B,\Delta ,\Pi }}\quad ({\land }R)$
${\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\rightarrow B\vdash \Delta ,\Pi }}\quad ({\rightarrow }L)$	${\cfrac {\Gamma ,A\vdash B,\Delta }{\Gamma \vdash A\rightarrow B,\Delta }}\quad ({\rightarrow }R)$
${\cfrac {\Gamma \vdash A,\Delta }{\Gamma ,\lnot A\vdash \Delta }}\quad ({\lnot }L)$	${\cfrac {\Gamma ,A\vdash \Delta }{\Gamma \vdash \lnot A,\Delta }}\quad ({\lnot }R)$
${\cfrac {\Gamma ,A[t/x]\vdash \Delta }{\Gamma ,\forall xA\vdash \Delta }}\quad ({\forall }L)$	${\cfrac {\Gamma \vdash A[y/x],\Delta }{\Gamma \vdash \forall xA,\Delta }}\quad ({\forall }R)$
${\cfrac {\Gamma ,A[y/x]\vdash \Delta }{\Gamma ,\exists xA\vdash \Delta }}\quad ({\exists }L)$	${\cfrac {\Gamma \vdash A[t/x],\Delta }{\Gamma \vdash \exists xA,\Delta }}\quad ({\exists }R)$
बाएं संरचनात्मक नियम	दाएं संरचनात्मक नियम
${\cfrac {\Gamma \vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {WL}})$	${\cfrac {\Gamma \vdash \Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {WR}})$
${\cfrac {\Gamma ,A,A\vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {CL}})$	${\cfrac {\Gamma \vdash A,A,\Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {CR}})$
${\cfrac {\Gamma _{1},A,B,\Gamma _{2}\vdash \Delta }{\Gamma _{1},B,A,\Gamma _{2}\vdash \Delta }}\quad ({\mathit {PL}})$	${\cfrac {\Gamma \vdash \Delta _{1},A,B,\Delta _{2}}{\Gamma \vdash \Delta _{1},B,A,\Delta _{2}}}\quad ({\mathit {PR}})$

प्रतिबंध: नियमों में $({\forall }R)$ और $({\exists }L)$ मे परिवर्तनीय $y$ संबंधित निम्नतर अनुक्रमों में कहीं भी मुक्त नहीं होना चाहिए।

एक सहज व्याख्या

उपरोक्त नियमों को दो प्रमुख समूहों तार्किक और संरचनात्मक में विभाजित किया जा सकता है। प्रत्येक तार्किक नियम टर्नस्टाइल (प्रतीक) के बाएं ओर अथवा दाईं ओर एक नया तार्किक $\vdash$ सूत्र प्रस्तुत करता है। इसके विपरीत संरचनात्मक नियम सूत्रों के त्रुटिहीन आकार की अनदेखी करते हुए अनुक्रमों की संरचना पर काम करते हैं। इस सामान्य योजना के दो अपवाद समानता के स्वयंसिद्ध (I) और ( परिवर्तन ) के नियम हैं।

चूंकि औपचारिक विधियों से कहा गया है कि उपरोक्त नियम मौलिक तर्क के संदर्भ में अति सहज ज्ञान युक्त अध्ययन की अनुमति देते हैं। उदाहरण के रूप मे नियम $({\land }L_{1})$ पर विचार करें । यह नियम कहता है कि, कोई इसे प्रमाणन कर सकता है और $\Delta$ सूत्रों के कुछ अनुक्रम से निष्कर्ष निकाला जा सकता है इसमे सम्मिलित $A$ , है तो कोई भी $\Delta$ (दृढ़) निष्कर्ष निकाल सकता है। जो $A\land B$ धारण करता है। इसी प्रकार नियम $({\neg }R)$ बताता है कि, $\Gamma$ और $A$ $\Delta$ को समाप्त करने के लिए पर्याप्त हैं, तो $\Gamma$ अकेले से या तो अभी भी $\Delta$ से निष्कर्ष निकाल सकता है अथवा $A$ अवास्तविक होना चाहिए, अर्थात ${\neg }A$ अधिकार रखता है। समस्त नियमों की व्याख्या इस प्रकार की जा सकती है।

परिमाणकों नियमों के संबंध में अंतर्ज्ञान के लिए नियम $({\forall }R)$ पर विचार करें । निस्संदेह यह निष्कर्ष निकाला $\forall {x}A$ मात्र इस तथ्य से अधिकार रखता है कि $A[y/x]$ सत्य है किन्तु यह सामान्य रूप पर संभव नहीं है। चूंकि चर y का कहीं और उल्लेख नहीं किया गया है (अर्थात इसे अभी भी अन्य सूत्रों को प्रभावित किए नियमबद्ध स्वतंत्र रूप से चयनित जा सकता है), तो कोई यह मान सकता है कि $A[y/x]$ y के किसी भी मान के लिए है। अन्य नियम तब अति प्रत्यक्ष होने चाहिए।

नियमों को विधेय तर्क में नियमबद्ध व्युत्पत्तियों के विवरण के रूप में देखने के अतिरिक्त उन्हें किसी दिए गए कथन प्रमाण के निर्माण निर्देश के रूप में भी माना जा सकता है। इस स्थितियों में नियमों को नीचे से ऊपर तक अध्ययन जा सकता है। उदाहरण के रूप मे $({\land }R)$ के द्वारा इसे प्रमाणन करने के लिए $A\land B$ धारणाओं $\Gamma$ और $\Sigma$ से अनुसरण करता है, यह प्रमाणन करने के लिए पर्याप्त है कि $A$ और $\Gamma$ से निष्कर्ष निकाला जा सकता है, और $B$ को क्रमश $\Sigma$ से निष्कर्ष निकाला जा सकता है। ध्यान दें कि कुछ पूर्ववृत्त दिए जाने पर यह स्पष्ट नहीं है कि इसे $\Gamma$ और $\Sigma$ कैसे विभाजित किया जाए। चूंकि मात्र अति संभावनाएँ निस्र्द्ध जा सकती हैं, क्योंकि धारणा के अनुसार पूर्ववर्ती परिमित है। यह यह भी प्रकट करता है कि कैसे प्रमाण सिद्धांत को मिश्रित प्रचलन में प्रमाण के रूप में देखा जा सकता है। $A$ और $B$ दोनों के लिए प्रमाण दिए गए है, कोई भी $A\land B$ के लिए प्रमाण बना सकता है।

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

द्वितीय नियम जो कुछ विशेष है वह समानता का स्वयंसिद्ध (I) है। इसका सहज ज्ञान स्पष्ट है। प्रत्येक सूत्र स्वयं को सिद्ध करता है। परिवर्तन नियम की प्रकार, समानता का स्वयंसिद्ध कुछ स्तर तक निरर्थक है। आणविक प्रारंभिक अनुक्रमों की पूर्णता वर्णन करती है कि नियम को किसी भी हानि के नियमबद्ध आणविक सूत्र तकों सीमित किया जा सकता है।

ध्यान दें कि निहितार्थ के नियमों को छोड़कर समस्त नियमों में दर्पण साथी होते हैं। यह इस तथ्य को प्रकट करता है कि, प्रथम-क्रम तर्क की सामान्य भाषा में संयोजक के अनुसार निहित नहीं है अथवा सम्मिलित नहीं है। संयोजी $\not \leftarrow$ जो निहितार्थ का डी मॉर्गन द्विवचन होगा। इस प्रकार के संयोजन को अपने प्राकृतिक नियमों के साथ संयोजन से कलन पूर्ण प्रकार से बाएँ-दाएँ सममित हो जाएगा।

उदाहरण व्युत्पत्ति

यहाँ $\vdash A\lor \lnot A$ की व्युत्पत्ति है। जिसे अपवर्जित मध्य का नियम के रूप मे विदित है (लैटिन में टर्शियम नॉन डाटूर)।

		$(I)$
$A\vdash A$
		$(\lnot R)$
$\vdash \lnot A,A$
		$(\lor R_{2})$
$\vdash A\lor \lnot A,A$
		$(PR)$
$\vdash A,A\lor \lnot A$
		$(\lor R_{1})$
$\vdash A\lor \lnot A,A\lor \lnot A$
		$(CR)$
$\vdash A\lor \lnot A$

आगामी एक साधारण तथ्य का प्रमाण है जिसमें परिमाणकों सम्मिलित हैं। ध्यान दें कि आक्षेप सत्य नहीं है, और इसकी असत्यता को नीचे-ऊपर व्युत्पन्न करने का प्रयास करते समय देखा जा सकता है। क्योंकि नियमों $(\forall R)$ और $(\exists L)$ में प्रतिस्थापन में वर्तमान मुक्त चर का उपयोग नहीं किया जा सकता है।

		$(I)$
$p(x,y)\vdash p(x,y)$
		$(\forall L)$
$\forall x\left(p(x,y)\right)\vdash p(x,y)$
		$(\exists R)$
$\forall x\left(p(x,y)\right)\vdash \exists y\left(p(x,y)\right)$
		$(\exists L)$
$\exists y\left(\forall x\left(p(x,y)\right)\right)\vdash \exists y\left(p(x,y)\right)$
		$(\forall R)$
$\exists y\left(\forall x\left(p(x,y)\right)\right)\vdash \forall x\left(\exists y\left(p(x,y)\right)\right)$

कुछ और रोचक के लिए हम ${\left(\left(A\rightarrow \left(B\lor C\right)\right)\rightarrow \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)\right)}$ प्रमाणन करेंगे। व्युत्पत्ति का ज्ञात करना प्रत्यक्ष है, जो स्वचालित प्रमाणन करने में LK की सार्थकता को प्रकट करता है।

		$(I)$
$A\vdash A$
		$(\lnot R)$
$\vdash \lnot A,A$
		$(PR)$
$\vdash A,\lnot A$

			$(I)$
$B\vdash B$			$(I)$
$B\vdash B$

			$(I)$
$C\vdash C$			$(I)$
$C\vdash C$

(\lor L)

B\lor C\vdash B,C

(PR)

B\lor C\vdash C,B

(\lnot L)

B\lor C,\lnot C\vdash B

संरेखित = केंद्र सीमा = 0 सेलस्पेसिंग = 0 सेलपैडिंग = 0

(I)

\lnot A\vdash \lnot A

(\rightarrow L)

\left(B\lor C\right),\lnot C,\left(B\rightarrow \lnot A\right)\vdash \lnot A

(\land L_{1})

\left(B\lor C\right),\lnot C,\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A

(PL)

\left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\lnot C\vdash \lnot A

(\land L_{2})

\left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A

(CL)

\left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A

(PL)

\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(B\lor C\right)\vdash \lnot A

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

विश्लेषणात्मक चित्र से संबंध

अनुक्रमिक कैलकुलस के कुछ सूत्रीकरण (अर्थात रूपांतर) के लिए इस प्रकार के कैलकुलस में निम्म प्रमाण, संवृत विश्लेषणात्मक उत्क्रम विधि के लिए समरूप है।^[25]

संरचनात्मक नियम

संरचनात्मक नियम कुछ अतिरिक्त परिचर्चा के पात्र हैं।

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

संकुचन (C) और क्रमचय (P) आश्वस्त करते हैं कि, अनुक्रम के तत्वों के न तो आदेश (P) और न ही घटनाओं की बहुलता (C) प्रयोजन रखती है। इस प्रकार अनुक्रमों के अतिरिक्त समुच्चय (गणित) पर भी विचार किया जा सकता है।

चूंकि अनुक्रमों का उपयोग करने का अतिरिक्त प्रयास उचित है क्योंकि खंड अथवा समस्त संरचनात्मक नियमों को त्यागा जा सकता है। ऐसा करने से तथाकथित अवसंरचनात्मक तर्क प्राप्त होता है।

प्रणाली LK के गुण

नियमों की इस प्रणाली को प्रथम-क्रम तर्क के संबंध में सुदृढ़ता और पूर्णता (तर्क) दोनों के रूप में दिखाया जा सकता है, अर्थात कथन $A$ परिसर के एक समुच्चय से शब्दार्थ का अनुसरण करता है। $\Gamma$ $(\Gamma \vDash A)$ यदि और मात्र अनुक्रम $\Gamma \vdash A$ उपरोक्त नियमों के अनुसार प्राप्त किया जा सकता है।^[26] अनुक्रमिक कलन में परिवर्तन -उन्मूलन का नियमस्वीकार्य है। इस परिणाम को जेंटजन हॉपट॒सत्ज़ (मुख्य प्रमेय) के रूप में भी उल्लिखित है।^[2]^[3]

रूपांतर

उपरोक्त नियमों को विभिन्न विधियों से संशोधित किया जा सकता है:

लघु संरचनात्मक विकल्प

अनुक्रमों और संरचनात्मक नियमों को कैसे औपचारिक रूप दिया जाता है, इसके तकनीकी विवरण के संबंध में विकल्प की स्वतंत्रता है। जब तक LK में प्रत्येक व्युत्पत्ति प्रभावी रूप से नए नियमों का उपयोग करके व्युत्पत्ति में परिवर्तित हो सकती है, और इसके विपरीत संशोधित नियमों को अभी भी LK कहा जा सकता है।

सबसे पूर्व जैसा कि ऊपर उल्लेख किया गया है, अनुक्रमों को समुच्चय अथवा बहु- समुच्चय से संमिश्रित देखा जा सकता है। इस स्थितियों में अनुमत करने के नियम और (समुच्चय का उपयोग करते समय) अनुबंध सूत्र अप्रचलित हैं।

अशक्त नियम स्वीकार्य हो जाएगा, जब स्वयंसिद्ध (I) को प्रवर्तित दिया जाता है। जैसे कि $\Gamma ,A\vdash A,\Delta$ रूप का अनुक्रम निष्कर्ष निकाला जा सकता है। इस का अर्थ है कि $A$ सिद्ध होता है। किसी भी संदर्भ में $A$ व्युत्पत्ति में प्रदर्शित देने वाली कोई भी निर्बलता प्रारंभ में ही सही की जा सकती है। प्रमाण को नीचे से ऊपर बनाते समय यह एक सुविधाजनक परिवर्तन हो सकता है।

इनमें से स्वतंत्र नियमों के अंतर्गत संदर्भों को विभाजित करने के विधियों को प्रवर्तित सकता है। स्थितियों में $({\land }R),({\lor }L)$ , और $({\rightarrow }L)$ वाम संदर्भ किस $\Gamma$ और $\Sigma$ मे विभाजित होता है। चूंकि संकुचन इनके दोहराव की अनुमति देता है, कोई यह मान सकता है, कि व्युत्पत्ति की दोनों शाखाओं में पूर्ण संदर्भ का उपयोग किया जाता है। ऐसा करने से यह सुनिश्चित होता है कि कोई भी महत्वपूर्ण परिसर त्रुटिपूर्ण उपखंड में लुप्त न हो जाए। संदर्भ के अप्रासंगिक खंडो को अशक्त करके उपरांत में समाप्त किया जा सकता है।

असंगति

एक स्वयंसिद्ध के साथ ⊥ असत्य का प्रतिनिधित्व करने वाले असंगति स्थिरांक को प्रस्तुत कर सकता है-

{\cfrac {}{\bot \vdash \quad }}

अथवा जैसा कि ऊपर वर्णित है, अशक्त करना स्वीकार्य नियम है, तो स्वयंसिद्ध के साथ-

{\cfrac {}{\Gamma ,\bot \vdash \Delta }}

परिभाषा $(\neg A)\iff (A\to \bot )$ के माध्यम से $\bot$ निषेध को निहितार्थ के एक विशेष स्थितियों के रूप में सम्मिलित किया जा सकता है।

अवसंरचनात्मक तर्क

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

अंतर्ज्ञानी अनुक्रम कलन: प्रणाली LJ

आश्चर्यजनक रूप से LK के नियमों में कुछ छोटे बदलाव इसे अंतर्ज्ञानवादी तर्क के लिए प्रमाण प्रणाली में बदलने के लिए पर्याप्त हैं।^[27] इसके लिए किसी को दाहिनी ओर अधिक से अधिक एक सूत्र वाले अनुक्रमों तक सीमित करना होगा, और इस अपरिवर्तनीय को बनाए रखने के लिए नियमों को संशोधित करना होगा। उदाहरण के रूप मे $({\lor }L)$ निम्नानुसार सुधार किया गया है (जहाँ C इच्छानुसार सूत्र है)।

{\cfrac {\Gamma ,A\vdash C\qquad \Sigma ,B\vdash C}{\Gamma ,\Sigma ,A\lor B\vdash C}}\quad ({\lor }L)

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

वास्तव में LK में एकमात्र नियम जिसे एकल-सूत्र परिणामों तक सीमित करने की आवश्यकता है वह हैं $({\to }R)$ $(\neg R)$ (जिसे ऊपर वर्णित { ${\to }R$ ऊपर विशेष स्थितियों के रूप में देखा जा सकता है) और $({\forall }R)$ बहु-सूत्र परिणामों को वियोजन के रूप में व्याख्यायित किया जाता है, तो LK के अन्य सभी निष्कर्ष नियम LJ में व्युत्पन्न होते हैं, जबकि नियम $({\to }R)$ और $({\forall }R)$ बन जाते हैं

{\cfrac {\Gamma ,A\vdash B\lor C}{\Gamma \vdash (A\to B)\lor C}}

और जब $y$ नीचे के क्रम में मुक्त नहीं होता है

{\cfrac {\Gamma \vdash A[y/x]\lor C}{\Gamma \vdash (\forall xA)\lor C}}.

ये नियम सहज रूप से मान्य नहीं हैं।

यह भी देखें

↑ ^1.0 ^1.1 Gentzen 1934, Gentzen 1935.
↑ ^2.0 ^2.1 Curry 1977, pp. 208–213, विलोपन प्रमेय का 5-पृष्ठ प्रमाण देता है। पेज 188, 250 भी देखें।
↑ ^3.0 ^3.1 Kleene 2009, pp. 453, कट-एलिमिनेशन प्रमेय का एक बहुत ही संक्षिप्त प्रमाण देता है।
↑ Curry 1977, pp. 189–244, calls Gentzen systems LC systems. Curry's emphasis is more on theory than on practical logic proofs.
↑ Kleene 2009, pp. 440–516. This book is much more concerned with the theoretical, metamathematical implications of Gentzen-style sequent calculus than applications to practical logic proofs.
↑ Kleene 2002, pp. 283–312, 331–361, defines Gentzen systems and proves various theorems within these systems, including Gödel's completeness theorem and Gentzen's theorem.
↑ Smullyan 1995, pp. 101–127, gives a brief theoretical presentation of Gentzen systems. He uses the tableau proof layout style.
↑ Curry 1977, pp. 184–244, compares natural deduction systems, denoted LA, and Gentzen systems, denoted LC. Curry's emphasis is more theoretical than practical.
↑ Suppes 1999, pp. 25–150, is an introductory presentation of practical natural deduction of this kind. This became the basis of System L.
↑ Lemmon 1965 is an elementary introduction to practical natural deduction based on the convenient abbreviated proof layout style System L based on Suppes 1999, pp. 25–150.
↑ Here, "whenever" is used as an informal abbreviation "for every assignment of values to the free variables in the judgment"
↑ Shankar, Natarajan; Owre, Sam; Rushby, John M.; Stringer-Calvert, David W. J. (2001-11-01). "पीवीएस प्रोवर गाइड" (PDF). User guide. SRI International. Retrieved 2015-05-29.
↑ For explanations of the disjunctive semantics for the right side of sequents, see Curry 1977, pp. 189–190, Kleene 2002, pp. 290, 297, Kleene 2009, p. 441, Hilbert & Bernays 1970, p. 385, Smullyan 1995, pp. 104–105 and Gentzen 1934, p. 180.
↑ Buss 1998, p. 10
↑ Gentzen 1934, p. 188. "Der Kalkül NJ hat manche formale Unschönheiten."
↑ Gentzen 1934, p. 191. "In dem klassischen Kalkül NK nahm der Satz vom ausgeschlossenen Dritten eine Sonderstellung unter den Schlußweisen ein [...], indem er sich der Einführungs- und Beseitigungssystematik nicht einfügte. Bei dem im folgenden anzugebenden logistischen klassichen Kalkül LK wird diese Sonderstellung aufgehoben."
↑ Gentzen 1934, p. 191. "Die damit erreichte Symmetrie erweist sich als für die klassische Logik angemessener."
↑ Gentzen 1934, p. 191. "Hiermit haben wir einige Gesichtspunkte zur Begründung der Aufstellung der folgenden Kalküle angegeben. Im wesentlichen ist ihre Form jedoch durch die Rücksicht auf den nachher zu beweisenden 'Hauptsatz' bestimmt und kann daher vorläufig nicht näher begründet werden."
↑ Kleene 2002, p. 441.
↑ ^20.0 ^20.1 ^20.2 Applied Logic, Univ. of Cornell: Lecture 9. Last Retrieved: 2016-06-25
↑ "Remember, the way that you prove an implication is by assuming the hypothesis."—Philip Wadler, on 2 November 2015, in his Keynote: "Propositions as Types". Minute 14:36 /55:28 of Code Mesh video clip
↑ Tait WW (2010). "Gentzen's original consistency proof and the Bar Theorem" (PDF). In Kahle R, Rathjen M (eds.). Gentzen's Centenary: The Quest for Consistency. New York: Springer. pp. 213–228.
↑ Jan von Plato, Elements of Logical Reasoning, Cambridge University Press, 2014, p. 32.
↑ Andrzej-Indrzejczak, An Introduction to the Theory and Applications of Propositional Sequent Calculi (2021, chapter "Gentzen's Sequent Calculus LK"). Accessed 3 August 2022.
↑ Smullyan 1995, p. 107
↑ Kleene 2002, p. 336, wrote in 1967 that "it was a major logical discovery by Gentzen 1934–5 that, when there is any (purely logical) proof of a proposition, there is a direct proof. The implications of this discovery are in theoretical logical investigations, rather than in building collections of proved formulas."
↑ Gentzen 1934, p. 194, wrote: "Der Unterschied zwischen intuitionistischer und klassischer Logik ist bei den Kalkülen LJ und LK äußerlich ganz anderer Art als bei NJ und NK. Dort bestand er in Weglassung bzw. Hinzunahme des Satzes vom ausgeschlossenen Dritten, während er hier durch die Sukzedensbedingung ausgedrückt wird." English translation: "The difference between intuitionistic and classical logic is in the case of the calculi LJ and LK of an extremely, totally different kind to the case of NJ and NK. In the latter case, it consisted of the removal or addition respectively of the excluded middle rule, whereas in the former case, it is expressed through the succedent conditions."

संदर्भ

Buss, Samuel R. (1998). "An introduction to proof theory". In Samuel R. Buss (ed.). Handbook of proof theory. Elsevier. pp. 1–78. ISBN 0-444-89840-9.
Curry, Haskell Brooks (1977) [1963]. Foundations of mathematical logic. New York: Dover Publications Inc. ISBN 978-0-486-63462-3.
Gentzen, Gerhard Karl Erich (1934). "Untersuchungen über das logische Schließen. I". Mathematische Zeitschrift. 39 (2): 176–210. doi:10.1007/BF01201353. S2CID 121546341.
Gentzen, Gerhard Karl Erich (1935). "Untersuchungen über das logische Schließen. II". Mathematische Zeitschrift. 39 (3): 405–431. doi:10.1007/bf01201363. S2CID 186239837.
Girard, Jean-Yves; Paul Taylor; Yves Lafont (1990) [1989]. Proofs and Types. Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 7). ISBN 0-521-37181-3.
Hilbert, David; Bernays, Paul (1970) [1939]. Grundlagen der Mathematik II (Second ed.). Berlin, New York: Springer-Verlag. ISBN 978-3-642-86897-9.
Kleene, Stephen Cole (2009) [1952]. Introduction to metamathematics. Ishi Press International. ISBN 978-0-923891-57-2.
Kleene, Stephen Cole (2002) [1967]. Mathematical logic. Mineola, New York: Dover Publications. ISBN 978-0-486-42533-7.
Lemmon, Edward John (1965). Beginning logic. Thomas Nelson. ISBN 0-17-712040-1.
Smullyan, Raymond Merrill (1995) [1968]. First-order logic. New York: Dover Publications. ISBN 978-0-486-68370-6.
Suppes, Patrick Colonel (1999) [1957]. Introduction to logic. Mineola, New York: Dover Publications. ISBN 978-0-486-40687-9.

बाहरी संबंध

[gentzen19341935-1] 1.0 ^1.1 Gentzen 1934, Gentzen 1935.

[curry_cut_elimination-2] 2.0 ^2.1 Curry 1977, pp. 208–213, विलोपन प्रमेय का 5-पृष्ठ प्रमाण देता है। पेज 188, 250 भी देखें।

[kleene_cut_elimination-3] 3.0 ^3.1 Kleene 2009, pp. 453, कट-एलिमिनेशन प्रमेय का एक बहुत ही संक्षिप्त प्रमाण देता है।

[4] Curry 1977, pp. 189–244, calls Gentzen systems LC systems. Curry's emphasis is more on theory than on practical logic proofs.

[5] Kleene 2009, pp. 440–516. This book is much more concerned with the theoretical, metamathematical implications of Gentzen-style sequent calculus than applications to practical logic proofs.

[6] Kleene 2002, pp. 283–312, 331–361, defines Gentzen systems and proves various theorems within these systems, including Gödel's completeness theorem and Gentzen's theorem.

[7] Smullyan 1995, pp. 101–127, gives a brief theoretical presentation of Gentzen systems. He uses the tableau proof layout style.

[8] Curry 1977, pp. 184–244, compares natural deduction systems, denoted LA, and Gentzen systems, denoted LC. Curry's emphasis is more theoretical than practical.

[9] Suppes 1999, pp. 25–150, is an introductory presentation of practical natural deduction of this kind. This became the basis of System L.

[10] Lemmon 1965 is an elementary introduction to practical natural deduction based on the convenient abbreviated proof layout style System L based on Suppes 1999, pp. 25–150.

[11] Here, "whenever" is used as an informal abbreviation "for every assignment of values to the free variables in the judgment"

[pvs-prover-12] Shankar, Natarajan; Owre, Sam; Rushby, John M.; Stringer-Calvert, David W. J. (2001-11-01). "पीवीएस प्रोवर गाइड" (PDF). User guide. SRI International. Retrieved 2015-05-29.

[13] For explanations of the disjunctive semantics for the right side of sequents, see Curry 1977, pp. 189–190, Kleene 2002, pp. 290, 297, Kleene 2009, p. 441, Hilbert & Bernays 1970, p. 385, Smullyan 1995, pp. 104–105 and Gentzen 1934, p. 180.

[14] Buss 1998, p. 10

[15] Gentzen 1934, p. 188. "Der Kalkül NJ hat manche formale Unschönheiten."

[16] Gentzen 1934, p. 191. "In dem klassischen Kalkül NK nahm der Satz vom ausgeschlossenen Dritten eine Sonderstellung unter den Schlußweisen ein [...], indem er sich der Einführungs- und Beseitigungssystematik nicht einfügte. Bei dem im folgenden anzugebenden logistischen klassichen Kalkül LK wird diese Sonderstellung aufgehoben."

[17] Gentzen 1934, p. 191. "Die damit erreichte Symmetrie erweist sich als für die klassische Logik angemessener."

[18] Gentzen 1934, p. 191. "Hiermit haben wir einige Gesichtspunkte zur Begründung der Aufstellung der folgenden Kalküle angegeben. Im wesentlichen ist ihre Form jedoch durch die Rücksicht auf den nachher zu beweisenden 'Hauptsatz' bestimmt und kann daher vorläufig nicht näher begründet werden."

[19] Kleene 2002, p. 441.

[Cornell09-20] 20.0 ^20.1 ^20.2 Applied Logic, Univ. of Cornell: Lecture 9. Last Retrieved: 2016-06-25

[Wadler-21] "Remember, the way that you prove an implication is by assuming the hypothesis."—Philip Wadler, on 2 November 2015, in his Keynote: "Propositions as Types". Minute 14:36 /55:28 of Code Mesh video clip

[Tait-22] Tait WW (2010). "Gentzen's original consistency proof and the Bar Theorem" (PDF). In Kahle R, Rathjen M (eds.). Gentzen's Centenary: The Quest for Consistency. New York: Springer. pp. 213–228.

[23] Jan von Plato, Elements of Logical Reasoning, Cambridge University Press, 2014, p. 32.

[24] Andrzej-Indrzejczak, An Introduction to the Theory and Applications of Propositional Sequent Calculi (2021, chapter "Gentzen's Sequent Calculus LK"). Accessed 3 August 2022.

[25] Smullyan 1995, p. 107

[26] Kleene 2002, p. 336, wrote in 1967 that "it was a major logical discovery by Gentzen 1934–5 that, when there is any (purely logical) proof of a proposition, there is a direct proof. The implications of this discovery are in theoretical logical investigations, rather than in building collections of proved formulas."

[27] Gentzen 1934, p. 194, wrote: "Der Unterschied zwischen intuitionistischer und klassischer Logik ist bei den Kalkülen LJ und LK äußerlich ganz anderer Art als bei NJ und NK. Dort bestand er in Weglassung bzw. Hinzunahme des Satzes vom ausgeschlossenen Dritten, während er hier durch die Sukzedensbedingung ausgedrückt wird." English translation: "The difference between intuitionistic and classical logic is in the case of the calculi LJ and LK of an extremely, totally different kind to the case of NJ and NK. In the latter case, it consisted of the removal or addition respectively of the excluded middle rule, whereas in the former case, it is expressed through the succedent conditions."

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

Anonymous

Search

अनुक्रमिक गणना: Difference between revisions

Namespaces

More

Page actions

Latest revision as of 16:56, 12 June 2023

Contents

अवलोकन

हिल्बर्ट-शैली निगमन प्रणाली

प्राकृतिक निगमन प्रणाली

अनुक्रमिक कैलकुलस सिस्टम

प्राकृतिक निगमन और अनुक्रमिक कलन के बीच का अंतर

अनुक्रम शब्द की उत्पत्ति

तार्किक सूत्र प्रमाणन

रिडक्शन ट्री

मानक स्वयंसिद्धीकरणों से संबंध

प्रणाली LK

अनुमान नियम

एक सहज व्याख्या

उदाहरण व्युत्पत्ति

विश्लेषणात्मक चित्र से संबंध

संरचनात्मक नियम

प्रणाली LK के गुण

रूपांतर

लघु संरचनात्मक विकल्प

असंगति

अवसंरचनात्मक तर्क

अंतर्ज्ञानी अनुक्रम कलन: प्रणाली LJ

यह भी देखें

टिप्पणियाँ

संदर्भ

बाहरी संबंध

Navigation

Navigation

Wiki tools

Wiki tools

@@ Line 1: / Line 1: @@
 {{Short description|Style of formal logical argumentation}}
-गणितीय [[तर्क]] में, अनुक्रमिक कलन औपचारिक तार्किक तर्क की एक शैली है जिसमें एक [[औपचारिक प्रमाण]] की प्रत्येक पंक्ति एक बिना शर्त पुनरुक्ति के बजाय एक सशर्त पुनरुक्ति (तर्क) ([[गेरहार्ड जेंटजन]] द्वारा अनुक्रम कहा जाता है) है। नियमों और [[अनुमान]] की प्रक्रियाओं के अनुसार एक [[औपचारिक तर्क]] में पहले की पंक्तियों पर अन्य सशर्त टॉटोलॉजी से प्रत्येक सशर्त टॉटोलॉजी का अनुमान लगाया जाता है, जो गणितज्ञों द्वारा डेविड हिल्बर्ट की तुलना में कटौती की प्राकृतिक शैली के लिए एक बेहतर सन्निकटन देता है। डेविड हिल्बर्ट की औपचारिक तर्क की पहले की शैली, जिसमें हर पंक्ति एक बिना शर्त पुनरुक्ति थी। अधिक सूक्ष्म भेद मौजूद हो सकते हैं; उदाहरण के लिए, प्रस्ताव अंतर्निहित रूप से गैर-तार्किक सिद्धांतों पर निर्भर हो सकते हैं। उस मामले में, अनुक्रम पहले क्रम के तर्क में सशर्त [[प्रमेय]]ों को दर्शाते हैं | सशर्त पुनरुक्ति के बजाय प्रथम-क्रम की भाषा।
+गणितीय [[तर्क]] में अनुक्रमिक कलन औपचारिक तार्किक तर्क की एक शैली है। जिसमें [[औपचारिक प्रमाण]] की प्रत्येक पंक्ति एक अप्रतिबन्ध पुनरुक्ति के अतिरिक्त एक नियमबद्ध पुनरुक्ति (तर्क) ([[गेरहार्ड जेंटजन]] के अनुसार अनुक्रम कहा जाता है) है। नियमों और [[अनुमान]] की प्रक्रियाओं के अनुसार [[औपचारिक तर्क]] में पूर्व की पंक्तियों पर अन्य नियमबद्ध पुनरुक्ति से प्रत्येक नियमबद्ध पुनरुक्ति का अनुमान लगाया जाता है जो गणितज्ञों के अनुसार डेविड हिल्बर्ट की तुलना में निगमन की प्राकृतिक शैली के लिए एक श्रेष्ठतर सन्निकटन देता है। डेविड हिल्बर्ट की औपचारिक तर्क की पूर्व की शैली जिसमें प्रत्येक पंक्ति एक नियमबद्ध पुनरुक्ति थी। जिसमे अधिक सूक्ष्म मुख्यता उपस्थित हो सकते हैं। उदाहरण के रूप मे प्रस्ताव अंतर्निहित रूप से अतार्किक सिद्धांतों पर निर्भर हो सकते हैं। उस स्थितियों में अनुक्रम पूर्व क्रम के तर्क में नियमबद्ध [[प्रमेय]] को प्रकट करते हैं | नियमबद्ध पुनरुक्ति के अतिरिक्त प्रथम-क्रम की भाषा है।
-पंक्ति-दर-पंक्ति तार्किक तर्कों को व्यक्त करने के लिए अनुक्रम कलन, प्रमाण कलन की कई मौजूदा शैलियों में से एक है।
+पंक्ति-दर-पंक्ति तार्किक तर्कों को व्यक्त करने के लिए अनुक्रम कलन, प्रमाण कलन की अनेक वर्तमान शैलियों में से एक है।
-* [[हिल्बर्ट प्रणाली]]। हर पंक्ति एक बिना शर्त पुनरुक्ति (या प्रमेय) है।
+* [[हिल्बर्ट प्रणाली|हिल्बर्ट शैली]]- प्रत्येक पंक्ति एक नियमबद्ध पुनरुक्ति ( अथवा प्रमेय) है।
-* जेंटजन स्टाइल। प्रत्येक पंक्ति बाईं ओर शून्य या अधिक शर्तों के साथ एक सशर्त पुनरुक्ति (या प्रमेय) है।
+* जेंटजन शैली- प्रत्येक पंक्ति बाएं ओर शून्य अथवा अधिक नियमों के साथ एक नियमबद्ध पुनरुक्ति ( अथवा प्रमेय) है।
-** [[प्राकृतिक कटौती]]। प्रत्येक (सशर्त) पंक्ति में दाईं ओर एक निश्चित प्रस्ताव है।
+** [[प्राकृतिक कटौती|प्राकृतिक निगमन]]- प्रत्येक (नियमबद्ध) पंक्ति में दाईं ओर निश्चित प्रस्ताव है।
-** अनुक्रमिक कलन। प्रत्येक (सशर्त) रेखा में दाईं ओर शून्य या अधिक मुखर प्रस्ताव होते हैं।
+** अनुक्रमिक कलन- प्रत्येक (नियमबद्ध) रेखा में दाईं ओर शून्य अथवा अधिक मुखर प्रस्ताव होते हैं।
-दूसरे शब्दों में, प्राकृतिक कटौती और अनुक्रमिक कलन प्रणालियाँ विशेष रूप से विशिष्ट प्रकार की जेंटजन-शैली प्रणालियाँ हैं। हिल्बर्ट-शैली प्रणालियों में आमतौर पर बहुत कम संख्या में अनुमान नियम होते हैं, जो [[स्वयंसिद्ध]]ों के सेट पर अधिक निर्भर करते हैं। जेंटजन-शैली प्रणालियों में आमतौर पर बहुत कम स्वयंसिद्ध होते हैं, यदि कोई हो, तो नियमों के सेट पर अधिक निर्भर करते हैं।
+दूसरे शब्दों में प्राकृतिक निगमन और अनुक्रमिक कलन प्रणालियाँ विशेष रूप से विशिष्ट प्रकार की जेंटजन-शैली प्रणालियाँ हैं। हिल्बर्ट-शैली प्रणालियों में सामान्यतः अति कम संख्या में अनुमान नियम होते हैं, जो [[स्वयंसिद्ध]] के समुच्चय पर अधिक निर्भर करते हैं। जेंटजन-शैली प्रणालियों में सामान्यतः अति कम स्वयं सिद्ध होते हैं। यदि कोई हो, तो नियमों के समुच्चय पर अधिक निर्भर करते हैं।
-हिल्बर्ट-शैली प्रणालियों की तुलना में जेंटजन-शैली प्रणालियों के महत्वपूर्ण व्यावहारिक और सैद्धांतिक लाभ हैं। उदाहरण के लिए, दोनों प्राकृतिक कटौती और अनुक्रमिक कलन प्रणालियाँ सार्वभौमिक और अस्तित्वगत [[परिमाणीकरण (तर्क)]] के उन्मूलन और परिचय की सुविधा प्रदान करती हैं ताकि प्रस्तावात्मक कलन के बहुत सरल नियमों के अनुसार अगणित तार्किक अभिव्यक्तियों में हेरफेर किया जा सके। एक विशिष्ट तर्क में, क्वांटिफायर्स को समाप्त कर दिया जाता है, फिर [[प्रस्तावक गणना]] को अनक्वांटिफाइड एक्सप्रेशंस (जिसमें आमतौर पर फ्री वेरिएबल्स होते हैं) पर लागू किया जाता है, और फिर क्वांटिफायर्स को फिर से प्रस्तुत किया जाता है। यह बहुत हद तक उस तरीके से मेल खाता है जिसमें गणितज्ञों द्वारा अभ्यास में गणितीय प्रमाणों का प्रयोग किया जाता है। विधेय कलन प्रमाण आमतौर पर इस दृष्टिकोण के साथ खोजने में बहुत आसान होते हैं, और अक्सर छोटे होते हैं। प्राकृतिक निगमन प्रणालियाँ व्यावहारिक प्रमेय सिद्ध करने के लिए अधिक अनुकूल हैं। सैद्धांतिक विश्लेषण के लिए अनुक्रमिक कलन प्रणाली अधिक अनुकूल हैं।
+हिल्बर्ट-शैली प्रणालियों की तुलना में जेंटजन-शैली प्रणालियों के महत्वपूर्ण व्यावहारिक और सैद्धांतिक लाभ हैं। उदाहरण के रूप मे दोनों प्राकृतिक निगमन और अनुक्रमिक कलन प्रणालियाँ सार्वभौमिक और अस्तित्वगत [[परिमाणीकरण (तर्क)]] के उन्मूलन और परिचय की सुविधा प्रदान करती हैं। जिससे प्रस्तावात्मक कलन के अति सरल नियमों के अनुसार अगणित तार्किक अभिव्यक्तियों में परिवर्तन किया जा सके। एक विशिष्ट तर्क में परिमाणकों को समाप्त कर दिया जाता है, तब [[प्रस्तावक गणना]] को अपरिमित अभिव्यक्ति (जिसमें सामान्यतः स्वतंत्र परिवर्तनशील होते हैं) पर प्रयुक्त किया जाता है, और तब परिमाणकों को पुनः प्रस्तुत किया जाता है। यह अति स्तर तक उस विधियों से अनुकूल होता है जिसमें गणितज्ञों के अनुसार अभ्यास में गणितीय प्रमाणों का प्रयोग किया जाता है। विधेय कलन प्रमाण अधिकांशतः छोटे होते हैं और सामान्यतः इस दृष्टिकोण के साथ प्रकट करने में अति सहज होते हैं। प्राकृतिक निगमन प्रणालियाँ व्यावहारिक प्रमेय सिद्ध करने के लिए अधिक अनुकूल हैं। सैद्धांतिक विश्लेषण के लिए अनुक्रमिक कलन प्रणाली अधिक अनुकूल हैं।
-== सिंहावलोकन<!--'Gentzen system' and 'Gentzen systems' redirect here-->==
+== अवलोकन ==
-[[सबूत सिद्धांत]] और गणितीय तर्क में, अनुक्रमिक कलन औपचारिक प्रणालियों का एक परिवार है जो अनुमान की एक निश्चित शैली और कुछ औपचारिक गुणों को साझा करता है। पहली अनुक्रमिक गणना प्रणाली, एलके और एलजे, 1934/1935 में गेरहार्ड जेंटजन द्वारा पेश की गई थी।<ref name=gentzen19341935>{{harvnb|Gentzen|1934}}, {{harvnb|Gentzen|1935}}.</ref> प्रथम-क्रम तर्क (क्रमशः [[शास्त्रीय तर्क]] और [[अंतर्ज्ञानवादी तर्क]] संस्करणों में) में प्राकृतिक कटौती का अध्ययन करने के लिए एक उपकरण के रूप में। LK और LJ के बारे में Gentzen का तथाकथित मुख्य प्रमेय (Hauptsatz) [[कट-उन्मूलन प्रमेय]] था,<ref name=curry_cut_elimination>{{harvnb|Curry|1977|pp=208–213}}, विलोपन प्रमेय का 5-पृष्ठ प्रमाण देता है। पेज 188, 250 भी देखें।</ref><ref name=kleene_cut_elimination>{{harvnb|Kleene|2009|pp=453}}, कट-एलिमिनेशन प्रमेय का एक बहुत ही संक्षिप्त प्रमाण देता है। </ref> दूरगामी [[मेटाथ्योरी]]|मेटा-सैद्धांतिक परिणामों के साथ संगति सहित एक परिणाम। जेंटजन ने कुछ साल बाद इस तकनीक की शक्ति और लचीलेपन का प्रदर्शन किया, गोडेल के अपूर्णता प्रमेय के आश्चर्यजनक जवाब में, एक (ट्रांसफिनिट) जेंटजेन की स्थिरता प्रमाण देने के लिए एक कट-उन्मूलन तर्क लागू किया। इस प्रारंभिक कार्य के बाद से, अनुक्रमिक कैलकुली, जिसे जेंटजेन सिस्टम भी कहा जाता है<!--boldface per WP:R#PLA-->,<ref>{{harvnb|Curry|1977|pp=189–244}}, calls Gentzen systems LC systems. Curry's emphasis is more on theory than on practical logic proofs.</ref><ref>{{harvnb|Kleene|2009|pp=440–516}}. This book is much more concerned with the theoretical, metamathematical implications of Gentzen-style sequent calculus than applications to practical logic proofs.</ref><ref>{{harvnb|Kleene|2002|pp=283–312, 331–361}}, defines Gentzen systems and proves various theorems within these systems, including Gödel's completeness theorem and Gentzen's theorem.</ref><ref>{{harvnb|Smullyan|1995|pp=101–127}}, gives a brief theoretical presentation of Gentzen systems. He uses the tableau proof layout style.</ref> और उनसे संबंधित सामान्य अवधारणाओं को प्रमाण सिद्धांत, गणितीय तर्क और [[स्वचालित कटौती]] के क्षेत्र में व्यापक रूप से लागू किया गया है।
+[[सबूत सिद्धांत|प्रमाण सिद्धांत]] और गणितीय तर्क में अनुक्रमिक कलन औपचारिक प्रणालियों का एक संतति है जो अनुमान की निश्चित शैली और कुछ औपचारिक गुणों को साझा करता है। प्रथम अनुक्रमिक गणना प्रणाली LK और LJ 1934/1935 में गेरहार्ड जेंटजन के अनुसार प्रस्तुत की गई थी।<ref name=gentzen19341935>{{harvnb|Gentzen|1934}}, {{harvnb|Gentzen|1935}}.</ref> प्रथम-क्रम तर्क (क्रमशः [[शास्त्रीय तर्क|मौलिक तर्क]] और [[अंतर्ज्ञानवादी तर्क]] संस्करणों में) में प्राकृतिक निगमन का अध्ययन करने के लिए उपकरण के रूप में थी। LK और LJ के संबंध में जेंटजन का तथाकथित मुख्य प्रमेय (हॉपट॒सत्ज़) [[कट-उन्मूलन प्रमेय|परिवर्तन -उन्मूलन प्रमेय]] था।<ref name=curry_cut_elimination>{{harvnb|Curry|1977|pp=208–213}}, विलोपन प्रमेय का 5-पृष्ठ प्रमाण देता है। पेज 188, 250 भी देखें।</ref><ref name=kleene_cut_elimination>{{harvnb|Kleene|2009|pp=453}}, कट-एलिमिनेशन प्रमेय का एक बहुत ही संक्षिप्त प्रमाण देता है। </ref> दूरगामी [[मेटाथ्योरी|मेटा-सैद्धांतिक]] परिणामों के साथ संगति संयुक्त एक परिणाम है। जेंटजन ने कुछ साल उपरांत इस प्रविधि की शक्ति और लचीलेपन का प्रदर्शन किया। गोडेल के अपूर्णता प्रमेय के आश्चर्यजनक उत्तर में (परिमित) जेंटजेन की स्थिरता प्रमाण देने के लिए एक परिवर्तन -उन्मूलन तर्क प्रयुक्त किया। इस प्रारंभिक कार्य के उपरांत से अनुक्रमिक गणना, जिसे जेंटजेन प्रणाली भी कहा जाता है,<ref>{{harvnb|Curry|1977|pp=189–244}}, calls Gentzen systems LC systems. Curry's emphasis is more on theory than on practical logic proofs.</ref><ref>{{harvnb|Kleene|2009|pp=440–516}}. This book is much more concerned with the theoretical, metamathematical implications of Gentzen-style sequent calculus than applications to practical logic proofs.</ref><ref>{{harvnb|Kleene|2002|pp=283–312, 331–361}}, defines Gentzen systems and proves various theorems within these systems, including Gödel's completeness theorem and Gentzen's theorem.</ref><ref>{{harvnb|Smullyan|1995|pp=101–127}}, gives a brief theoretical presentation of Gentzen systems. He uses the tableau proof layout style.</ref> और उनसे संबंधित सामान्य अवधारणाओं को प्रमाण सिद्धांत गणितीय तर्क और [[स्वचालित कटौती|स्वचालित निगमन]] के क्षेत्र में व्यापक रूप से प्रयुक्त किया गया है।
-=== [[हिल्बर्ट-शैली कटौती प्रणाली]] ===
+=== [[हिल्बर्ट-शैली कटौती प्रणाली|'''हिल्बर्ट-शैली निगमन प्रणाली''']] ===
-कटौती प्रणालियों की विभिन्न शैलियों को वर्गीकृत करने का एक तरीका सिस्टम में [[निर्णय (गणितीय तर्क)]] के रूप को देखना है, यानी, कौन सी चीजें एक (उप) प्रमाण के निष्कर्ष के रूप में प्रकट हो सकती हैं। हिल्बर्ट-शैली की कटौती प्रणालियों में सबसे सरल निर्णय प्रपत्र का उपयोग किया जाता है, जहाँ एक निर्णय का रूप होता है
+निगमन प्रणालियों की विभिन्न शैलियों को वर्गीकृत करने का प्रणाली में [[निर्णय (गणितीय तर्क)]] के रूप को देखना है, अर्थात कौन सी काम (उप) प्रमाण के निष्कर्ष के रूप में प्रकट हो सकती हैं। हिल्बर्ट-शैली की निगमन प्रणालियों में सबसे सरल निर्णय प्रपत्र का उपयोग किया जाता है। जहाँ निर्णय का रूप निम्म होता है
 :<math>B</math>
-कहाँ <math>B</math> प्रथम-क्रम तर्क (या जो भी तर्क कटौती प्रणाली पर लागू होता है, उदाहरण के लिए, प्रस्तावपरक कलन या उच्च-क्रम तर्क या एक [[मॉडल तर्क]]) का कोई भी सुव्यवस्थित सूत्र है। प्रमेय वे सूत्र हैं जो एक वैध प्रमाण में अंतिम निर्णय के रूप में प्रकट होते हैं। एक हिल्बर्ट-शैली प्रणाली को सूत्रों और निर्णयों के बीच कोई अंतर करने की आवश्यकता नहीं है; हम यहां केवल बाद के मामलों की तुलना के लिए एक बनाते हैं।
+<math>B</math> प्रथम-क्रम तर्क ( अथवा जो भी तर्क निगमन प्रणाली पर प्रयुक्त होता है। उदाहरण के रूप मे प्रस्तावपरक कलन अथवा उच्च-क्रम तर्क अथवा एक [[मॉडल तर्क|प्रतिरूप तर्क]]) का कोई भी सुव्यवस्थित सूत्र है। प्रमेय वह सूत्र हैं जो एक वैध प्रमाण में अंतिम निर्णय के रूप में प्रकट होते हैं। हिल्बर्ट-शैली प्रणाली को सूत्रों और निर्णयों के बीच कोई अंतर करने की आवश्यकता नहीं है। हम यहां मात्र उपरांत के स्थितियों की तुलना के लिए बनाते हैं।
-हिल्बर्ट-शैली प्रणाली के सरल वाक्य-विन्यास के लिए भुगतान की गई कीमत यह है कि पूर्ण औपचारिक प्रमाण बहुत लंबे हो जाते हैं। ऐसी प्रणाली में सबूत के बारे में ठोस तर्क लगभग हमेशा [[कटौती प्रमेय]] के लिए अपील करते हैं। यह कटौती प्रमेय को प्रणाली में एक औपचारिक नियम के रूप में शामिल करने के विचार की ओर ले जाता है, जो प्राकृतिक कटौती में होता है।
+हिल्बर्ट-शैली प्रणाली के सरल वाक्य-विन्यास के लिए भुगतान किया गया मान यह है, कि पूर्ण औपचारिक प्रमाण अति दीर्घ हो जाते हैं। ऐसी प्रणाली में प्रमाण के संबंध में ठोस तर्क लगभग सदैव [[कटौती प्रमेय|निगमन प्रमेय]] के लिए अनुरोध करते हैं। यह निगमन प्रमेय को प्रणाली में औपचारिक नियम के रूप में सम्मिलित करने के विचार की ओर ले जाता है, जो प्राकृतिक निगमन में होता है।
-=== प्राकृतिक कटौती प्रणाली ===
+=== प्राकृतिक निगमन प्रणाली ===
-प्राकृतिक कटौती में, निर्णयों का आकार होता है
+प्राकृतिक निगमन में निर्णयों का आकार होता है।
 :<math>A_1, A_2, \ldots, A_n \vdash B</math>
-जहां <math>A_i</math>'रेत <math>B</math> फिर से सूत्र हैं और <math>n\geq 0</math>. के क्रमपरिवर्तन <math>A_i</math>सारहीन हैं। दूसरे शब्दों में, एक निर्णय में [[घूमने वाला दरवाज़ा (प्रतीक)]]प्रतीक) प्रतीक के बाईं ओर सूत्रों की एक सूची (संभवतः खाली) होती है।<math>\vdash</math>, दाईं ओर एक सूत्र के साथ।<ref>{{harvnb|Curry|1977|pp=184–244}}, compares natural deduction systems, denoted LA, and Gentzen systems, denoted LC. Curry's emphasis is more theoretical than practical.</ref><ref>{{harvnb|Suppes|1999|pp=25–150}}, is an introductory presentation of practical natural deduction of this kind. This became the basis of [[System L]].</ref><ref>{{harvnb|Lemmon|1965}} is an elementary introduction to practical natural deduction based on the convenient abbreviated proof layout style [[System L]] based on {{harvnb|Suppes|1999|pp=25–150}}.</ref> प्रमेय वे सूत्र हैं <math>B</math> ऐसा है कि <math>\vdash B</math> (खाली बायीं ओर) एक वैध प्रमाण का निष्कर्ष है।
+जिस स्थान पर <math>A_i</math> और <math>B</math> पुनः सूत्र हैं, और <math>n\geq 0</math>. के क्रमपरिवर्तन <math>A_i</math> सारहीन हैं। दूसरे शब्दों में निर्णय में [[घूमने वाला दरवाज़ा (प्रतीक)|टर्नस्टाइल (प्रतीक)]] <math>\vdash</math> के बाएं ओर सूत्रों की सूची (संभवतः रिक्त ) होती है, जिसमे दाईं ओर सूत्र होता है।<ref>{{harvnb|Curry|1977|pp=184–244}}, compares natural deduction systems, denoted LA, and Gentzen systems, denoted LC. Curry's emphasis is more theoretical than practical.</ref><ref>{{harvnb|Suppes|1999|pp=25–150}}, is an introductory presentation of practical natural deduction of this kind. This became the basis of [[System L]].</ref><ref>{{harvnb|Lemmon|1965}} is an elementary introduction to practical natural deduction based on the convenient abbreviated proof layout style [[System L]] based on {{harvnb|Suppes|1999|pp=25–150}}.</ref> प्रमेय वह सूत्र <math>B</math> हैं जैसे कि <math>\vdash B</math> ( रिक्त बायीं ओर) वैध प्रमाण का निष्कर्ष है। (प्राकृतिक निगमन की कुछ प्रस्तुतियों में <math>A_i</math>s और टर्नस्टाइल स्पष्ट रूप से नहीं लिखा गया है। इसके अतरिक्त द्वि-आयामी संकेतन का उपयोग किया जाता है, जिससे उनका अनुमान लगाया जा सकता है।)
-(प्राकृतिक कटौती की कुछ प्रस्तुतियों में, <math>A_i</math>एस और घूमने वाला दरवाज़ा स्पष्ट रूप से नहीं लिखा गया है; इसके बजाय एक द्वि-आयामी संकेतन का उपयोग किया जाता है जिससे उनका अनुमान लगाया जा सकता है।)
-प्राकृतिक कटौती में एक निर्णय का मानक शब्दार्थ यह है कि यह दावा करता है कि जब भी<ref>Here, "whenever" is used as an informal abbreviation "for every assignment of values to the free variables in the judgment"</ref> <math>A_1</math>, <math>A_2</math>आदि सब सत्य हैं, <math>B</math> भी सच होगा। निर्णय
+प्राकृतिक निगमन में निर्णय का मानक शब्दार्थ यह है कि यह अनुरोध करता है कि जब भी<ref>Here, "whenever" is used as an informal abbreviation "for every assignment of values to the free variables in the judgment"</ref> <math>A_1</math>, <math>A_2</math> आदि सब सत्य हैं तो <math>B</math> भी सत्य होगा। निर्णय
 :<math>A_1, \ldots, A_n \vdash B</math>
 और
 :<math>\vdash (A_1 \land \cdots \land A_n) \rightarrow B</math>
-मजबूत अर्थों में समतुल्य हैं कि किसी एक के प्रमाण को दूसरे के प्रमाण तक बढ़ाया जा सकता है।
+दृढ़ अर्थों में समतुल्य हैं, कि किसी एक के प्रमाण को दूसरे के प्रमाण तक बढ़ाया जा सकता है।
-=== अनुक्रमिक कैलकुस सिस्टम ===
+=== अनुक्रमिक कैलकुलस सिस्टम ===
-अंत में, अनुक्रमिक कैलकुस प्राकृतिक कटौती निर्णय के रूप को सामान्यीकृत करता है
+अंत में अनुक्रमिक कैलकुलस प्राकृतिक निगमन निर्णय के रूप को सामान्यीकृत करता है
 : <math>A_1, \ldots, A_n \vdash B_1, \ldots, B_k,</math>
-एक सिंटैक्टिक ऑब्जेक्ट जिसे अनुक्रम कहा जाता है। टर्नस्टाइल (प्रतीक) के बायीं ओर के सूत्रों को पूर्ववर्ती कहा जाता है, और दायीं ओर के सूत्रों को क्रमिक या परिणामी कहा जाता है; साथ में उन्हें सीडेंट या अनुक्रम कहा जाता है।<ref name="pvs-prover">{{cite web |url=http://pvs.csl.sri.com/doc/pvs-prover-guide.pdf |title=पीवीएस प्रोवर गाइड|last1=Shankar |first1=Natarajan |author-link=Natarajan Shankar |last2=Owre |first2=Sam |last3=Rushby |first3=John M. |author-link3=John Rushby |last4=Stringer-Calvert |first4=David W. J. |work=User guide |publisher=[[SRI International]] |date=2001-11-01 |access-date=2015-05-29 }}</ref> दोबारा, <math>A_i</math> और <math>B_i</math> सूत्र हैं, और <math>n</math> और <math>k</math> गैर-नकारात्मक पूर्णांक हैं, अर्थात, बाएँ हाथ की ओर या दाईं ओर (या दोनों में से कोई भी) खाली हो सकता है। प्राकृतिक कटौती के रूप में, प्रमेय वे हैं <math>B</math> कहाँ <math>\vdash B</math> एक वैध प्रमाण का निष्कर्ष है।
+एक वाक्यात्मक प्रदर्शन जिसे अनुक्रम कहा जाता है। टर्नस्टाइल (प्रतीक) के बायीं ओर के सूत्रों को पूर्ववर्ती कहा जाता है, और दायीं ओर के सूत्रों को क्रमिक अथवा परिणामी कहा जाता है। साथ में उन्हें विनम्र अथवा अनुक्रम कहा जाता है।<ref name="pvs-prover">{{cite web |url=http://pvs.csl.sri.com/doc/pvs-prover-guide.pdf |title=पीवीएस प्रोवर गाइड|last1=Shankar |first1=Natarajan |author-link=Natarajan Shankar |last2=Owre |first2=Sam |last3=Rushby |first3=John M. |author-link3=John Rushby |last4=Stringer-Calvert |first4=David W. J. |work=User guide |publisher=[[SRI International]] |date=2001-11-01 |access-date=2015-05-29 }}</ref> पुनः , <math>A_i</math> और <math>B_i</math> सूत्र हैं, और <math>n</math> और <math>k</math> अनकारात्मक पूर्णांक हैं, अर्थात बाएँ ओर अथवा दाईं ओर ( अथवा दोनों में से कोई भी) रिक्त हो सकता है। प्राकृतिक निगमन के रूप में प्रमेय वह हैं <math>B</math> जहाँ <math>\vdash B</math> वैध प्रमाण का निष्कर्ष है।
-एक अनुक्रम का मानक शब्दार्थ एक दावा है कि जब भी हर  <math> A_i</math> सच है, कम से कम एक <math>B_i</math> भी सच होगा।<ref>For explanations of the disjunctive semantics for the right side of sequents, see {{harvnb|Curry|1977|pp=189–190}}, {{harvnb|Kleene|2002|pp=290, 297}}, {{harvnb|Kleene|2009|p=441}}, {{harvnb|Hilbert|Bernays|1970|p=385}}, {{harvnb|Smullyan|1995|pp=104–105}} and {{harvnb|Gentzen|1934|p=180}}.</ref> इस प्रकार खाली अनुक्रम, जिसमें दोनों सीडेंट खाली हैं, झूठा है।<ref>{{harvnb|Buss|1998|p=10}}</ref> इसे व्यक्त करने का एक तरीका यह है कि घूमने वाले दरवाज़े के बाईं ओर के अल्पविराम को और के रूप में माना जाना चाहिए, और घूमने वाले दरवाज़े के दाईं ओर के अल्पविराम को एक (सम्मिलित) या के रूप में माना जाना चाहिए। अनुक्रम
+एक अनुक्रम का मानक शब्दार्थ एक अनुरोध है कि जब भी प्रत्येक <math> A_i</math> सत्य है एवं कम से कम एक <math>B_i</math> भी सत्य होगा।<ref>For explanations of the disjunctive semantics for the right side of sequents, see {{harvnb|Curry|1977|pp=189–190}}, {{harvnb|Kleene|2002|pp=290, 297}}, {{harvnb|Kleene|2009|p=441}}, {{harvnb|Hilbert|Bernays|1970|p=385}}, {{harvnb|Smullyan|1995|pp=104–105}} and {{harvnb|Gentzen|1934|p=180}}.</ref> इस प्रकार रिक्त अनुक्रम अवास्तविक है, जिसमें दोनों विनम्र रिक्त हैं।<ref>{{harvnb|Buss|1998|p=10}}</ref> इसे व्यक्त करने का विधि यह है कि, टर्नस्टाइल को बाएं ओर के अल्पविराम को और के रूप में उल्लिखित होना चाहिए, और टर्नस्टाइल दाईं ओर के अल्पविराम को (सम्मिलित) अथवा के रूप में माना उल्लिखित होना चाहिए। अनुक्रम
 :<math>A_1, \ldots, A_n \vdash B_1, \ldots, B_k</math>
 और
 :<math>\vdash (A_1 \land\cdots\land A_n)\rightarrow(B_1 \lor\cdots\lor B_k)</math>
-मजबूत अर्थों में समतुल्य हैं कि किसी भी क्रम के प्रमाण को दूसरे अनुक्रम के प्रमाण तक बढ़ाया जा सकता है।
+दृढ़ अर्थों में समतुल्य हैं कि किसी भी क्रम के प्रमाण को दूसरे अनुक्रम के प्रमाण तक बढ़ाया जा सकता है।
-पहली नजर में, निर्णय प्रपत्र का यह विस्तार एक अजीब जटिलता प्रतीत हो सकता है - यह प्राकृतिक कटौती की एक स्पष्ट कमी से प्रेरित नहीं है, और यह शुरू में भ्रामक है कि अल्पविराम के दोनों पक्षों पर पूरी तरह से अलग-अलग चीजों का अर्थ लगता है घूमने वाला दरवाज़ा। हालाँकि, शास्त्रीय तर्क में अनुक्रम के शब्दार्थ भी (प्रस्तावात्मक तनातनी द्वारा) या तो व्यक्त किए जा सकते हैं
+प्रथम अवलोकन में निर्णय प्रपत्र का यह विस्तार एक विचित्र जटिलता प्रतीत हो सकता है। यह प्राकृतिक निगमन की स्पष्ट आभाव से प्रेरित नहीं है, और यह प्रारंभ में भ्रामक है कि अल्पविराम के दोनों पक्षों पर पूर्ण प्रकार से प्रथक- प्रथक चीजों का अर्थ लगता है अथार्त टर्नस्टाइल है। चूंकि मौलिक तर्क में अनुक्रम के शब्दार्थ भी (प्रस्तावात्मक तनाव के अनुसार ) व्यक्त किए जा सकते हैं
 :: <math>\vdash \neg A_1 \lor \neg A_2 \lor \cdots \lor \neg A_n \lor B_1 \lor B_2 \lor\cdots\lor B_k</math>
-(कम से कम एक असत्य है, या बीएस में से एक सत्य है)
+(कम से कम एक As असत्य है, अथवा Bs में से एक सत्य है)
-: या के रूप में
+: अथवा रूप में
 :: <math>\vdash \neg(A_1 \land A_2 \land \cdots \land A_n \land \neg B_1 \land \neg B_2 \land\cdots\land \neg B_k)</math>
-(ऐसा नहीं हो सकता कि सभी As सत्य हैं और सभी Bs असत्य हैं)।
+(ऐसा नहीं हो सकता कि समस्त As सत्य हैं और समस्त Bs असत्य हैं)।
-इन योगों में, घूमने वाले दरवाज़े के दोनों ओर के सूत्रों के बीच एकमात्र अंतर यह है कि एक पक्ष को नकारा गया है। इस प्रकार, एक क्रम में बाएं से दाएं की अदला-बदली सभी घटक सूत्रों को नकारने के अनुरूप है। इसका मतलब यह है कि एक समरूपता जैसे डी मॉर्गन के कानून, जो सिमेंटिक स्तर पर खुद को तार्किक निषेध के रूप में प्रकट करते हैं, अनुक्रमों के बाएं-दाएं समरूपता में सीधे अनुवाद करते हैं- और वास्तव में, संयोजन (∧) से निपटने के लिए अनुक्रमिक कलन में अनुमान नियम हैं संयोजन से निपटने वालों की दर्पण छवियां (∨)।
+इन परिणाम में टर्नस्टाइल दोनों ओर के सूत्रों के बीच एकमात्र अंतर यह है कि एक पक्ष को अस्वीकार करा गया है। इस प्रकार एक क्रम में बाएं से दाएं की परिवर्तन समस्त घटक सूत्रों को अस्वीकार के अनुरूप है। इसका अर्थ यह है कि समरूपता जैसे डी मॉर्गन के नियम जो अर्थ स्तर पर खुद को तार्किक निषेध के रूप में प्रकट करते हैं, अनुक्रमों के बाएं-दाएं समरूपता में प्रत्यक्ष अनुवाद करते हैं और वास्तव में संयोजन (∧) से व्यवहार के लिए अनुक्रमिक कलन में निष्कर्ष नियम संयोजन (∨) से व्यवहार वालों की दर्पण छवियां है।
-कई तर्कशास्त्री महसूस करते हैं {{Citation needed|date=November 2018}} कि यह सममित प्रस्तुति सबूत प्रणाली की अन्य शैलियों की तुलना में तर्क की संरचना में गहरी अंतर्दृष्टि प्रदान करती है, जहां नियमों में नकारात्मकता का शास्त्रीय द्वंद्व उतना स्पष्ट नहीं है।
+अनेक तर्कशास्त्री अनुभव करते हैं कि यह सममित प्रस्तुति प्रमाण प्रणाली की अन्य शैलियों की तुलना में तर्क की संरचना में गहन अंतर्दृष्टि प्रदान करती है जिस स्थान पर नियमों में नकारात्मकता का मौलिक द्वंद्व उतना स्पष्ट नहीं है।
-=== प्राकृतिक कटौती और अनुक्रमिक कलन के बीच का अंतर ===
+=== प्राकृतिक निगमन और अनुक्रमिक कलन के बीच का अंतर ===
-जेंटजन ने अपने एकल-आउटपुट प्राकृतिक कटौती प्रणाली (एनके और एनजे) और उनके बहु-आउटपुट सीक्वेंट कैलकुलस सिस्टम (एलके और एलजे) के बीच एक तेज अंतर पर जोर दिया। उन्होंने लिखा है कि अंतर्ज्ञानवादी प्राकृतिक कटौती प्रणाली एनजे कुछ बदसूरत थी।<ref>{{harvnb|Gentzen|1934|p=188}}. "Der Kalkül ''NJ'' hat manche formale Unschönheiten."</ref> उन्होंने कहा कि शास्त्रीय प्राकृतिक कटौती प्रणाली एनके में बहिष्कृत मध्य के कानून की विशेष भूमिका को शास्त्रीय अनुक्रम कैलकुस प्रणाली एलके में हटा दिया गया है।<ref>{{harvnb|Gentzen|1934|p=191}}. "In dem klassischen Kalkül ''NK'' nahm der Satz vom ausgeschlossenen Dritten eine Sonderstellung unter den Schlußweisen ein [...], indem er sich der Einführungs- und Beseitigungssystematik nicht einfügte. Bei dem im folgenden anzugebenden logistischen klassichen Kalkül ''LK'' wird diese Sonderstellung aufgehoben."</ref> उन्होंने कहा कि अनुक्रमिक कलन एलजे ने अंतर्ज्ञानवादी तर्क के मामले में प्राकृतिक कटौती एनजे की तुलना में अधिक समरूपता प्रदान की, साथ ही शास्त्रीय तर्क (एलके बनाम एनके) के मामले में भी।<ref>{{harvnb|Gentzen|1934|p=191}}. "Die damit erreichte Symmetrie erweist sich als für die klassische Logik angemessener."</ref> फिर उन्होंने कहा कि इन कारणों के अलावा, कई उत्तरवर्ती सूत्रों के साथ अनुक्रमिक कलन विशेष रूप से उनके प्रमुख प्रमेय (हौप्त्सत्ज़) के लिए अभिप्रेत है।<ref>{{harvnb|Gentzen|1934|p=191}}. "Hiermit haben wir einige Gesichtspunkte zur Begründung der Aufstellung der folgenden Kalküle angegeben. Im wesentlichen ist ihre Form jedoch durch die Rücksicht auf den nachher zu beweisenden 'Hauptsatz' bestimmt und kann daher vorläufig nicht näher begründet werden."</ref>
+जेंटजन ने अपने एकल उत्पादन प्राकृतिक निगमन प्रणाली (NK और NJ) और उनके बहु- उत्पादन अनुक्रम कैलकुलस प्रणाली (LK और LJ) के बीच एक त्वरित्र अंतर पर बल दिया। उन्होंने लिखा है कि अंतर्ज्ञानवादी प्राकृतिक निगमन प्रणाली NJ कुछ कुरूप थी।<ref>{{harvnb|Gentzen|1934|p=188}}. "Der Kalkül ''NJ'' hat manche formale Unschönheiten."</ref> उन्होंने कहा कि मौलिक प्राकृतिक निगमन प्रणाली NK में बहिष्कृत मध्य के नियम की विशेष भूमिका को मौलिक अनुक्रम कैलकुलस प्रणाली LK में पदच्युत दिया गया है।<ref>{{harvnb|Gentzen|1934|p=191}}. "In dem klassischen Kalkül ''NK'' nahm der Satz vom ausgeschlossenen Dritten eine Sonderstellung unter den Schlußweisen ein [...], indem er sich der Einführungs- und Beseitigungssystematik nicht einfügte. Bei dem im folgenden anzugebenden logistischen klassichen Kalkül ''LK'' wird diese Sonderstellung aufgehoben."</ref> उन्होंने कहा कि अनुक्रमिक कलन LJ ने अंतर्ज्ञानवादी तर्क के स्थितियों में प्राकृतिक निगमन NJ की तुलना में अधिक समरूपता प्रदान की, और साथ ही मौलिक तर्क (LK विरुद्ध NK) के स्थितियों में भी प्राप्त की है।<ref>{{harvnb|Gentzen|1934|p=191}}. "Die damit erreichte Symmetrie erweist sich als für die klassische Logik angemessener."</ref> तब उन्होंने कहा कि इन कारणों के अतिरिक्त अनेक उत्तरवर्ती सूत्रों के साथ अनुक्रमिक कलन विशेष रूप से उनके प्रमुख प्रमेय (हॉपत्सत्ज़) के लिए अभिप्रेत है।<ref>{{harvnb|Gentzen|1934|p=191}}. "Hiermit haben wir einige Gesichtspunkte zur Begründung der Aufstellung der folgenden Kalküle angegeben. Im wesentlichen ist ihre Form jedoch durch die Rücksicht auf den nachher zu beweisenden 'Hauptsatz' bestimmt und kann daher vorläufig nicht näher begründet werden."</ref>
+=== अनुक्रम शब्द की उत्पत्ति ===
+अनुक्रम शब्द जेंटजन के 1934 के लेख्य में अनुक्रम शब्द से लिया गया है।<ref name=gentzen19341935 />[[स्टीफन कोल क्लेन]] अंग्रेजी में अनुवाद पर निम्नलिखित टिप्पणी करते हैं। जेंटजन ' अनुक्रम ' कहते हैं, जिसे हम 'अनुक्रम' के रूप में अनुवादित करते हैं क्योंकि हम ने पूर्व से ही वस्तुओं के अनुक्रम के लिए 'अनुक्रम' का उपयोग कर लिया हैं, जिस स्थान पर जर्मन 'फोल्गे' है।<ref>{{harvnb|Kleene|2002|p=441}}.</ref>
-=== शब्द अनुक्रम की उत्पत्ति ===
-अनुक्रम शब्द Gentzen के 1934 के पेपर में Sequenz शब्द से लिया गया है।<ref name=gentzen19341935 />[[स्टीफन कोल क्लेन]] अंग्रेजी में अनुवाद पर निम्नलिखित टिप्पणी करते हैं: जेंटजन 'सीक्वेंज' कहते हैं, जिसे हम 'अनुक्रम' के रूप में अनुवादित करते हैं, क्योंकि हम पहले से ही वस्तुओं के किसी भी उत्तराधिकार के लिए 'अनुक्रम' का उपयोग कर चुके हैं, जहां जर्मन 'फोल्गे' है।<ref>{{harvnb|Kleene|2002|p=441}}.</ref>
+== तार्किक सूत्र प्रमाणन ==
+[[File:Sequent calculus proof tree example.png|thumb|अनुक्रमिक कलन के अनुसार एक प्रमाण प्रकट करने की प्रक्रिया का वर्णन करने वाला एक मूल वाला ट्री   ]]
+=== रिडक्शन ट्री   ===
-== तार्किक सूत्र सिद्ध करना ==
+अनुक्रमिक कलन को [[विश्लेषणात्मक झांकी की विधि|विश्लेषणात्मक दृश्य की विधि]] के समान प्रस्तावपरक तर्क में सूत्र सिद्ध करने के लिए उपकरण के रूप में देखा जा सकता है। यह चरणों की एक श्रृंखला देता है जो तार्किक सूत्र को सरल और सरल सूत्रों को प्रमाणन करने की उपपाद्य विषय को कम करने की अनुमति देता है जब तक कि कोई साधारण नहीं हो जाता।<ref name = "Cornell09">[http://www.cs.cornell.edu/courses/cs4860/2009sp/lec-09.pdf Applied Logic, Univ. of Cornell: Lecture 9]. Last Retrieved: 2016-06-25</ref> निम्नलिखित सूत्र पर विचार करें-
-[[File:Sequent calculus proof tree example.png|thumb|अनुक्रमिक कलन द्वारा एक सबूत खोजने की प्रक्रिया का वर्णन करने वाला एक जड़ वाला पेड़]]
-=== कटौती के पेड़<!--'Reduction tree', 'Reduction trees', 'Inference line' and 'Inference lines' redirect here--> ===
-अनुक्रमिक कलन को [[विश्लेषणात्मक झांकी की विधि]] के समान, प्रस्तावपरक तर्क में सूत्र सिद्ध करने के लिए एक उपकरण के रूप में देखा जा सकता है। यह चरणों की एक श्रृंखला देता है जो एक तार्किक सूत्र को सरल और सरल सूत्रों को साबित करने की समस्या को कम करने की अनुमति देता है जब तक कि कोई तुच्छ नहीं हो जाता।<ref name = "Cornell09">[http://www.cs.cornell.edu/courses/cs4860/2009sp/lec-09.pdf Applied Logic, Univ. of Cornell: Lecture 9]. Last Retrieved: 2016-06-25</ref>
-निम्नलिखित सूत्र पर विचार करें:
 :<math>((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)</math>
-यह निम्नलिखित रूप में लिखा गया है, जहां सिद्ध करने की आवश्यकता वाले प्रस्ताव टर्नस्टाइल (प्रतीक) के दाईं ओर है <math>\vdash</math>:
+यह निम्नलिखित रूप में लिखा गया है, जिस स्थान पर सिद्ध करने की आवश्यकता वाले प्रस्ताव टर्नस्टाइल (प्रतीक) के दाईं ओर है <math>\vdash</math>:
 :<math>\vdash((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)</math>
-अब, इसे स्वयंसिद्धों से सिद्ध करने के बजाय, [[तार्किक परिणाम]] के आधार को मान लेना और फिर उसके निष्कर्ष को सिद्ध करने का प्रयास करना पर्याप्त है।<ref name=Wadler>"Remember, the way that you [[Proof (truth)|prove]]  an [[logical consequence|implication]] is by assuming the [[hypothesis]]."—[[Philip Wadler]], [https://www.youtube.com/watch?v=OGF-TGd-CIo&list=PLWbHc_FXPo2jB6IZ887vLXsPoympL3KEy&index=11 on 2 November 2015, in his  Keynote: "Propositions as Types". Minute 14:36 /55:28 of Code Mesh video clip ]</ref> इसलिए एक निम्नलिखित अनुक्रम में जाता है:
+अब इसे स्वयंसिद्धों से सिद्ध करने के अतिरिक्त [[तार्किक परिणाम]] के आधार को मान लेना और तब उसके निष्कर्ष को सिद्ध करने का प्रयास करना पर्याप्त है।<ref name=Wadler>"Remember, the way that you [[Proof (truth)|prove]]  an [[logical consequence|implication]] is by assuming the [[hypothesis]]."—[[Philip Wadler]], [https://www.youtube.com/watch?v=OGF-TGd-CIo&list=PLWbHc_FXPo2jB6IZ887vLXsPoympL3KEy&index=11 on 2 November 2015, in his  Keynote: "Propositions as Types". Minute 14:36 /55:28 of Code Mesh video clip ]</ref> इसलिए निम्नलिखित अनुक्रम में जाता है-
 :<math>(p\rightarrow r)\lor (q\rightarrow r)\vdash (p\land q)\rightarrow r</math>
-फिर से दाहिने हाथ की ओर एक निहितार्थ शामिल है, जिसका आधार आगे माना जा सकता है ताकि केवल इसके निष्कर्ष को सिद्ध करने की आवश्यकता हो:
+पुनः दाहिने हाथ की ओर निहितार्थ सम्मिलित है जिसका आधार आगे माना जा सकता है जिससे मात्र इसके निष्कर्ष को सिद्ध करने की आवश्यकता हो-
 :<math>(p\rightarrow r)\lor (q\rightarrow r), (p\land q)\vdash r</math>
-चूँकि बाईं ओर के तर्कों को [[तार्किक संयोजन]] द्वारा संबंधित माना जाता है, इसे निम्नलिखित द्वारा प्रतिस्थापित किया जा सकता है:
+चूँकि बाएं ओर के तर्कों को [[तार्किक संयोजन]] के अनुसार संबंधित माना जाता है, इसे निम्नलिखित के अनुसार प्रतिस्थापित किया जा सकता है-
 :<math>(p\rightarrow r)\lor (q\rightarrow r), p, q\vdash r</math>
-यह बाईं ओर के पहले तर्क पर तार्किक वियोग के दोनों मामलों में निष्कर्ष सिद्ध करने के बराबर है। इस प्रकार हम अनुक्रम को दो में विभाजित कर सकते हैं, जहाँ अब हमें प्रत्येक को अलग-अलग सिद्ध करना होगा:
+यह बाएं ओर के पूर्व तर्क पर संयोजन के दोनों स्थितियों में निष्कर्ष सिद्ध करने के बराबर है। इस प्रकार हम अनुक्रम को दो में विभाजित कर सकते हैं, जहाँ अब हमें प्रत्येक को प्रथक- प्रथक सिद्ध करना होगा-
 :<math>p\rightarrow r, p, q\vdash r</math>
 :<math>q\rightarrow r, p, q\vdash r</math>
-पहले फैसले के मामले में, हम फिर से लिखते हैं <math>p\rightarrow r</math> जैसा <math>\lnot p \lor r</math> और अनुक्रम को फिर से विभाजित करने के लिए विभाजित करें:
+पूर्व फैसले के स्थितियों में हम पुनः लिखते हैं <math>p\rightarrow r</math> जैसा <math>\lnot p \lor r</math> और अनुक्रम को पुनः विभाजित करके प्राप्त करें-
 :<math>\lnot p, p, q \vdash r</math>
 :<math>r, p, q \vdash r</math>
-दूसरा क्रम किया जाता है; पहले अनुक्रम को और सरल बनाया जा सकता है:
+द्वितीय क्रम किया जाता है; पूर्व अनुक्रम को और सरल बनाया जा सकता है-
 :<math>p, q \vdash p, r</math>
-इस प्रक्रिया को हमेशा तब तक जारी रखा जा सकता है जब तक कि प्रत्येक पक्ष में केवल परमाणु सूत्र न हों।
+इस प्रक्रिया को सदैव तब तक प्रचलित रखा जा सकता है जब तक कि प्रत्येक पक्ष में मात्र आणविक सूत्र न हों। इस प्रक्रिया को रेखांकन के रूप में [[वृक्ष (ग्राफ सिद्धांत)|ट्री ( रेखाचित्र सिद्धांत)]] के अनुसार वर्णित किया जा सकता है, जैसा कि दाईं ओर दर्शाया गया है। ट्री की मूल वह सूत्र है, जिसे हम सिद्ध करना चाहते हैं। पत्तियों में मात्र आणविक सूत्र होते हैं। ट्री को आभाव ट्री के रूप में उल्लिखित किया जाता है। <ref name = "Cornell09"/><ref name = "Tait">{{cite book| vauthors = Tait WW | title = Gentzen's Centenary: The Quest for Consistency |chapter= Gentzen's original consistency proof and the Bar Theorem |chapter-url= http://home.uchicago.edu/~wwtx/Gentzen.original.pdf | veditors = Kahle R, Rathjen M |pages= 213–228 |location= New York |publisher= Springer |year= 2010}}</ref> टर्नस्टाइल बायीं ओर की वस्तुओं को संयुग्मन के अनुसार जुड़ा हुआ समझा जाता है, और जो दायीं ओर विच्छेद के अनुसार जुड़ा हुआ है। इसलिए जब दोनों में मात्र आणविक प्रतीक होते हैं, तो अनुक्रम को स्वैच्छिक रूप से (और सदैव सत्य) स्वीकार किया जाता है यदि और मात्र दाईं ओर कम से कम एक प्रतीक भी बाएं ओर प्रदर्शित होता है।
-इस प्रक्रिया को रेखांकन के रूप में एक [[वृक्ष (ग्राफ सिद्धांत)]] द्वारा वर्णित किया जा सकता है, जैसा कि दाईं ओर दर्शाया गया है। वृक्ष की जड़ वह सूत्र है जिसे हम सिद्ध करना चाहते हैं; पत्तियों में केवल परमाणु सूत्र होते हैं। पेड़ को कमी पेड़ के रूप में जाना जाता है<!--boldface per WP:R#PLA-->.<ref name = "Cornell09"/><ref name = "Tait">{{cite book| vauthors = Tait WW | title = Gentzen's Centenary: The Quest for Consistency |chapter= Gentzen's original consistency proof and the Bar Theorem |chapter-url= http://home.uchicago.edu/~wwtx/Gentzen.original.pdf | veditors = Kahle R, Rathjen M |pages= 213–228 |location= New York |publisher= Springer |year= 2010}}</ref>
-घूमने वाले दरवाज़े के बायीं ओर की वस्तुओं को संयुग्मन द्वारा जुड़ा हुआ समझा जाता है, और जो दायीं ओर वियोग द्वारा जुड़ा हुआ है। इसलिए, जब दोनों में केवल परमाणु प्रतीक होते हैं, तो अनुक्रम को स्वैच्छिक रूप से (और हमेशा सत्य) स्वीकार किया जाता है यदि और केवल अगर दाईं ओर कम से कम एक प्रतीक भी बाईं ओर दिखाई देता है।
-निम्नलिखित नियम हैं जिनके द्वारा कोई व्यक्ति पेड़ के साथ आगे बढ़ता है। जब भी एक अनुक्रम को दो में विभाजित किया जाता है, ट्री वर्टेक्स में दो चाइल्ड वर्टिकल होते हैं, और ट्री शाखित होता है। इसके अतिरिक्त, प्रत्येक पक्ष में तर्कों के क्रम को स्वतंत्र रूप से बदला जा सकता है; Γ और Δ संभावित अतिरिक्त तर्कों के लिए खड़े हैं।<ref name = "Cornell09"/>
+निम्नलिखित नियम हैं, जिनके के अनुसार कोई एक ट्री के साथ आगे बढ़ता है। जब भी एक अनुक्रम को दो में विभाजित किया जाता है, ट्री वर्टेक्स में दो चाइल्ड वर्टिकल होते हैं, और ट्री शाखित होता है। इसके अतिरिक्त प्रत्येक पक्ष में तर्कों के क्रम को स्वतंत्र रूप से बदला जा सकता है। Γ और Δ संभावित अतिरिक्त तर्कों के लिए खंड हैं।<ref name = "Cornell09"/>
-प्राकृतिक कटौती के लिए जेंटजन-शैली के लेआउट में उपयोग की जाने वाली क्षैतिज रेखा के लिए सामान्य शब्द अनुमान रेखा है<!--boldface per WP:R#PLA-->.<ref>Jan von Plato, ''Elements of Logical Reasoning'', Cambridge University Press, 2014, p. 32.</ref>
+प्राकृतिक निगमन के लिए जेंटजन-शैली के विन्यास में उपयोग की जाने वाली क्षैतिज रेखा के लिए सामान्य शब्द अनुमान रेखा है। <ref>Jan von Plato, ''Elements of Logical Reasoning'', Cambridge University Press, 2014, p. 32.</ref>
 {| border="0" cellpadding="20" style="text-align:center"
@@ Line 139: / Line 133: @@
 |}
-प्रोपोज़िशनल लॉजिक में किसी भी सूत्र से शुरू करके, चरणों की एक श्रृंखला द्वारा, घूमने वाले दरवाज़े के दाईं ओर संसाधित किया जा सकता है जब तक कि इसमें केवल परमाणु प्रतीक शामिल न हों। फिर, बाईं ओर के लिए भी ऐसा ही किया जाता है। चूँकि प्रत्येक तार्किक संकारक ऊपर दिए गए नियमों में से एक में प्रकट होता है, और नियम द्वारा हटा दिया जाता है, जब कोई तार्किक संकारक नहीं रह जाता है तो प्रक्रिया समाप्त हो जाती है: सूत्र विघटित हो गया है।
+वक्‍तव्‍य कथन तर्क में किसी भी सूत्र से प्रारंभ करके चरणों की श्रृंखला के अनुसार टर्नस्टाइल दाईं ओर संसाधित किया जा सकता है। जब तक कि इसमें मात्र आणविक प्रतीक सम्मिलित न हों। तब बाएं ओर के लिए भी ऐसा ही किया जाता है। चूँकि प्रत्येक तार्किक संकारक ऊपर दिए गए नियमों में से एक में प्रकट होता है और नियम के अनुसार पदच्युत दिया जाता है। जब कोई तार्किक संकारक नहीं रह जाता है तो प्रक्रिया समाप्त हो जाती है। अब सूत्र विघटित हो गया है।
-इस प्रकार, पेड़ों की पत्तियों में अनुक्रमों में केवल परमाणु प्रतीक शामिल होते हैं, जो या तो स्वयंसिद्ध द्वारा सिद्ध होते हैं या नहीं, इसके अनुसार दाईं ओर के प्रतीकों में से एक बाईं ओर भी दिखाई देता है।
+इस प्रकार वृक्षों की पत्तियों में अनुक्रमों में मात्र आणविक प्रतीक सम्मिलित होते हैं जो स्वयंसिद्ध के अनुसार सिद्ध होते हैं अथवा नहीं। इसके अनुसार दाईं ओर के प्रतीकों में से एक बाएं ओर भी प्रदर्शित देता है।
-यह देखना आसान है कि पेड़ के चरण उनके द्वारा निहित सूत्रों के सिमेंटिक ट्रुथ वैल्यू को संरक्षित करते हैं, जब भी कोई विभाजन होता है तो पेड़ की विभिन्न शाखाओं के बीच संयोजन को समझा जाता है। यह भी स्पष्ट है कि एक अभिगृहीत सिद्ध होता है यदि और केवल यदि यह परमाणु प्रतीकों के सत्य मानों के प्रत्येक आबंटन के लिए सत्य है। इस प्रकार शास्त्रीय प्रस्तावपरक तर्क के लिए यह प्रणाली सु[[दृढ़ता]] और [[पूर्णता (तर्क)]] है।
+यह देखना सहज है कि, ट्री के चरण उनके के अनुसार निहित सूत्रों के वास्त्विकता अर्थ महत्व को संरक्षित करते हैं। जब भी कोई विभाजन होता है तो ट्री की विभिन्न शाखाओं के बीच संयोजन को समझा जाता है। यह भी स्पष्ट है कि अभिगृहीत सिद्ध होता है और मात्र यह आणविक प्रतीकों के सत्य मानों के प्रत्येक आबंटन के लिए सत्य है। इस प्रकार मौलिक प्रस्ताव परक तर्क के लिए यह प्रणाली सु[[दृढ़ता]] और [[पूर्णता (तर्क)]] है।
 === मानक स्वयंसिद्धीकरणों से संबंध ===
-सीक्वेंट कैलकुलस प्रोपोज़िशनल कैलकुलस के अन्य स्वयंसिद्धों से संबंधित है, जैसे कि फ़्रीज का प्रोपोज़ल कैलकुलस या प्रोपोज़िशनल कैलकुलस # उदाहरण 1। एक कमी का पेड़।
+अनुक्रम कैलकुलस वक्‍तव्‍य कथन कैलकुलस के अन्य स्वयंसिद्धों से संबंधित है जैसे कि स्थिर का प्रस्ताव कैलकुलस अथवा जान लुकासिविक्ज़ का स्वयंसिद्धीकरण (स्वयं मानक हिल्बर्ट प्रणाली का एक खंड ) है। प्रत्येक सूत्र जो इनमें सिद्ध किया जा सकता है में पराभव का ट्री है।
-इसे निम्न प्रकार से दिखाया जा सकता है: तर्कवाक्य कलन में प्रत्येक उपपत्ति केवल अभिगृहीतों और अनुमान नियमों का उपयोग करती है। स्वयंसिद्ध योजना का प्रत्येक उपयोग एक वास्तविक तार्किक सूत्र उत्पन्न करता है, और इस प्रकार अनुक्रमिक कलन में सिद्ध किया जा सकता है; इनके लिए उदाहरण अनुक्रमिक कैलकुस # उदाहरण व्युत्पन्न हैं। ऊपर वर्णित प्रणालियों में एकमात्र निष्कर्ष नियम मॉडस पोनेंस है, जिसे कट नियम द्वारा कार्यान्वित किया जाता है।
+इसे निम्न प्रकार से दिखाया जा सकता है। तर्कवाक्य कलन में प्रत्येक उपपत्ति मात्र अभिगृहीतों और अनुमान नियमों का उपयोग करती है। स्वयंसिद्ध योजना का प्रत्येक उपयोग वास्तविक तार्किक सूत्र उत्पन्न करता है, और इस प्रकार अनुक्रमिक कलन में सिद्ध किया जा सकता है। इनके लिए उदाहरण अनुक्रमिक कैलकुलस व्युत्पन्न हैं। ऊपर वर्णित प्रणालियों में एकमात्र निष्कर्ष नियम विधानात्मक हेतु फलानुमान है। जिसे परिवर्तन नियम के अनुसार कार्यान्वित किया जाता है।
-== सिस्टम एलके ==
+== प्रणाली LK ==
-यह खंड 1934 में जेंटजेन द्वारा पेश किए गए अनुक्रमिक कैलकुस एलके (लॉजिस्टिस कल्कुल के लिए खड़े) के नियमों का परिचय देता है। <ref>Andrzej-Indrzejczak, [https://link.springer.com/chapter/10.1007/978-3-030-57145-0_2 An Introduction to the Theory and Applications of Propositional Sequent Calculi] (2021, chapter "Gentzen's Sequent Calculus LK"). Accessed 3 August 2022.</ref>
+यह खंड 1934 में जेंटजेन के अनुसार प्रस्तुत किए गए अनुक्रमिक कैलकुलस LK ( तार्किक कल्कुल स्थिति) के नियमों का परिचय देता है। <ref>Andrzej-Indrzejczak, [https://link.springer.com/chapter/10.1007/978-3-030-57145-0_2 An Introduction to the Theory and Applications of Propositional Sequent Calculi] (2021, chapter "Gentzen's Sequent Calculus LK"). Accessed 3 August 2022.</ref> इस कैलकुलस में (औपचारिक) प्रमाण अनुक्रमों का क्रम है। जिस स्थान पर अनुक्रम में से प्रत्येक नीचे दिए गए अनुमान के नियम का उपयोग करके अनुक्रम में पूर्व प्रदर्शित अनुक्रमों से व्युत्पन्न होता है।
-इस कैलकुलस में ए (औपचारिक) प्रमाण अनुक्रमों का एक क्रम है, जहां अनुक्रम में से प्रत्येक नीचे दिए गए अनुमान के नियम का उपयोग करके अनुक्रम में पहले दिखाई देने वाले अनुक्रमों से व्युत्पन्न होता है।
 === अनुमान नियम ===
-निम्नलिखित नोटेशन का उपयोग किया जाएगा:
+निम्नलिखित टिप्पणी का उपयोग किया जाएगा-
-* <math>\vdash</math> टर्नस्टाइल (प्रतीक) के रूप में जाना जाता है, बाईं ओर की मान्यताओं को दाईं ओर के प्रस्तावों से अलग करता है
+* <math>\vdash</math> टर्नस्टाइल (प्रतीक) के रूप में उल्लिखित किया जाता है, और बाएं ओर की मान्यताओं को दाईं ओर के प्रस्तावों से प्रथक करता है।
-* <math>A</math> और <math>B</math> प्रथम-क्रम विधेय तर्क के सूत्रों को निरूपित करें (कोई इसे प्रस्तावपरक तर्क तक सीमित भी कर सकता है),
+* <math>A</math> और <math>B</math> प्रथम-क्रम विधेय तर्क के सूत्रों को निरूपित करता है(कोई इसे प्रस्तावपरक तर्क तक सीमित भी कर सकता है)।
-* <math>\Gamma, \Delta, \Sigma</math>, और <math>\Pi</math> सूत्रों के परिमित (संभवतः खाली) अनुक्रम हैं (वास्तव में, सूत्रों का क्रम मायने नहीं रखता; देखें {{slink||Structural rules}}), संदर्भ कहा जाता है,
+* <math>\Gamma, \Delta, \Sigma</math>, और <math>\Pi</math> सूत्रों के परिमित (संभवतः रिक्त ) अनुक्रम हैं (वास्तव में सूत्रों का क्रम प्रयोजन नहीं रखता; देखें {{slink||संरचनात्मक नियम}})। जिन्हें संदर्भ कहा जाता है।
-** जब बाईं ओर <math>\vdash</math>, सूत्रों के अनुक्रम को संयोजन के रूप में माना जाता है (सभी को एक ही समय में माना जाता है),
+** जब बाएं ओर <math>\vdash</math> सूत्रों के अनुक्रम को संयोजन के रूप में माना जाता है ( समस्त को एक ही समय धारण करने के लिए माना जाता है)।
-** जबकि के दाईं ओर <math>\vdash</math>, सूत्रों के अनुक्रम को वियोगात्मक रूप से माना जाता है (चर के किसी भी असाइनमेंट के लिए कम से कम एक सूत्र को धारण करना चाहिए),
+** यद्यपि दाईं ओर <math>\vdash</math> सूत्रों के अनुक्रम को वियोगात्मक रूप से माना जाता है (चर के किसी भी कार्य के लिए कम से कम एक सूत्र को धारण करना चाहिए)।
-* <math>t</math> एक मनमाना शब्द दर्शाता है,
+* <math>t</math> इच्छानुसार अवधि प्रकट करता है।
-* <math>x</math> और <math>y</math> चरों को निरूपित करें।
+* <math>x</math> और <math>y</math> चरों को निरूपित करता है।
-* एक चर को एक सूत्र के भीतर [[मुक्त चर और बाध्य चर]] कहा जाता है यदि यह क्वांटिफायर द्वारा बाध्य नहीं है <math>\forall</math> या <math>\exists</math>.
+* चर को एक सूत्र के अंतर्गत [[मुक्त चर और बाध्य चर|मुक्त]] होने के लिए कहा जाता है यदि यह परिमाणकों के अनुसार बाध्य नहीं है । <math>\forall</math> अथवा <math>\exists</math> अस्तित्व में है।
-* <math>A[t/x]</math> शब्द को प्रतिस्थापित करके प्राप्त सूत्र को दर्शाता है <math>t</math> चर की प्रत्येक मुक्त घटना के लिए <math>x</math> सूत्र में <math>A</math> प्रतिबंध के साथ कि शब्द <math>t</math> चर के लिए मुक्त होना चाहिए <math>x</math> में <math>A</math> (यानी, किसी भी चर की कोई घटना नहीं है <math>t</math> में बंध जाता है <math>A[t/x]</math>).
+* <math>A[t/x]</math> उस सूत्र को प्रकट करता है, जो सूत्र <math>A</math> में चर <math>x</math> की प्रत्येक मुक्त घटना के लिए शब्द <math>t</math> को प्रतिस्थापित करके प्राप्त किया जाता है, सूत्र में <math>A</math> इस प्रतिबंध के साथ कि शब्द <math>t</math> को <math>A</math> मे चर <math>x</math> के लिए मुक्त होना चाहिए ( अर्थात किसी भी चर की कोई घटना नहीं है) <math>t</math> में कोई भी चर <math>A[t/x]</math>) में बाध्य हो जाता है।
-* <math>WL</math>, <math>WR</math>, <math>CL</math>, <math>CR</math>, <math>PL</math>, <math>PR</math>: ये छह तीन संरचनात्मक नियमों में से प्रत्येक के दो संस्करणों के लिए खड़े हैं; a के बाईं ओर ('L') उपयोग के लिए एक <math>\vdash</math>, और दूसरा इसके दाईं ओर ('आर')। नियमों को कमजोर करने के लिए 'डब्ल्यू' (बाएं / दाएं), संकुचन के लिए 'सी' और क्रमचय के लिए 'पी' संक्षिप्त किया गया है।
+* <math>WL</math>, <math>WR</math>, <math>CL</math>, <math>CR</math>, <math>PL</math>, <math>PR</math> ये छह तीन संरचनात्मक नियमों में से प्रत्येक के दो संस्करणों के लिए खड़े हैं। एक a<math>\vdash</math> के बाएं ओर ('L') उपयोग के लिए और द्वितीय इसके दाईं ओर ('R') है। नियमों को अशक्त करने के लिए 'W' (बाएं / दाएं), संकुचन के लिए 'C' और क्रमचय के लिए 'P' संक्षिप्त किया गया है।
-ध्यान दें कि, ऊपर प्रस्तुत कटौती वृक्ष के साथ आगे बढ़ने के नियमों के विपरीत, निम्नलिखित नियम विपरीत दिशाओं में जाने के लिए हैं, स्वयंसिद्ध से प्रमेय तक। इस प्रकार वे उपरोक्त नियमों की सटीक दर्पण-छवियां हैं, सिवाय इसके कि यहां समरूपता को स्पष्ट रूप से ग्रहण नहीं किया गया है, और [[परिमाणक (तर्क)]] के संबंध में नियम जोड़े गए हैं।
+ध्यान दें कि, ऊपर प्रस्तुत रिडक्शन ट्री के साथ आगे बढ़ने के नियमों के विपरीत निम्नलिखित नियम विपरीत दिशाओं में जाने के लिए हैं, अथार्त स्वयंसिद्ध से प्रमेय तक। इस प्रकार वह उपरोक्त नियमों की त्रुटिहीन दर्पण-छवियां हैं। अतिरिक्त इसके कि यहां समरूपता को स्पष्ट रूप से ग्रहण नहीं किया गया है, और [[परिमाणक (तर्क)|परिमाणन (तर्क)]] के संबंध में नियम संकलित किये गए हैं।
 {| border="0" cellpadding="20" style="text-align:center"
 |-
-| Axiom:
+| स्वयंसिद्ध
-| Cut:
+| आभाव
 |-
 | style="background:#fafafa; border:1px #ccc solid;" |
@@ Line 184: / Line 177: @@
   </math>
 |-
-| Left logical rules:
+| बाएं तार्किक नियम
-| Right logical rules:
+| दाएं तार्किक नियम
 |-
 | style="background:#fafafa; border:1px #ccc solid;" |
@@ Line 244: / Line 237: @@
   </math>
 |-
-| Left structural rules:
+| बाएं संरचनात्मक नियम
-| Right structural rules:
+| दाएं संरचनात्मक नियम
 |-
 | style="background:#fafafa; border:1px #ccc solid;" |
@@ Line 274: / Line 267: @@
   </math>
 |}
-प्रतिबंध: नियमों में <math>({\forall}R)</math> और <math>({\exists}L)</math>, चर <math>y</math> संबंधित निचले अनुक्रमों में कहीं भी मुक्त नहीं होना चाहिए।
+प्रतिबंध: नियमों में <math>({\forall}R)</math> और <math>({\exists}L)</math> मे परिवर्तनीय <math>y</math> संबंधित निम्नतर अनुक्रमों में कहीं भी मुक्त नहीं होना चाहिए।
 === एक सहज व्याख्या ===
-उपरोक्त नियमों को दो प्रमुख समूहों में विभाजित किया जा सकता है: तार्किक और संरचनात्मक। प्रत्येक तार्किक नियम टर्नस्टाइल (प्रतीक) के बाईं ओर या दाईं ओर एक नया तार्किक सूत्र प्रस्तुत करता है। <math>\vdash</math>. इसके विपरीत, संरचनात्मक नियम सूत्रों के सटीक आकार की अनदेखी करते हुए अनुक्रमों की संरचना पर काम करते हैं। इस सामान्य योजना के दो अपवाद पहचान के स्वयंसिद्ध (I) और (कट) के नियम हैं।
+उपरोक्त नियमों को दो प्रमुख समूहों तार्किक और संरचनात्मक में विभाजित किया जा सकता है। प्रत्येक तार्किक नियम टर्नस्टाइल (प्रतीक) के बाएं ओर अथवा दाईं ओर एक नया तार्किक <math>\vdash</math> सूत्र प्रस्तुत करता है। इसके विपरीत संरचनात्मक नियम सूत्रों के त्रुटिहीन आकार की अनदेखी करते हुए अनुक्रमों की संरचना पर काम करते हैं। इस सामान्य योजना के दो अपवाद समानता के स्वयंसिद्ध (I) और ( परिवर्तन ) के नियम हैं।
-हालांकि एक औपचारिक तरीके से कहा गया है, उपरोक्त नियम शास्त्रीय तर्क के संदर्भ में बहुत सहज ज्ञान युक्त पढ़ने की अनुमति देते हैं। उदाहरण के लिए, नियम पर विचार करें <math>({\land}L_1)</math>. यह कहता है कि, जब भी कोई इसे साबित कर सकता है <math>\Delta</math> शामिल सूत्रों के कुछ अनुक्रम से निष्कर्ष निकाला जा सकता है <math>A</math>, तो कोई भी निष्कर्ष निकाल सकता है <math>\Delta</math> (मजबूत) धारणा से <math>A \land B</math> रखती है। इसी प्रकार, नियम <math>({\neg}R)</math> बताता है कि, अगर <math>\Gamma</math> और <math>A</math> निष्कर्ष निकालने के लिए पर्याप्त <math>\Delta</math>, फिर से <math>\Gamma</math> अकेला कोई भी अभी भी निष्कर्ष निकाल सकता है <math>\Delta</math> या <math>A</math> झूठा होना चाहिए, यानी <math>{\neg}A</math> रखती है। सभी नियमों की व्याख्या इस प्रकार की जा सकती है।
+चूंकि औपचारिक विधियों से कहा गया है कि उपरोक्त नियम मौलिक तर्क के संदर्भ में अति सहज ज्ञान युक्त अध्ययन की अनुमति देते हैं। उदाहरण के रूप मे नियम <math>({\land}L_1)</math> पर विचार करें । यह नियम कहता है कि, कोई इसे प्रमाणन कर सकता है और <math>\Delta</math> सूत्रों के कुछ अनुक्रम से निष्कर्ष निकाला जा सकता है इसमे सम्मिलित <math>A</math>, है तो कोई भी <math>\Delta</math> (दृढ़) निष्कर्ष निकाल सकता है। जो <math>A \land B</math> धारण करता है। इसी प्रकार नियम <math>({\neg}R)</math> बताता है कि, <math>\Gamma</math> और <math>A</math> <math>\Delta</math> को समाप्त करने के लिए पर्याप्त हैं, तो <math>\Gamma</math> अकेले से या तो अभी भी <math>\Delta</math> से निष्कर्ष निकाल सकता है अथवा <math>A</math> अवास्तविक होना चाहिए, अर्थात <math>{\neg}A</math> अधिकार रखता है। समस्त नियमों की व्याख्या इस प्रकार की जा सकती है।
-क्वांटिफायर नियमों के बारे में अंतर्ज्ञान के लिए, नियम पर विचार करें <math>({\forall}R)</math>. बेशक यह निष्कर्ष निकाला <math>\forall{x} A</math> केवल इस तथ्य से है <math>A[y/x]</math> सच है सामान्य तौर पर संभव नहीं है। यदि, हालांकि, चर y का कहीं और उल्लेख नहीं किया गया है (अर्थात इसे अभी भी अन्य सूत्रों को प्रभावित किए बिना स्वतंत्र रूप से चुना जा सकता है), तो कोई यह मान सकता है कि <math>A[y/x]</math> y के किसी भी मान के लिए धारण करता है। अन्य नियम तब बहुत सीधे होने चाहिए।
+परिमाणकों नियमों के संबंध में अंतर्ज्ञान के लिए नियम <math>({\forall}R)</math> पर विचार करें । निस्संदेह यह निष्कर्ष निकाला <math>\forall{x} A</math> मात्र इस तथ्य से अधिकार रखता है कि <math>A[y/x]</math> सत्य है किन्तु यह सामान्य रूप पर संभव नहीं है। चूंकि चर y का कहीं और उल्लेख नहीं किया गया है (अर्थात इसे अभी भी अन्य सूत्रों को प्रभावित किए नियमबद्ध स्वतंत्र रूप से चयनित जा सकता है), तो कोई यह मान सकता है कि <math>A[y/x]</math> y के किसी भी मान के लिए है। अन्य नियम तब अति प्रत्यक्ष होने चाहिए।
-नियमों को विधेय तर्क में कानूनी व्युत्पत्तियों के विवरण के रूप में देखने के बजाय, उन्हें किसी दिए गए कथन के प्रमाण के निर्माण के निर्देश के रूप में भी माना जा सकता है। इस मामले में नियमों को नीचे से ऊपर तक पढ़ा जा सकता है; उदाहरण के लिए, <math>({\land}R)</math> कहते हैं, यह साबित करने के लिए <math>A \land B</math> धारणाओं से चलता है <math>\Gamma</math> और <math>\Sigma</math>, यह साबित करने के लिए काफी है <math>A</math> से निष्कर्ष निकाला जा सकता है <math>\Gamma</math> और <math>B</math> से निष्कर्ष निकाला जा सकता है <math>\Sigma</math>, क्रमश। ध्यान दें कि, कुछ पूर्ववृत्त दिए जाने पर, यह स्पष्ट नहीं है कि इसे कैसे विभाजित किया जाए <math>\Gamma</math> और <math>\Sigma</math>. हालाँकि, केवल बहुत सी संभावनाएँ जाँची जा सकती हैं क्योंकि धारणा द्वारा पूर्ववर्ती परिमित है। यह यह भी दर्शाता है कि कैसे प्रूफ थ्योरी को कॉम्बिनेटरियल फैशन में प्रूफ पर काम करने के रूप में देखा जा सकता है: दोनों के लिए दिए गए प्रूफ <math>A</math> और <math>B</math>, कोई इसके लिए एक प्रमाण बना सकता है <math>A \land B</math>.
+नियमों को विधेय तर्क में नियमबद्ध व्युत्पत्तियों के विवरण के रूप में देखने के अतिरिक्त उन्हें किसी दिए गए कथन प्रमाण के निर्माण निर्देश के रूप में भी माना जा सकता है। इस स्थितियों में नियमों को नीचे से ऊपर तक अध्ययन जा सकता है। उदाहरण के रूप मे <math>({\land}R)</math> के द्वारा इसे प्रमाणन करने के लिए <math>A \land B</math> धारणाओं <math>\Gamma</math> और <math>\Sigma</math> से अनुसरण करता है, यह प्रमाणन करने के लिए पर्याप्त है कि <math>A</math> और <math>\Gamma</math> से निष्कर्ष निकाला जा सकता है, और <math>B</math> को क्रमश <math>\Sigma</math> से निष्कर्ष निकाला जा सकता है। ध्यान दें कि कुछ पूर्ववृत्त दिए जाने पर यह स्पष्ट नहीं है कि इसे <math>\Gamma</math> और <math>\Sigma</math> कैसे विभाजित किया जाए। चूंकि मात्र अति संभावनाएँ निस्र्द्ध जा सकती हैं, क्योंकि धारणा के अनुसार पूर्ववर्ती परिमित है। यह यह भी प्रकट करता है कि कैसे प्रमाण सिद्धांत को मिश्रित प्रचलन में प्रमाण के रूप में देखा जा सकता है। <math>A</math> और <math>B</math> दोनों के लिए प्रमाण दिए गए है, कोई भी <math>A \land B</math> के लिए प्रमाण बना सकता है।
-कुछ सबूत की तलाश करते समय, अधिकांश नियम यह करने के तरीके के बारे में कम या ज्यादा प्रत्यक्ष व्यंजनों की पेशकश करते हैं। कट का नियम अलग है: यह बताता है कि, जब कोई सूत्र <math>A</math> निष्कर्ष निकाला जा सकता है और यह सूत्र अन्य कथनों के समापन के लिए एक आधार के रूप में भी काम कर सकता है, फिर सूत्र <math>A</math> काटा जा सकता है और संबंधित व्युत्पत्तियों में शामिल हो गए हैं। प्रूफ बॉटम-अप का निर्माण करते समय, यह अनुमान लगाने की समस्या पैदा करता है <math>A</math> (चूंकि यह नीचे बिल्कुल नहीं दिखता है)। कट-एलिमिनेशन प्रमेय इस प्रकार स्वचालित कटौती में अनुक्रम कलन के अनुप्रयोगों के लिए महत्वपूर्ण है: यह बताता है कि कट नियम के सभी उपयोगों को एक प्रमाण से समाप्त किया जा सकता है, जिसका अर्थ है कि किसी भी सिद्ध अनुक्रम को कट-फ्री प्रमाण दिया जा सकता है।
+कुछ प्रमाण की खोज करते समय अधिकांश नियम यह करने के विधियों के संबंध में कम अथवा ज्यादा प्रत्यक्ष व्यंजनों की प्रस्तुति करते हैं। परिवर्तन का नियम प्रथक है। यह बताता है कि, जब कोई सूत्र <math>A</math> का निष्कर्ष निकाला जा सकता है और यह सूत्र अन्य कथनों के समापन के लिए आधार के रूप में भी काम कर सकता है। तब सूत्र <math>A</math> समाप्त करा जा सकता है और संबंधित व्युत्पत्तियों में सम्मिलित हो गया हैं। नीचे से ऊपर का निर्माण करते समय यह <math>A</math> अनुमान लगाने की उपपाद्य विषय उत्पन्न करता है (चूंकि यह नीचे कदाचित नहीं दिखता है)। परिवर्तन उन्मूलन प्रमेय इस प्रकार स्वचालित निगमन में अनुक्रम कलन के अनुप्रयोगों के लिए महत्वपूर्ण है। यह बताता है कि परिवर्तन नियम के समस्त उपयोगों को प्रमाण से समाप्त किया जा सकता है, जिसका अर्थ है कि किसी भी सिद्ध अनुक्रम को परिवर्तन - स्वतंत्र प्रमाण दिया जा सकता है।
-दूसरा नियम जो कुछ विशेष है वह पहचान का स्वयंसिद्ध (I) है। इसका सहज ज्ञान स्पष्ट है: प्रत्येक सूत्र स्वयं को सिद्ध करता है। कट नियम की तरह, पहचान का स्वयंसिद्ध कुछ हद तक बेमानी है: [[परमाणु प्रारंभिक अनुक्रमों की पूर्णता]] बताती है कि नियम को किसी भी नुकसान के बिना [[परमाणु सूत्र]]ों तक सीमित किया जा सकता है।
+द्वितीय नियम जो कुछ विशेष है वह समानता का स्वयंसिद्ध (I) है। इसका सहज ज्ञान स्पष्ट है। प्रत्येक सूत्र स्वयं को सिद्ध करता है। परिवर्तन नियम की प्रकार, समानता का स्वयंसिद्ध कुछ स्तर तक निरर्थक है। [[परमाणु प्रारंभिक अनुक्रमों की पूर्णता|आणविक प्रारंभिक अनुक्रमों की पूर्णता]] वर्णन करती है कि नियम को किसी भी हानि के नियमबद्ध [[परमाणु सूत्र|आणविक सू]]त्र तकों सीमित किया जा सकता है।
-ध्यान दें कि निहितार्थ के नियमों को छोड़कर, सभी नियमों में दर्पण साथी होते हैं। यह इस तथ्य को दर्शाता है कि प्रथम-क्रम तर्क की सामान्य भाषा में संयोजी द्वारा निहित नहीं है शामिल नहीं है <math>\not\leftarrow</math> यह निहितार्थ का डी मॉर्गन दोहरा होगा। इस तरह के संयोजन को अपने प्राकृतिक नियमों के साथ जोड़ने से कलन पूरी तरह से बाएँ-दाएँ सममित हो जाएगा।
+ध्यान दें कि निहितार्थ के नियमों को छोड़कर समस्त नियमों में दर्पण साथी होते हैं। यह इस तथ्य को प्रकट करता है कि, प्रथम-क्रम तर्क की सामान्य भाषा में संयोजक के अनुसार निहित नहीं है अथवा सम्मिलित नहीं है। संयोजी <math>\not\leftarrow</math> जो निहितार्थ का डी मॉर्गन द्विवचन होगा। इस प्रकार के संयोजन को अपने प्राकृतिक नियमों के साथ संयोजन से कलन पूर्ण प्रकार से बाएँ-दाएँ सममित हो जाएगा।
 === उदाहरण व्युत्पत्ति ===
-यहाँ की व्युत्पत्ति है<math> \vdash A \lor \lnot A </math>, जाना जाता है
+यहाँ <math> \vdash A \lor \lnot A </math> की व्युत्पत्ति है। जिसे अपवर्जित मध्य का नियम के रूप मे विदित है (लैटिन में टर्शियम नॉन डाटूर)।
-बहिष्कृत मध्य का नियम (लैटिन में टर्शियम नॉन डाटूर)।
 {| align=center border=0 cellspacing=0 cellpadding=0
 |-
@@ Line 362: / Line 354: @@
 | &nbsp;
 |}
-अगला एक साधारण तथ्य का प्रमाण है जिसमें क्वांटिफायर शामिल हैं। ध्यान दें कि आक्षेप सत्य नहीं है, और इसकी असत्यता को नीचे-ऊपर व्युत्पन्न करने का प्रयास करते समय देखा जा सकता है, क्योंकि नियमों में प्रतिस्थापन में मौजूदा मुक्त चर का उपयोग नहीं किया जा सकता है <math>(\forall R)</math> और <math>(\exists L)</math>.
+आगामी एक साधारण तथ्य का प्रमाण है जिसमें परिमाणकों सम्मिलित हैं। ध्यान दें कि आक्षेप सत्य नहीं है, और इसकी असत्यता को नीचे-ऊपर व्युत्पन्न करने का प्रयास करते समय देखा जा सकता है। क्योंकि नियमों <math>(\forall R)</math> और <math>(\exists L)</math> में प्रतिस्थापन में वर्तमान मुक्त चर का उपयोग नहीं किया जा सकता है।
 {| align=center border=0 cellspacing=0 cellpadding=0
 |-
@@ Line 419: / Line 411: @@
 | &nbsp;
 |}
-कुछ और दिलचस्प के लिए हम साबित करेंगे <math>{\left( \left( A \rightarrow \left( B \lor C \right) \right) \rightarrow \left( \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \rightarrow \lnot A \right) \right)}</math>. व्युत्पत्ति का पता लगाना सीधा है, जो स्वचालित साबित करने में एलके की उपयोगिता को दर्शाता है।
+कुछ और रोचक के लिए हम <math>{\left( \left( A \rightarrow \left( B \lor C \right) \right) \rightarrow \left( \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \rightarrow \lnot A \right) \right)}</math> प्रमाणन करेंगे। व्युत्पत्ति का ज्ञात करना प्रत्यक्ष है, जो स्वचालित प्रमाणन करने में LK की सार्थकता को प्रकट करता है।
 {| align=center border=0 cellspacing=0 cellpadding=0
 |-
@@ Line 630: / Line 622: @@
 |}
 |}
-|
+ये व्युत्पत्ति अनुक्रमिक कलन की दृढ़ता औपचारिक संरचना पर भी बल देती हैं। उदाहरण के रूप मे ऊपर परिभाषित तार्किक नियम टर्नस्टाइल के समीप सूत्र पर कार्य करते हैं, जैसे कि क्रमचय नियम आवश्यक हैं। चूंकि ध्यान दें कि यह जेंटज़ेन की मूल शैली में प्रस्तुति का एक खंड है। सामान्य सरलीकरण में एक स्पष्ट क्रमपरिवर्तन नियम की आवश्यकता को समाप्त करते हुए अनुक्रम के अतिरिक्त अनुक्रम की व्याख्या में सूत्रों के [[ multiset |मल्टी सेट]] का उपयोग सम्मिलित है। यह अनुक्रम कलन के बाह्य अनुमान और व्युत्पत्तियों की क्रमविनिमेयता को स्थानांतरित करने के अनुरूप है। यद्यपि LK इसे प्रणाली के अंतर्गत ही अंतः स्थापित करता है।
-| रोस्पान = 2 वैलिग्न = नीचे | <math>
-      (\rightarrow L)
-    </math>
-|-
-| संरेखित करें = केंद्र शैली = 'बॉर्डर-टॉप: 1 पीएक्स ठोस काला;' रोस्पान = 2 | <math>
-      \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) , \left( A \rightarrow \left( B \lor C \right) \right) \vdash \lnot A , \lnot A
-    </math>
-|
-|-
-|
-| रोस्पान = 2 | <math>
-      (CR)
-    </math>
-|-
-| संरेखित करें = केंद्र शैली = 'बॉर्डर-टॉप: 1 पीएक्स ठोस काला;' रोस्पान = 2 | <math>
-      \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) , \left( A \rightarrow \left( B \lor C \right) \right) \vdash \lnot A
-    </math>
-|
-|-
-|
-| रोस्पान = 2 | <math>
-      (PL)
-    </math>
-|-
-| संरेखित करें = केंद्र शैली = 'बॉर्डर-टॉप: 1 पीएक्स ठोस काला;' रोस्पान = 2 | <math>
-      \left( A \rightarrow \left( B \lor C \right) \right) , \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \vdash \lnot A
-    </math>
-|
-|-
-|
-| रोस्पान = 2 | <math>
-      (\rightarrow R)
-    </math>
-|-
-| संरेखित करें = केंद्र शैली = 'बॉर्डर-टॉप: 1 पीएक्स ठोस काला;' रोस्पान = 2 | <math>
-      \left( A \rightarrow \left( B \lor C \right) \right) \vdash \left( \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \rightarrow \lnot A \right)
-    </math>
-|
-|-
-|
-| रोस्पान = 2 | <math>
-      (\rightarrow R)
-    </math>
-|-
-| संरेखित करें = केंद्र शैली = 'बॉर्डर-टॉप: 1 पीएक्स ठोस काला;' रोस्पान = 2 | <math>
-      \vdash \left( \left( A \rightarrow \left( B \lor C \right) \right) \rightarrow \left( \left( \left( B \rightarrow \lnot A \right) \land \lnot C \right) \rightarrow \lnot A \right) \right)
-    </math>
-|
-|-
-|
-|
-|}
-ये व्युत्पत्ति अनुक्रमिक कलन की सख्त औपचारिक संरचना पर भी जोर देती हैं। उदाहरण के लिए, ऊपर परिभाषित तार्किक नियम हमेशा घूमने वाले दरवाज़े से सटे सूत्र पर कार्य करते हैं, जैसे कि क्रमचय नियम आवश्यक हैं। हालाँकि, ध्यान दें कि यह जेंटज़ेन की मूल शैली में प्रस्तुति का एक हिस्सा है। एक सामान्य सरलीकरण में एक स्पष्ट क्रमपरिवर्तन नियम की आवश्यकता को समाप्त करते हुए अनुक्रम के बजाय अनुक्रम की व्याख्या में सूत्रों के [[ multiset ]] का उपयोग शामिल है। यह अनुक्रम कलन के बाहर मान्यताओं और व्युत्पत्तियों की कम्यूटेटिविटी को स्थानांतरित करने के अनुरूप है, जबकि एलके इसे सिस्टम के भीतर ही एम्बेड करता है।
-=== विश्लेषणात्मक झांकी से संबंध ===
-अनुक्रमिक कैलकुस के कुछ फॉर्मूलेशन (यानी वेरिएंट) के लिए, इस तरह के कैलकुस में एक प्रमाण विश्लेषणात्मक झांकी के उल्टा, बंद विधि के लिए आइसोमोर्फिक है।<ref>{{harvnb|Smullyan|1995|p=107}}</ref>
-=== संरचनात्मक नियम ===
-संरचनात्मक नियम कुछ अतिरिक्त चर्चा के पात्र हैं।
-कमजोर करना (डब्ल्यू) मनमाना तत्वों को [[अनुक्रम]] में जोड़ने की अनुमति देता है। सहज रूप से, पूर्ववर्ती में इसकी अनुमति है क्योंकि हम हमेशा अपने प्रमाण के दायरे को सीमित कर सकते हैं (यदि सभी कारों में पहिए हैं, तो यह कहना सुरक्षित है कि सभी काली कारों में पहिए हैं); और उत्तरवर्ती में क्योंकि हम हमेशा वैकल्पिक निष्कर्ष की अनुमति दे सकते हैं (यदि सभी कारों में पहिए हैं, तो यह कहना सुरक्षित है कि सभी कारों में पहिए या पंख होते हैं)।
+=== विश्लेषणात्मक चित्र से संबंध ===
+अनुक्रमिक कैलकुलस के कुछ सूत्रीकरण (अर्थात रूपांतर) के लिए इस प्रकार के कैलकुलस में निम्म प्रमाण, संवृत विश्लेषणात्मक उत्क्रम विधि के लिए समरूप है।<ref>{{harvnb|Smullyan|1995|p=107}}</ref>
+=== संरचनात्मक नियम                                                                                                        ===
-संकुचन (सी) और क्रमचय (पी) आश्वस्त करते हैं कि अनुक्रम के तत्वों के न तो आदेश (पी) और न ही घटनाओं की बहुलता (सी) मायने रखती है। इस प्रकार, अनुक्रमों के बजाय [[सेट (गणित)]] पर भी विचार किया जा सकता है।
+संरचनात्मक नियम कुछ अतिरिक्त परिचर्चा के पात्र हैं।
-हालाँकि, अनुक्रमों का उपयोग करने का अतिरिक्त प्रयास उचित है क्योंकि भाग या सभी संरचनात्मक नियमों को छोड़ा जा सकता है। ऐसा करने से, तथाकथित [[अवसंरचनात्मक तर्क]] प्राप्त होता है।
+अशक्त (W) इच्छानुसार तत्वों को [[अनुक्रम]] में संयोजन की अनुमति देता है। सहज रूप से पूर्ववर्ती में इसकी अनुमति है, क्योंकि हम सदैव अपने प्रमाण के सीमा को सीमित कर सकते हैं (यदि समस्त कारों में पहिए हैं, तो यह कहना सुरक्षित है कि समस्त काली कारों में पहिए हैं)। और उत्तरवर्ती में क्योंकि हम सदैव वैकल्पिक निष्कर्ष की अनुमति दे सकते हैं (यदि समस्त कारों में पहिए हैं तो यह कहना सुरक्षित है कि समस्त कारों में पहिए अथवा पंख होते हैं)।
-=== सिस्टम एलके === के गुण
+संकुचन (C) और क्रमचय (P) आश्वस्त करते हैं कि, अनुक्रम के तत्वों के न तो आदेश (P) और न ही घटनाओं की बहुलता (C) प्रयोजन रखती है। इस प्रकार अनुक्रमों के अतिरिक्त [[सेट (गणित)|समुच्चय (गणित)]] पर भी विचार किया जा सकता है।
-नियमों की इस प्रणाली को प्रथम-क्रम तर्क के संबंध में सुदृढ़ता और पूर्णता (तर्क) दोनों के रूप में दिखाया जा सकता है, अर्थात एक कथन <math>A</math> परिसर के एक सेट से शब्दार्थ का अनुसरण करता है <math>\Gamma</math> <math>(\Gamma \vDash A)</math> [[अगर और केवल अगर]] अनुक्रम <math>\Gamma \vdash A</math> उपरोक्त नियमों द्वारा प्राप्त किया जा सकता है।<ref>{{harvnb|Kleene|2002|p=336}}, wrote in 1967 that "it was a major logical discovery by Gentzen 1934–5 that, when there is any (purely logical) proof of a proposition, there is a direct proof. The implications of this discovery are in theoretical logical investigations, rather than in building collections of proved formulas."</ref>
+चूंकि अनुक्रमों का उपयोग करने का अतिरिक्त प्रयास उचित है क्योंकि खंड अथवा समस्त संरचनात्मक नियमों को त्यागा जा सकता है। ऐसा करने से तथाकथित [[अवसंरचनात्मक तर्क]] प्राप्त होता है।
-अनुक्रमिक कलन में, [[कट-उन्मूलन]] का नियम। इस परिणाम को Gentzen's Hauptsatz (मुख्य प्रमेय) के रूप में भी जाना जाता है।<ref name=curry_cut_elimination /><ref name=kleene_cut_elimination />
+=== प्रणाली LK के गुण ===
+नियमों की इस प्रणाली को प्रथम-क्रम तर्क के संबंध में सुदृढ़ता और पूर्णता (तर्क) दोनों के रूप में दिखाया जा सकता है, अर्थात कथन <math>A</math> परिसर के एक समुच्चय से शब्दार्थ का अनुसरण करता है। <math>\Gamma</math> <math>(\Gamma \vDash A)</math> [[अगर और केवल अगर|यदि और मात्र]] अनुक्रम <math>\Gamma \vdash A</math> उपरोक्त नियमों के अनुसार प्राप्त किया जा सकता है।<ref>{{harvnb|Kleene|2002|p=336}}, wrote in 1967 that "it was a major logical discovery by Gentzen 1934–5 that, when there is any (purely logical) proof of a proposition, there is a direct proof. The implications of this discovery are in theoretical logical investigations, rather than in building collections of proved formulas."</ref> अनुक्रमिक कलन में [[कट-उन्मूलन|परिवर्तन -उन्मूलन]] का नियमस्वीकार्य है। इस परिणाम को जेंटजन हॉपट॒सत्ज़ (मुख्य प्रमेय) के रूप में भी उल्लिखित है।<ref name="curry_cut_elimination" /><ref name="kleene_cut_elimination" />
+== रूपांतर ==
-== वेरिएंट ==
+उपरोक्त नियमों को विभिन्न विधियों से संशोधित किया जा सकता है:
-उपरोक्त नियमों को विभिन्न तरीकों से संशोधित किया जा सकता है:
+=== लघु संरचनात्मक विकल्प ===
-=== मामूली संरचनात्मक विकल्प ===
+अनुक्रमों और संरचनात्मक नियमों को कैसे औपचारिक रूप दिया जाता है, इसके तकनीकी विवरण के संबंध में विकल्प की स्वतंत्रता है। जब तक LK में प्रत्येक व्युत्पत्ति प्रभावी रूप से नए नियमों का उपयोग करके व्युत्पत्ति में परिवर्तित हो सकती है, और इसके विपरीत संशोधित नियमों को अभी भी LK कहा जा सकता है।
-अनुक्रमों और संरचनात्मक नियमों को कैसे औपचारिक रूप दिया जाता है, इसके तकनीकी विवरण के बारे में पसंद की कुछ स्वतंत्रता है। जब तक एलके में प्रत्येक व्युत्पत्ति प्रभावी रूप से नए नियमों का उपयोग करके व्युत्पत्ति में परिवर्तित हो सकती है और इसके विपरीत, संशोधित नियमों को अभी भी एलके कहा जा सकता है।
+सबसे पूर्व जैसा कि ऊपर उल्लेख किया गया है, अनुक्रमों को समुच्चय अथवा बहु- समुच्चय से संमिश्रित देखा जा सकता है। इस स्थितियों में अनुमत करने के नियम और (समुच्चय का उपयोग करते समय) अनुबंध सूत्र अप्रचलित हैं।
-सबसे पहले, जैसा कि ऊपर उल्लेख किया गया है, अनुक्रमों को सेट या मल्टीसेट से मिलकर देखा जा सकता है। इस मामले में, अनुमत करने के नियम और (सेट का उपयोग करते समय) अनुबंध सूत्र अप्रचलित हैं।
+अशक्त नियम स्वीकार्य हो जाएगा, जब स्वयंसिद्ध (I) को प्रवर्तित दिया जाता है। जैसे कि <math>\Gamma , A \vdash A , \Delta</math> रूप का अनुक्रम निष्कर्ष निकाला जा सकता है। इस का अर्थ है कि <math>A</math> सिद्ध होता है। किसी भी संदर्भ में <math>A</math> व्युत्पत्ति में प्रदर्शित देने वाली कोई भी निर्बलता प्रारंभ में ही सही की जा सकती है। प्रमाण को नीचे से ऊपर बनाते समय यह एक सुविधाजनक परिवर्तन हो सकता है।
-कमजोर करने का नियम स्वीकार्य हो जाएगा, जब स्वयंसिद्ध (I) को बदल दिया जाता है, जैसे कि रूप का कोई अनुक्रम <math>\Gamma , A \vdash A , \Delta</math> निष्कर्ष निकाला जा सकता है। इस का मतलब है कि <math>A</math> को सिद्ध करता <math>A</math> किसी भी संदर्भ में। व्युत्पत्ति में दिखाई देने वाली कोई भी कमजोरी शुरुआत में ही सही की जा सकती है। प्रूफ़ को नीचे से ऊपर बनाते समय यह एक सुविधाजनक परिवर्तन हो सकता है।
+इनमें से स्वतंत्र नियमों के अंतर्गत संदर्भों को विभाजित करने के विधियों को प्रवर्तित सकता है। स्थितियों में <math>({\land}R), ({\lor}L)</math>, और <math>({\rightarrow}L)</math> वाम संदर्भ किस <math>\Gamma</math> और <math>\Sigma</math> मे विभाजित होता है। चूंकि संकुचन इनके दोहराव की अनुमति देता है, कोई यह मान सकता है, कि व्युत्पत्ति की दोनों शाखाओं में पूर्ण संदर्भ का उपयोग किया जाता है। ऐसा करने से यह सुनिश्चित होता है कि कोई भी महत्वपूर्ण परिसर त्रुटिपूर्ण उपखंड में लुप्त न हो जाए। संदर्भ के अप्रासंगिक खंडो को अशक्त करके उपरांत में समाप्त किया जा सकता है।
-इनमें से स्वतंत्र भी नियमों के भीतर संदर्भों को विभाजित करने के तरीके को बदल सकता है: मामलों में <math>({\land}R), ({\lor}L)</math>, और <math>({\rightarrow}L)</math> वाम संदर्भ किसी तरह विभाजित है <math>\Gamma</math> और <math>\Sigma</math> ऊपर जाने पर। चूंकि संकुचन इनके दोहराव की अनुमति देता है, कोई यह मान सकता है कि व्युत्पत्ति की दोनों शाखाओं में पूर्ण संदर्भ का उपयोग किया जाता है। ऐसा करने से, यह सुनिश्चित होता है कि कोई भी महत्वपूर्ण परिसर गलत शाखा में खो न जाए। कमजोर पड़ने का उपयोग करके, संदर्भ के अप्रासंगिक भागों को बाद में समाप्त किया जा सकता है।
+=== असंगति ===
+एक स्वयंसिद्ध के साथ ⊥ असत्य का प्रतिनिधित्व करने वाले [[विस्फोट का सिद्धांत|असंगति स्थिरांक]] को प्रस्तुत कर सकता है-
-=== बेतुकापन ===
-कोई परिचय दे सकता है <math>\bot</math>, स्वयंसिद्ध के साथ झूठे प्रतिनिधित्व वाले [[विस्फोट का सिद्धांत]]:
 :<math>
    \cfrac{}{\bot \vdash \quad }
 </math>
-या यदि, जैसा कि ऊपर वर्णित है, कमजोर करना एक स्वीकार्य नियम है, तो स्वयंसिद्ध के साथ:
+अथवा जैसा कि ऊपर वर्णित है, अशक्त करना स्वीकार्य नियम है, तो स्वयंसिद्ध के साथ-
 :<math>
    \cfrac{}{\Gamma, \bot \vdash \Delta}
 </math>
-साथ <math>\bot</math>परिभाषा के माध्यम से, निषेध को निहितार्थ के एक विशेष मामले के रूप में शामिल किया जा सकता है <math>(\neg A) \iff (A \to \bot)</math>.
+परिभाषा <math>(\neg A) \iff (A \to \bot)</math> के माध्यम से <math>\bot</math> निषेध को निहितार्थ के एक विशेष स्थितियों के रूप में सम्मिलित किया जा सकता है।
 === अवसंरचनात्मक तर्क ===
-{{main article|Substructural logic}}
+{{main article|अवसंरचनात्मक तर्क}}
-वैकल्पिक रूप से, कोई कुछ संरचनात्मक नियमों के उपयोग को प्रतिबंधित या प्रतिबंधित कर सकता है। यह विभिन्न प्रकार के अवसंरचनात्मक तर्क प्रणालियों का उत्पादन करता है। वे आम तौर पर एलके से कमजोर होते हैं (यानी, उनके पास कम प्रमेय होते हैं), और इस प्रकार प्रथम-क्रम तर्क के मानक शब्दों के संबंध में पूर्ण नहीं होते हैं। हालांकि, उनके पास अन्य रोचक गुण हैं जो सैद्धांतिक [[कंप्यूटर विज्ञान]] और कृत्रिम बुद्धि में अनुप्रयोगों के लिए प्रेरित हुए हैं।
+वैकल्पिक रूप से कोई कुछ संरचनात्मक नियमों के उपयोग को प्रतिबंधित अथवा प्रतिबंधित कर सकती है। यह विभिन्न प्रकार के अवसंरचनात्मक तर्क प्रणालियों का उत्पादन करता है। वह सामान्यतः LK से अशक्त होते हैं (अर्थात कम प्रमेय), और इस प्रकार प्रथम-क्रम तर्क के मानक शब्दों के संबंध में पूर्ण नहीं होते हैं। चूंकि उनके पास अन्य रोचक गुण हैं जो सैद्धांतिक [[कंप्यूटर विज्ञान]] और कृत्रिम सुचना में अनुप्रयोगों के लिए प्रेरित हुए हैं।
-===अंतर्ज्ञानी अनुक्रम कलन: सिस्टम एलजे ===
+===अंतर्ज्ञानी अनुक्रम कलन: प्रणाली LJ ===
-आश्चर्यजनक रूप से, एलके के नियमों में कुछ छोटे बदलाव इसे अंतर्ज्ञानवादी तर्क के लिए एक प्रमाण प्रणाली में बदलने के लिए पर्याप्त हैं।<ref>{{harvnb|Gentzen|1934|p=194}}, wrote: "Der Unterschied zwischen ''intuitionistischer'' und ''klassischer'' Logik ist bei den Kalkülen ''LJ'' und ''LK'' äußerlich ganz anderer Art als bei ''NJ'' und ''NK''. Dort bestand er in Weglassung bzw. Hinzunahme des Satzes vom ausgeschlossenen Dritten, während er hier durch die Sukzedensbedingung ausgedrückt wird." English translation: "The difference between ''intuitionistic'' and ''classical'' logic is in the case of the calculi ''LJ'' and ''LK'' of an extremely, totally different kind to the case of ''NJ'' and ''NK''. In the latter case, it consisted of the removal or addition respectively of the excluded middle rule, whereas in the former case, it is expressed through the succedent conditions."</ref> इसके लिए, किसी को दाहिनी ओर अधिक से अधिक एक सूत्र वाले अनुक्रमों तक सीमित करना होगा, और इस अपरिवर्तनीय को बनाए रखने के लिए नियमों को संशोधित करना होगा। उदाहरण के लिए, <math>({\lor}L)</math> निम्नानुसार सुधार किया गया है (जहाँ C एक मनमाना सूत्र है):
+आश्चर्यजनक रूप से LK के नियमों में कुछ छोटे बदलाव इसे अंतर्ज्ञानवादी तर्क के लिए प्रमाण प्रणाली में बदलने के लिए पर्याप्त हैं।<ref>{{harvnb|Gentzen|1934|p=194}}, wrote: "Der Unterschied zwischen ''intuitionistischer'' und ''klassischer'' Logik ist bei den Kalkülen ''LJ'' und ''LK'' äußerlich ganz anderer Art als bei ''NJ'' und ''NK''. Dort bestand er in Weglassung bzw. Hinzunahme des Satzes vom ausgeschlossenen Dritten, während er hier durch die Sukzedensbedingung ausgedrückt wird." English translation: "The difference between ''intuitionistic'' and ''classical'' logic is in the case of the calculi ''LJ'' and ''LK'' of an extremely, totally different kind to the case of ''NJ'' and ''NK''. In the latter case, it consisted of the removal or addition respectively of the excluded middle rule, whereas in the former case, it is expressed through the succedent conditions."</ref> इसके लिए किसी को दाहिनी ओर अधिक से अधिक एक सूत्र वाले अनुक्रमों तक सीमित करना होगा, और इस अपरिवर्तनीय को बनाए रखने के लिए नियमों को संशोधित करना होगा। उदाहरण के रूप मे <math>({\lor}L)</math> निम्नानुसार सुधार किया गया है (जहाँ C इच्छानुसार सूत्र है)।
 :<math>
    \cfrac{\Gamma, A \vdash C \qquad \Sigma, B \vdash C }{\Gamma, \Sigma, A \lor B \vdash C} \quad ({\lor}L)
 </math>
-परिणामी प्रणाली को एलजे कहा जाता है। यह अंतर्ज्ञानवादी तर्क के संबंध में ध्वनि और पूर्ण है और एक समान कट-उन्मूलन प्रमाण को स्वीकार करता है। इसका उपयोग [[संयोजन और अस्तित्व गुण]]ों को साबित करने में किया जा सकता है।
+परिणामी प्रणाली को LJ कहा जाता है। यह अंतर्ज्ञानवादी तर्क के संबंध में ध्वनि और पूर्ण है और एक समान परिवर्तन -उन्मूलन प्रमाण को स्वीकार करता है। इसका उपयोग [[संयोजन और अस्तित्व गुण]] को प्रमाणन करने में किया जा सकता है।
+वास्तव में LK में एकमात्र नियम जिसे एकल-सूत्र परिणामों तक सीमित करने की आवश्यकता है वह हैं <math>({\to}R)</math> <math>(\neg R)</math> (जिसे ऊपर वर्णित {<math>{\to}R</math> ऊपर विशेष स्थितियों के रूप में देखा जा सकता है) और <math>({\forall}R)</math> बहु-सूत्र परिणामों को वियोजन के रूप में व्याख्यायित किया जाता है, तो LK के अन्य सभी निष्कर्ष नियम LJ में व्युत्पन्न होते हैं, जबकि नियम <math>({\to}R)</math> और <math>({\forall}R)</math> बन जाते हैं
-वास्तव में, एलके में एकमात्र नियम जिसे एकल-सूत्र परिणामों तक सीमित करने की आवश्यकता है <math>({\to}R)</math>, <math>(\neg R)</math> (जिसे एक विशेष मामले के रूप में देखा जा सकता है <math>{\to}R</math>, जैसा कि ऊपर बताया गया है) और <math>({\forall}R)</math>. जब बहु-सूत्र परिणामों को विच्छेदन के रूप में व्याख्यायित किया जाता है, तो LK के अन्य सभी निष्कर्ष नियम LJ में व्युत्पन्न होते हैं, जबकि नियम <math>({\to}R)</math> और <math>({\forall}R)</math> बनना
 :<math>
    \cfrac{\Gamma, A \vdash B \lor C}{\Gamma \vdash (A \to B) \lor C}
 </math>
-और जब <math>y</math> नीचे के क्रम में मुक्त नहीं होता है)
+और जब <math>y</math> नीचे के क्रम में मुक्त नहीं होता है
 :<math>
    \cfrac{\Gamma \vdash A[y/x] \lor C}{\Gamma \vdash (\forall x A) \lor C}.
@@ Line 761: / Line 694: @@
 * [[नेस्टेड अनुक्रम कलन]]
 * [[संकल्प (तर्क)]]
-* सबूत सिद्धांत
+* प्रमाण सिद्धांत
 ==टिप्पणियाँ==
@@ Line 785: / Line 718: @@
 * [http://scienceblogs.com/goodmath/2006/07/17/a-brief-diversion-sequent-calc/ A Brief Diversion: Sequent Calculus]
 * [http://logitext.mit.edu/logitext.fcgi/tutorial Interactive tutorial of the Sequent Calculus]
-[[Category: सबूत सिद्धांत]] [[Category: तार्किक गणना]] [[Category: स्वचालित प्रमेय साबित करना]]
-[[Category: Machine Translated Page]]
+[[Category:Articles with hatnote templates targeting a nonexistent page]]
 [[Category:Created On 18/05/2023]]
+[[Category:Lua-based templates]]
+[[Category:Machine Translated Page]]
+[[Category:Pages that use a deprecated format of the math tags]]
+[[Category:Pages with script errors]]
+[[Category:Templates Vigyan Ready]]
+[[Category:Templates that add a tracking category]]
+[[Category:Templates that generate short descriptions]]
+[[Category:Templates using TemplateData]]
+[[Category:तार्किक गणना]]
+[[Category:सबूत सिद्धांत]]
+[[Category:स्वचालित प्रमेय साबित करना]]

Anonymous

Search

अनुक्रमिक गणना: Difference between revisions

Latest revision as of 16:56, 12 June 2023

अवलोकन

हिल्बर्ट-शैली निगमन प्रणाली

प्राकृतिक निगमन प्रणाली

अनुक्रमिक कैलकुलस सिस्टम

प्राकृतिक निगमन और अनुक्रमिक कलन के बीच का अंतर

अनुक्रम शब्द की उत्पत्ति

तार्किक सूत्र प्रमाणन

रिडक्शन ट्री

मानक स्वयंसिद्धीकरणों से संबंध

प्रणाली LK

अनुमान नियम

एक सहज व्याख्या

उदाहरण व्युत्पत्ति

विश्लेषणात्मक चित्र से संबंध

संरचनात्मक नियम

प्रणाली LK के गुण

रूपांतर

लघु संरचनात्मक विकल्प

असंगति

अवसंरचनात्मक तर्क

अंतर्ज्ञानी अनुक्रम कलन: प्रणाली LJ

यह भी देखें

टिप्पणियाँ

संदर्भ

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories