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

Revision as of 13:01, 23 May 2023

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

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

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

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

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

अवलोकन

प्रमाण सिद्धांत और गणितीय तर्क में, अनुक्रमिक कलन औपचारिक प्रणालियों का एक परिवार है जो अनुमान की एक निश्चित शैली और कुछ औपचारिक गुणों को साझा करता है। प्रथम अनुक्रमिक गणना प्रणाली, एलके और एलजे, 1934/1935 में गेरहार्ड जेंटजन के अनुसार प्रस्तुत की गई थी।^[1] प्रथम-क्रम तर्क (क्रमशः शास्त्रीय तर्क और अंतर्ज्ञानवादी तर्क संस्करणों में) में प्राकृतिक निगमन का अध्ययन करने के लिए एक उपकरण के रूप में। एलके और एलजे के बारे में जेंटजन का तथाकथित मुख्य प्रमेय ( हॉपट॒सत्ज़ ) परिवर्तन -उन्मूलन प्रमेय था,^[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}

(कम से कम एक असत्य है, या बीएस में से एक सत्य है)

या रूप में

\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})

(ऐसा नहीं हो सकता कि सभी एअइस सत्य हैं और सभी बीएस असत्य हैं)।

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

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

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

जेंटजन ने अपने एकल- उत्पादन प्राकृतिक निगमन प्रणाली (एनके और एनजे) और उनके बहु- उत्पादन अनुक्रम अश्म सिस्टम (एलके और एलजे) के बीच एक त्वरित्र अंतर पर बल दिया। उन्होंने लिखा है कि अंतर्ज्ञानवादी प्राकृतिक निगमन प्रणाली एनजे कुछ कुरूप थी।^[15] उन्होंने कहा कि शास्त्रीय प्राकृतिक निगमन प्रणाली एनके में बहिष्कृत मध्य के कानून की विशेष भूमिका को शास्त्रीय अनुक्रम अश्म प्रणाली एलके में पदच्युत दिया गया है।^[16] उन्होंने कहा कि अनुक्रमिक कलन एलजे ने अंतर्ज्ञानवादी तर्क के मामले में प्राकृतिक निगमन एनजे की तुलना में अधिक समरूपता प्रदान की, साथ ही शास्त्रीय तर्क (एलके बनाम एनके) के मामले में भी।^[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$

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

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

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

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

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

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

सिस्टम एलके

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

अनुमान नियम

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

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

		$(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

| | रोस्पान = 2 वैलिग्न = नीचे | $(\rightarrow L)$ |- | संरेखित करें = केंद्र शैली = 'बॉर्डर-टॉप: 1 पीएक्स ठोस काला;' रोस्पान = 2 | $\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$ | |- | | रोस्पान = 2 | $(CR)$ |- | संरेखित करें = केंद्र शैली = 'बॉर्डर-टॉप: 1 पीएक्स ठोस काला;' रोस्पान = 2 | $\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(A\rightarrow \left(B\lor C\right)\right)\vdash \lnot A$ | |- | | रोस्पान = 2 | $(PL)$ |- | संरेखित करें = केंद्र शैली = 'बॉर्डर-टॉप: 1 पीएक्स ठोस काला;' रोस्पान = 2 | $\left(A\rightarrow \left(B\lor C\right)\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A$ | |- | | रोस्पान = 2 | $(\rightarrow R)$ |- | संरेखित करें = केंद्र शैली = 'बॉर्डर-टॉप: 1 पीएक्स ठोस काला;' रोस्पान = 2 | $\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)$ | |- | | रोस्पान = 2 | $(\rightarrow R)$ |- | संरेखित करें = केंद्र शैली = 'बॉर्डर-टॉप: 1 पीएक्स ठोस काला;' रोस्पान = 2 | $\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)$ | |- | | |}

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

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

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

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

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

अदृढ़ करना (डब्ल्यू) मनमाना तत्वों को अनुक्रम में जोड़ने की अनुमति देता है। सहज रूप से, पूर्ववर्ती में इसकी अनुमति है क्योंकि हम सदैव अपने प्रमाण के दायरे को सीमित कर सकते हैं (यदि सभी कारों में पहिए हैं, तो यह कहना सुरक्षित है कि सभी काली कारों में पहिए हैं); और उत्तरवर्ती में क्योंकि हम सदैव वैकल्पिक निष्कर्ष की अनुमति दे सकते हैं (यदि सभी कारों में पहिए हैं, तो यह कहना सुरक्षित है कि सभी कारों में पहिए या पंख होते हैं)।

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

हालाँकि, अनुक्रमों का उपयोग करने का अतिरिक्त प्रयास उचित है क्योंकि भाग या सभी संरचनात्मक नियमों को छोड़ा जा सकता है। ऐसा करने से, तथाकथित अवसंरचनात्मक तर्क प्राप्त होता है।

=== सिस्टम एलके === के गुण

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

वेरिएंट

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

मामूली संरचनात्मक विकल्प

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

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

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

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

बेतुकापन

कोई परिचय दे सकता है $\bot$ , स्वयंसिद्ध के साथ झूठे प्रतिनिधित्व वाले विस्फोट का सिद्धांत:

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

या यदि, जैसा कि ऊपर वर्णित है, अदृढ़ करना एक स्वीकार्य नियम है, तो स्वयंसिद्ध के साथ:

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

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

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

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

अंतर्ज्ञानी अनुक्रम कलन: सिस्टम एलजे

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

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

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

वास्तव में, एलके में एकमात्र नियम जिसे एकल-सूत्र परिणामों तक सीमित करने की आवश्यकता है $({\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]

@@ Line 9: / Line 9: @@
 दूसरे शब्दों में, प्राकृतिक     निगमन और अनुक्रमिक कलन प्रणालियाँ विशेष रूप से विशिष्ट प्रकार की जेंटजन-शैली प्रणालियाँ हैं। हिल्बर्ट-शैली प्रणालियों में आमतौर पर   अति  कम संख्या में अनुमान नियम होते हैं, जो [[स्वयंसिद्ध]] के सेट पर अधिक निर्भर करते हैं। जेंटजन-शैली प्रणालियों में आमतौर पर   अति  कम स्वयं सिद्ध होते हैं, यदि कोई हो, तो नियमों के सेट पर अधिक निर्भर करते हैं।
-हिल्बर्ट-शैली प्रणालियों की तुलना में जेंटजन-शैली प्रणालियों के महत्वपूर्ण व्यावहारिक और सैद्धांतिक लाभ हैं। उदाहरण के लिए, दोनों प्राकृतिक     निगमन और अनुक्रमिक कलन प्रणालियाँ सार्वभौमिक और अस्तित्वगत [[परिमाणीकरण (तर्क)]] के उन्मूलन और परिचय की सुविधा प्रदान करती हैं ताकि प्रस्तावात्मक कलन के   अति  सरल नियमों के अनुसार अगणित तार्किक अभिव्यक्तियों में परिवर्तन किया जा सके। एक विशिष्ट तर्क में,   परिमाणकों को समाप्त कर दिया जाता है, फिर [[प्रस्तावक गणना]] को   अपरिमित   अभिव्यक्ति (जिसमें आमतौर पर   स्वतंत्र   परिवर्तनशील  होते हैं) पर लागू किया जाता है, और फिर   परिमाणकों को     पुनः      प्रस्तुत किया जाता है। यह   अति    स्तर  तक उस तरीके से   अनुकूल    होता  है जिसमें गणितज्ञों    के अनुसार  अभ्यास में गणितीय प्रमाणों का प्रयोग किया जाता है। विधेय कलन प्रमाण आमतौर पर इस दृष्टिकोण के साथ    प्रकट करने  में   अति  आसान होते हैं, और अक्सर छोटे होते हैं। प्राकृतिक निगमन प्रणालियाँ व्यावहारिक प्रमेय सिद्ध करने के लिए अधिक अनुकूल हैं। सैद्धांतिक विश्लेषण के लिए अनुक्रमिक कलन प्रणाली अधिक अनुकूल हैं।
+हिल्बर्ट-शैली प्रणालियों की तुलना में जेंटजन-शैली प्रणालियों के महत्वपूर्ण व्यावहारिक और सैद्धांतिक लाभ हैं। उदाहरण के लिए, दोनों प्राकृतिक     निगमन और अनुक्रमिक कलन प्रणालियाँ सार्वभौमिक और अस्तित्वगत [[परिमाणीकरण (तर्क)]] के उन्मूलन और परिचय की सुविधा प्रदान करती हैं ताकि प्रस्तावात्मक कलन के   अति  सरल नियमों के अनुसार अगणित तार्किक अभिव्यक्तियों में परिवर्तन किया जा सके। एक विशिष्ट तर्क में,   परिमाणकों को समाप्त कर दिया जाता है, फिर [[प्रस्तावक गणना]] को   अपरिमित   अभिव्यक्ति (जिसमें आमतौर पर   स्वतंत्र   परिवर्तनशील  होते हैं) पर लागू किया जाता है, और फिर   परिमाणकों को     पुनः      प्रस्तुत किया जाता है। यह   अति    स्तर  तक उस तरीके से   अनुकूल    होता  है जिसमें गणितज्ञों    के अनुसार  अभ्यास में गणितीय प्रमाणों का प्रयोग किया जाता है। विधेय कलन प्रमाण आमतौर पर इस दृष्टिकोण के साथ    प्रकट करने  में   अति      सहज  होते हैं, और अक्सर छोटे होते हैं। प्राकृतिक निगमन प्रणालियाँ व्यावहारिक प्रमेय सिद्ध करने के लिए अधिक अनुकूल हैं। सैद्धांतिक विश्लेषण के लिए अनुक्रमिक कलन प्रणाली अधिक अनुकूल हैं।
 == अवलोकन ==
-[[सबूत सिद्धांत|प्रमाण  सिद्धांत]] और गणितीय तर्क में, अनुक्रमिक कलन औपचारिक प्रणालियों का एक परिवार है जो अनुमान की एक निश्चित शैली और कुछ औपचारिक गुणों को साझा करता है।    प्रथम  अनुक्रमिक गणना प्रणाली, एलके और एलजे, 1934/1935 में गेरहार्ड जेंटजन    के अनुसार     प्रस्तुत  की गई थी।<ref name=gentzen19341935>{{harvnb|Gentzen|1934}}, {{harvnb|Gentzen|1935}}.</ref> प्रथम-क्रम तर्क (क्रमशः [[शास्त्रीय तर्क]] और [[अंतर्ज्ञानवादी तर्क]] संस्करणों में) में प्राकृतिक     निगमन का अध्ययन करने के लिए एक उपकरण के रूप में। एलके और एलजे के बारे में    जेंटजन  का तथाकथित मुख्य प्रमेय (   हॉपट॒सत्ज़ )    [[कट-उन्मूलन प्रमेय|परिवर्तन -उन्मूलन प्रमेय]] था,<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> और उनसे संबंधित सामान्य अवधारणाओं को प्रमाण सिद्धांत, गणितीय तर्क और [[स्वचालित कटौती|स्वचालित     निगमन]] के क्षेत्र में व्यापक रूप से लागू किया गया है।
+[[सबूत सिद्धांत|प्रमाण  सिद्धांत]] और गणितीय तर्क में, अनुक्रमिक कलन औपचारिक प्रणालियों का एक परिवार है जो अनुमान की एक निश्चित शैली और कुछ औपचारिक गुणों को साझा करता है।    प्रथम  अनुक्रमिक गणना प्रणाली, एलके और एलजे, 1934/1935 में गेरहार्ड जेंटजन    के अनुसार     प्रस्तुत  की गई थी।<ref name=gentzen19341935>{{harvnb|Gentzen|1934}}, {{harvnb|Gentzen|1935}}.</ref> प्रथम-क्रम तर्क (क्रमशः [[शास्त्रीय तर्क]] और [[अंतर्ज्ञानवादी तर्क]] संस्करणों में) में प्राकृतिक     निगमन का अध्ययन करने के लिए एक उपकरण के रूप में। एलके और एलजे के बारे में    जेंटजन  का तथाकथित मुख्य प्रमेय (   हॉपट॒सत्ज़ )    [[कट-उन्मूलन प्रमेय|परिवर्तन -उन्मूलन प्रमेय]] था,<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> प्रथम-क्रम तर्क (या जो भी तर्क     निगमन प्रणाली पर लागू होता है, उदाहरण के लिए, प्रस्तावपरक कलन या उच्च-क्रम तर्क या एक    [[मॉडल तर्क|प्रतिरूप  तर्क]]) का कोई भी सुव्यवस्थित सूत्र है। प्रमेय वे सूत्र हैं जो एक वैध प्रमाण में अंतिम निर्णय के रूप में प्रकट होते हैं। एक हिल्बर्ट-शैली प्रणाली को सूत्रों और निर्णयों के बीच कोई अंतर करने की आवश्यकता नहीं है; हम यहां    मात्र  बाद के मामलों की तुलना के लिए एक बनाते हैं।
@@ Line 54: / Line 54: @@
 (ऐसा नहीं हो सकता कि सभी एअइस सत्य हैं और सभी बीएस असत्य हैं)।
-इन     परिणाम में,     चक्र द्वार  दोनों ओर के सूत्रों के बीच एकमात्र अंतर यह है कि एक पक्ष को     अस्वीकार करा गया है। इस प्रकार, एक क्रम में बाएं से दाएं की     परिवर्तन सभी घटक सूत्रों को     अस्वीकार के अनुरूप है। इसका     अर्थ यह है कि एक समरूपता जैसे डी मॉर्गन के कानून, जो सिमेंटिक स्तर पर खुद को तार्किक निषेध के रूप में प्रकट करते हैं, अनुक्रमों के बाएं-दाएं समरूपता में सीधे अनुवाद करते हैं- और वास्तव में, संयोजन (∧) से निपटने के लिए अनुक्रमिक कलन में निष्कर्ष नियम संयोजन (∨) से निपटने वालों की दर्पण छवियां  है।
+इन     परिणाम में,     चक्र द्वार  दोनों ओर के सूत्रों के बीच एकमात्र अंतर यह है कि एक पक्ष को     अस्वीकार करा गया है। इस प्रकार, एक क्रम में बाएं से दाएं की     परिवर्तन सभी घटक सूत्रों को     अस्वीकार के अनुरूप है। इसका     अर्थ यह है कि एक समरूपता जैसे डी मॉर्गन के कानून, जो     अर्थ स्तर पर खुद को तार्किक निषेध के रूप में प्रकट करते हैं, अनुक्रमों के बाएं-दाएं समरूपता में सीधे अनुवाद करते हैं- और वास्तव में, संयोजन (∧) से निपटने के लिए अनुक्रमिक कलन में निष्कर्ष नियम संयोजन (∨) से निपटने वालों की दर्पण छवियां  है।
 कई तर्कशास्त्री     अनुभव   करते हैं  कि यह सममित प्रस्तुति    प्रमाण  प्रणाली की अन्य शैलियों की तुलना में तर्क की संरचना में     गहन   अंतर्दृष्टि प्रदान करती है, जहां नियमों में नकारात्मकता का शास्त्रीय द्वंद्व उतना स्पष्ट नहीं है।
@@ Line 60: / Line 60: @@
 === प्राकृतिक     निगमन और अनुक्रमिक कलन के बीच का अंतर ===
-जेंटजन ने अपने एकल-    उत्पादन   प्राकृतिक     निगमन प्रणाली (एनके और एनजे) और उनके बहु-    उत्पादन   सीक्वेंट     अश्म   सिस्टम (एलके और एलजे) के बीच एक     त्वरित्र   अंतर पर     बल   दिया। उन्होंने लिखा है कि अंतर्ज्ञानवादी प्राकृतिक     निगमन प्रणाली एनजे कुछ     कुरूप   थी।<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>
+जेंटजन ने अपने एकल-    उत्पादन   प्राकृतिक     निगमन प्रणाली (एनके और एनजे) और उनके बहु-    उत्पादन       अनुक्रम      अश्म   सिस्टम (एलके और एलजे) के बीच एक     त्वरित्र   अंतर पर     बल   दिया। उन्होंने लिखा है कि अंतर्ज्ञानवादी प्राकृतिक     निगमन प्रणाली एनजे कुछ     कुरूप   थी।<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>
@@ Line 88: / Line 88: @@
 :<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> चक्र द्वार  बायीं ओर की वस्तुओं को संयुग्मन    के अनुसार  जुड़ा हुआ समझा जाता है, और जो दायीं ओर     विच्छेद         के अनुसार  जुड़ा हुआ है। इसलिए, जब दोनों में    मात्र  परमाणु प्रतीक होते हैं, तो अनुक्रम को स्वैच्छिक रूप से (और    सदैव सत्य) स्वीकार किया जाता है यदि और    मात्र   दाईं ओर कम से कम एक प्रतीक भी बाईं ओर दिखाई देता है।
+इस प्रक्रिया को    सदैव तब तक जारी रखा जा सकता है जब तक कि प्रत्येक पक्ष में    मात्र  परमाणु सूत्र न हों। इस प्रक्रिया को रेखांकन के रूप में एक [[वृक्ष (ग्राफ सिद्धांत)|वृक्ष (    रेखाचित्र      सिद्धांत)]]    के अनुसार  वर्णित किया जा सकता है, जैसा कि दाईं ओर दर्शाया गया है। वृक्ष की जड़ वह सूत्र है जिसे हम सिद्ध करना चाहते हैं; पत्तियों में    मात्र  परमाणु सूत्र होते हैं।     वृक्ष    को     आभाव     वृक्ष    के रूप में जाना जाता है.<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"/>
 प्राकृतिक     निगमन के लिए जेंटजन-शैली के     विन्यास  में उपयोग की जाने वाली क्षैतिज रेखा के लिए सामान्य शब्द अनुमान रेखा है.<ref>Jan von Plato, ''Elements of Logical Reasoning'', Cambridge University Press, 2014, p. 32.</ref>
@@ Line 135: / Line 135: @@
 |}
-वक्‍तव्‍य कथन      तर्क में किसी भी सूत्र से शुरू करके, चरणों की एक श्रृंखला    के अनुसार ,     चक्र द्वार  दाईं ओर संसाधित किया जा सकता है जब तक कि इसमें    मात्र  परमाणु प्रतीक शामिल न हों। फिर, बाईं ओर के लिए भी ऐसा ही किया जाता है। चूँकि प्रत्येक तार्किक संकारक ऊपर दिए गए नियमों में से एक में प्रकट होता है, और नियम    के अनुसार  हटा दिया जाता है, जब कोई तार्किक संकारक नहीं रह जाता है तो प्रक्रिया समाप्त हो जाती है: सूत्र विघटित हो गया है।
+वक्‍तव्‍य कथन      तर्क में किसी भी सूत्र से शुरू करके, चरणों की एक श्रृंखला    के अनुसार ,     चक्र द्वार  दाईं ओर संसाधित किया जा सकता है जब तक कि इसमें    मात्र  परमाणु प्रतीक शामिल न हों। फिर, बाईं ओर के लिए भी ऐसा ही किया जाता है। चूँकि प्रत्येक तार्किक संकारक ऊपर दिए गए नियमों में से एक में प्रकट होता है, और नियम    के अनुसार      पदच्युत दिया जाता है, जब कोई तार्किक संकारक नहीं रह जाता है तो प्रक्रिया समाप्त हो जाती है: सूत्र विघटित हो गया है।
-इस प्रकार, पेड़ों की पत्तियों में अनुक्रमों में    मात्र  परमाणु प्रतीक शामिल होते हैं, जो या तो स्वयंसिद्ध    के अनुसार  सिद्ध होते हैं या नहीं, इसके अनुसार दाईं ओर के प्रतीकों में से एक बाईं ओर भी दिखाई देता है।
+इस प्रकार,     वृक्षों की पत्तियों में अनुक्रमों में    मात्र  परमाणु प्रतीक शामिल होते हैं, जो या तो स्वयंसिद्ध    के अनुसार  सिद्ध होते हैं या नहीं, इसके अनुसार दाईं ओर के प्रतीकों में से एक बाईं ओर भी     प्रदर्शित देता है।
-यह देखना आसान है कि     वृक्ष    के चरण उनके    के अनुसार  निहित सूत्रों के सिमेंटिक ट्रुथ वैल्यू को संरक्षित करते हैं, जब भी कोई विभाजन होता है तो     वृक्ष    की विभिन्न शाखाओं के बीच संयोजन को समझा जाता है। यह भी स्पष्ट है कि एक अभिगृहीत सिद्ध होता है यदि और    मात्र  यदि यह परमाणु प्रतीकों के सत्य मानों के प्रत्येक आबंटन के लिए सत्य है। इस प्रकार शास्त्रीय प्रस्तावपरक तर्क के लिए यह प्रणाली सु[[दृढ़ता]] और [[पूर्णता (तर्क)]] है।
+यह देखना     सहज  है कि     वृक्ष    के चरण उनके    के अनुसार  निहित सूत्रों के    वास्त्विकता  अर्थ       महत्व को संरक्षित करते हैं, जब भी कोई विभाजन होता है तो     वृक्ष    की विभिन्न शाखाओं के बीच संयोजन को समझा जाता है। यह भी स्पष्ट है कि एक अभिगृहीत सिद्ध होता है यदि और    मात्र  यदि यह परमाणु प्रतीकों के सत्य मानों के प्रत्येक आबंटन के लिए सत्य है। इस प्रकार शास्त्रीय प्रस्तावपरक तर्क के लिए यह प्रणाली सु[[दृढ़ता]] और [[पूर्णता (तर्क)]] है।
 === मानक स्वयंसिद्धीकरणों से संबंध ===
-सीक्वेंट     अश्म       वक्‍तव्‍य कथन      अश्म   के अन्य स्वयंसिद्धों से संबंधित है, जैसे कि फ़्रीज का प्रोपोज़ल     अश्म   या     वक्‍तव्‍य कथन      अश्म   # उदाहरण 1। एक     आभाव का     वृक्ष   ।
+अनुक्रम      अश्म       वक्‍तव्‍य कथन      अश्म के अन्य स्वयंसिद्धों से संबंधित है, जैसे कि     स्थिर  का     प्रस्ताव  कैलकुलस या जान लुकासिविक्ज़ का     स्वयंसिद्धीकरण  (स्वयं मानक हिल्बर्ट सिस्टम का एक     खंड ): प्रत्येक सूत्र जो इनमें सिद्ध किया जा सकता है, में     पराभव  का     वृक्ष है।
-इसे निम्न प्रकार से दिखाया जा सकता है: तर्कवाक्य कलन में प्रत्येक उपपत्ति    मात्र  अभिगृहीतों और अनुमान नियमों का उपयोग करती है। स्वयंसिद्ध योजना का प्रत्येक उपयोग एक वास्तविक तार्किक सूत्र उत्पन्न करता है, और इस प्रकार अनुक्रमिक कलन में सिद्ध किया जा सकता है; इनके लिए उदाहरण अनुक्रमिक     अश्म   # उदाहरण व्युत्पन्न हैं। ऊपर वर्णित प्रणालियों में एकमात्र निष्कर्ष नियम मॉडस पोनेंस है, जिसे    परिवर्तन  नियम    के अनुसार  कार्यान्वित किया जाता है।
+इसे निम्न प्रकार से दिखाया जा सकता है: तर्कवाक्य कलन में प्रत्येक उपपत्ति    मात्र  अभिगृहीतों और अनुमान नियमों का उपयोग करती है। स्वयंसिद्ध योजना का प्रत्येक उपयोग एक वास्तविक तार्किक सूत्र उत्पन्न करता है, और इस प्रकार अनुक्रमिक कलन में सिद्ध किया जा सकता है; इनके लिए उदाहरण अनुक्रमिक     अश्म व्युत्पन्न हैं। ऊपर वर्णित प्रणालियों में एकमात्र निष्कर्ष नियम     विधानात्मक हेतु फलानुमान है, जिसे    परिवर्तन  नियम    के अनुसार  कार्यान्वित किया जाता है।
 == सिस्टम एलके ==
-यह खंड 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 में जेंटजेन    के अनुसार     प्रस्तुत  किए गए अनुक्रमिक     अश्म   एलके (    तार्किक कल्कुल स्थिति) के नियमों का परिचय देता है। <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>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>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>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>: ये छह तीन संरचनात्मक नियमों में से प्रत्येक के दो संस्करणों के लिए खड़े हैं; बाईं ओर ('L') उपयोग के लिए a<math>\vdash</math>, और    द्वितीय  इसके दाईं ओर ('R')। नियमों को    अदृढ़  करने के लिए 'W' (बाएं / दाएं), संकुचन के लिए 'C' और क्रमचय के लिए 'P' संक्षिप्त किया गया है।
-ध्यान दें कि, ऊपर प्रस्तुत     निगमन वृक्ष के साथ आगे बढ़ने के नियमों के विपरीत, निम्नलिखित नियम विपरीत दिशाओं में जाने के लिए हैं, स्वयंसिद्ध से प्रमेय तक। इस प्रकार वे उपरोक्त नियमों की सटीक दर्पण-छवियां हैं, सिवाय इसके कि यहां समरूपता को स्पष्ट रूप से ग्रहण नहीं किया गया है, और [[परिमाणक (तर्क)]] के संबंध में नियम जोड़े गए हैं।
+ध्यान दें कि, ऊपर प्रस्तुत     निगमन वृक्ष के साथ आगे बढ़ने के नियमों के विपरीत, निम्नलिखित नियम विपरीत दिशाओं में जाने के लिए हैं, स्वयंसिद्ध से प्रमेय तक। इस प्रकार वे उपरोक्त नियमों की सटीक दर्पण-छवियां हैं,    अतिरिक्त  इसके कि यहां समरूपता को स्पष्ट रूप से ग्रहण नहीं किया गया है, और [[परिमाणक (तर्क)]] के संबंध में नियम    संकलित किये  गए हैं।
 {| border="0" cellpadding="20" style="text-align:center"
 |-
-| Axiom:
+| स्वयंसिद्ध
-| Cut:
+| आभाव
 |-
 | style="background:#fafafa; border:1px #ccc solid;" |
@@ Line 180: / Line 179: @@
   </math>
 |-
-| Left logical rules:
+| बाएं तार्किक नियम
-| Right logical rules:
+| दाएं  तार्किक नियम
 |-
 | style="background:#fafafa; border:1px #ccc solid;" |
@@ Line 240: / Line 239: @@
   </math>
 |-
-| Left structural rules:
+| बाएं  संरचनात्मक नियम
-| Right structural rules:
+| दाएं  संरचनात्मक नियम
 |-
 | style="background:#fafafa; border:1px #ccc solid;" |
@@ Line 270: / Line 269: @@
   </math>
 |}
-प्रतिबंध: नियमों में <math>({\forall}R)</math> और <math>({\exists}L)</math>, चर <math>y</math> संबंधित निचले अनुक्रमों में कहीं भी मुक्त नहीं होना चाहिए।
+प्रतिबंध: नियमों में <math>({\forall}R)</math> और <math>({\exists}L)</math>, चर <math>y</math> संबंधित    निम्नतर    अनुक्रमों में कहीं भी मुक्त नहीं होना चाहिए।
 === एक सहज व्याख्या ===
@@ Line 276: / Line 275: @@
 उपरोक्त नियमों को दो प्रमुख समूहों में विभाजित किया जा सकता है: तार्किक और संरचनात्मक। प्रत्येक तार्किक नियम     चक्रद्वार  (प्रतीक) के बाईं ओर या दाईं ओर एक नया तार्किक सूत्र प्रस्तुत करता है। <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> (चूंकि यह नीचे बिल्कुल नहीं दिखता है)।    परिवर्तन -एलिमिनेशन प्रमेय इस प्रकार स्वचालित     निगमन में अनुक्रम कलन के अनुप्रयोगों के लिए महत्वपूर्ण है: यह बताता है कि    परिवर्तन  नियम के सभी उपयोगों को एक प्रमाण से समाप्त किया जा सकता है, जिसका अर्थ है कि किसी भी सिद्ध अनुक्रम को    परिवर्तन -  स्वतंत्र प्रमाण दिया जा सकता है।
-दूसरा नियम जो कुछ विशेष है वह पहचान का स्वयंसिद्ध (I) है। इसका सहज ज्ञान स्पष्ट है: प्रत्येक सूत्र स्वयं को सिद्ध करता है।    परिवर्तन  नियम की तरह, पहचान का स्वयंसिद्ध कुछ   स्तर  तक बेमानी है: [[परमाणु प्रारंभिक अनुक्रमों की पूर्णता]] बताती है कि नियम को किसी भी नुकसान के  नियमबद्ध [[परमाणु सूत्र]]ों तक सीमित किया जा सकता है।
+द्वितीय  नियम जो कुछ विशेष है वह पहचान का स्वयंसिद्ध (I) है। इसका सहज ज्ञान स्पष्ट है: प्रत्येक सूत्र स्वयं को सिद्ध करता है।    परिवर्तन  नियम की तरह, पहचान का स्वयंसिद्ध कुछ   स्तर  तक बेमानी है: [[परमाणु प्रारंभिक अनुक्रमों की पूर्णता]] बताती है कि नियम को किसी भी नुकसान के  नियमबद्ध [[परमाणु सूत्र]]ों तक सीमित किया जा सकता है।
-ध्यान दें कि निहितार्थ के नियमों को छोड़कर, सभी नियमों में दर्पण साथी होते हैं। यह इस तथ्य को दर्शाता है कि प्रथम-क्रम तर्क की सामान्य भाषा में संयोजी    के अनुसार  निहित नहीं है शामिल नहीं है <math>\not\leftarrow</math> यह निहितार्थ का डी मॉर्गन दोहरा होगा। इस तरह के संयोजन को अपने प्राकृतिक नियमों के साथ जोड़ने से कलन पूरी तरह से बाएँ-दाएँ सममित हो जाएगा।
+ध्यान दें कि निहितार्थ के नियमों को छोड़कर, सभी नियमों में दर्पण साथी होते हैं। यह इस तथ्य को    प्रकट करता   है कि प्रथम-क्रम तर्क की सामान्य भाषा में संयोजी    के अनुसार  निहित नहीं है शामिल नहीं है <math>\not\leftarrow</math> यह निहितार्थ का डी मॉर्गन दोहरा होगा। इस तरह के संयोजन को अपने प्राकृतिक नियमों के साथ जोड़ने से कलन पूरी तरह से बाएँ-दाएँ सममित हो जाएगा।
 === उदाहरण व्युत्पत्ति ===
@@ Line 358: / Line 357: @@
 | &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 415: / Line 414: @@
 | &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>. व्युत्पत्ति का पता लगाना सीधा है, जो स्वचालित     प्रमाणन      करने में एलके की उपयोगिता को    प्रकट करता   है।
 {| align=center border=0 cellspacing=0 cellpadding=0
 |-
@@ Line 680: / Line 679: @@
 |}
-ये व्युत्पत्ति अनुक्रमिक कलन की सख्त औपचारिक संरचना पर भी     बल   देती हैं। उदाहरण के लिए, ऊपर परिभाषित तार्किक नियम    सदैव घूमने वाले दरवाज़े से सटे सूत्र पर कार्य करते हैं, जैसे कि क्रमचय नियम आवश्यक हैं। हालाँकि, ध्यान दें कि यह जेंटज़ेन की मूल शैली में प्रस्तुति का एक हिस्सा है। एक सामान्य सरलीकरण में एक स्पष्ट क्रमपरिवर्तन नियम की आवश्यकता को समाप्त करते हुए अनुक्रम के बजाय अनुक्रम की व्याख्या में सूत्रों के [[ multiset ]] का उपयोग शामिल है। यह अनुक्रम कलन के बाहर मान्यताओं और व्युत्पत्तियों की कम्यूटेटिविटी को स्थानांतरित करने के अनुरूप है, जबकि एलके इसे सिस्टम के भीतर ही एम्बेड करता है।
+ये व्युत्पत्ति अनुक्रमिक कलन की सख्त औपचारिक संरचना पर भी     बल   देती हैं। उदाहरण के लिए, ऊपर परिभाषित तार्किक नियम    सदैव घूमने वाले दरवाज़े से सटे सूत्र पर कार्य करते हैं, जैसे कि क्रमचय नियम आवश्यक हैं। हालाँकि, ध्यान दें कि यह जेंटज़ेन की मूल शैली में प्रस्तुति का एक     खंड  है। एक सामान्य सरलीकरण में एक स्पष्ट क्रमपरिवर्तन नियम की आवश्यकता को समाप्त करते हुए अनुक्रम के बजाय अनुक्रम की व्याख्या में सूत्रों के [[ multiset ]] का उपयोग शामिल है। यह अनुक्रम कलन के बाहर मान्यताओं और व्युत्पत्तियों की कम्यूटेटिविटी को स्थानांतरित करने के अनुरूप है,     यद्यपि  एलके इसे सिस्टम के भीतर ही एम्बेड करता है।
 === विश्लेषणात्मक झांकी से संबंध ===
-अनुक्रमिक     अश्म   के कुछ फॉर्मूलेशन (यानी वेरिएंट) के लिए, इस तरह के     अश्म   में एक प्रमाण विश्लेषणात्मक झांकी के उल्टा, बंद विधि के लिए आइसोमोर्फिक है।<ref>{{harvnb|Smullyan|1995|p=107}}</ref>
+अनुक्रमिक     अश्म   के कुछ फॉर्मूलेशन (   अर्थात  वेरिएंट) के लिए, इस तरह के     अश्म   में एक प्रमाण विश्लेषणात्मक झांकी के उल्टा, बंद विधि के लिए आइसोमोर्फिक है।<ref>{{harvnb|Smullyan|1995|p=107}}</ref>
@@ Line 690: / Line 689: @@
 संरचनात्मक नियम कुछ अतिरिक्त चर्चा के पात्र हैं।
-कमजोर करना (डब्ल्यू) मनमाना तत्वों को [[अनुक्रम]] में जोड़ने की अनुमति देता है। सहज रूप से, पूर्ववर्ती में इसकी अनुमति है क्योंकि हम    सदैव अपने प्रमाण के दायरे को सीमित कर सकते हैं (यदि सभी कारों में पहिए हैं, तो यह कहना सुरक्षित है कि सभी काली कारों में पहिए हैं); और उत्तरवर्ती में क्योंकि हम    सदैव वैकल्पिक निष्कर्ष की अनुमति दे सकते हैं (यदि सभी कारों में पहिए हैं, तो यह कहना सुरक्षित है कि सभी कारों में पहिए या पंख होते हैं)।
+अदृढ़  करना (डब्ल्यू) मनमाना तत्वों को [[अनुक्रम]] में जोड़ने की अनुमति देता है। सहज रूप से, पूर्ववर्ती में इसकी अनुमति है क्योंकि हम    सदैव अपने प्रमाण के दायरे को सीमित कर सकते हैं (यदि सभी कारों में पहिए हैं, तो यह कहना सुरक्षित है कि सभी काली कारों में पहिए हैं); और उत्तरवर्ती में क्योंकि हम    सदैव वैकल्पिक निष्कर्ष की अनुमति दे सकते हैं (यदि सभी कारों में पहिए हैं, तो यह कहना सुरक्षित है कि सभी कारों में पहिए या पंख होते हैं)।
-संकुचन (सी) और क्रमचय (पी) आश्वस्त करते हैं कि अनुक्रम के तत्वों के न तो आदेश (पी) और न ही घटनाओं की बहुलता (सी) मायने रखती है। इस प्रकार, अनुक्रमों के बजाय [[सेट (गणित)]] पर भी विचार किया जा सकता है।
+संकुचन (सी) और क्रमचय (पी) आश्वस्त करते हैं कि अनुक्रम के तत्वों के न तो आदेश (पी) और न ही घटनाओं की बहुलता (सी)     प्रयोजन रखती है। इस प्रकार, अनुक्रमों के बजाय [[सेट (गणित)]] पर भी विचार किया जा सकता है।
 हालाँकि, अनुक्रमों का उपयोग करने का अतिरिक्त प्रयास उचित है क्योंकि भाग या सभी संरचनात्मक नियमों को छोड़ा जा सकता है। ऐसा करने से, तथाकथित [[अवसंरचनात्मक तर्क]] प्राप्त होता है।
@@ Line 712: / Line 711: @@
 सबसे पहले, जैसा कि ऊपर उल्लेख किया गया है, अनुक्रमों को सेट या मल्टीसेट से मिलकर देखा जा सकता है। इस मामले में, अनुमत करने के नियम और (सेट का उपयोग करते समय) अनुबंध सूत्र अप्रचलित हैं।
-कमजोर करने का नियम स्वीकार्य हो जाएगा, जब स्वयंसिद्ध (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> ऊपर जाने पर। चूंकि संकुचन इनके दोहराव की अनुमति देता है, कोई यह मान सकता है कि व्युत्पत्ति की दोनों शाखाओं में पूर्ण संदर्भ का उपयोग किया जाता है। ऐसा करने से, यह सुनिश्चित होता है कि कोई भी महत्वपूर्ण परिसर गलत शाखा में खो न जाए।    अदृढ़  पड़ने का उपयोग करके, संदर्भ के अप्रासंगिक भागों को बाद में समाप्त किया जा सकता है।
 === बेतुकापन ===
@@ Line 722: / Line 721: @@
    \cfrac{}{\bot \vdash \quad }
 </math>
-या यदि, जैसा कि ऊपर वर्णित है, कमजोर करना एक स्वीकार्य नियम है, तो स्वयंसिद्ध के साथ:
+या यदि, जैसा कि ऊपर वर्णित है,    अदृढ़  करना एक स्वीकार्य नियम है, तो स्वयंसिद्ध के साथ:
 :<math>
@@ Line 732: / Line 731: @@
 {{main article|Substructural logic}}
-वैकल्पिक रूप से, कोई कुछ संरचनात्मक नियमों के उपयोग को प्रतिबंधित या प्रतिबंधित कर सकता है। यह विभिन्न प्रकार के अवसंरचनात्मक तर्क प्रणालियों का उत्पादन करता है। वे आम तौर पर एलके से कमजोर होते हैं (यानी, उनके पास कम प्रमेय होते हैं), और इस प्रकार प्रथम-क्रम तर्क के मानक शब्दों के संबंध में पूर्ण नहीं होते हैं। हालांकि, उनके पास अन्य रोचक गुण हैं जो सैद्धांतिक [[कंप्यूटर विज्ञान]] और कृत्रिम बुद्धि में अनुप्रयोगों के लिए प्रेरित हुए हैं।
+वैकल्पिक रूप से, कोई कुछ संरचनात्मक नियमों के उपयोग को प्रतिबंधित या प्रतिबंधित कर सकता है। यह विभिन्न प्रकार के अवसंरचनात्मक तर्क प्रणालियों का उत्पादन करता है। वे आम तौर पर एलके से    अदृढ़  होते हैं (   अर्थात , उनके पास कम प्रमेय होते हैं), और इस प्रकार प्रथम-क्रम तर्क के मानक शब्दों के संबंध में पूर्ण नहीं होते हैं। हालांकि, उनके पास अन्य रोचक गुण हैं जो सैद्धांतिक [[कंप्यूटर विज्ञान]] और कृत्रिम बुद्धि में अनुप्रयोगों के लिए प्रेरित हुए हैं।
 ===अंतर्ज्ञानी अनुक्रम कलन: सिस्टम एलजे ===
@@ Line 743: / Line 742: @@
 परिणामी प्रणाली को एलजे कहा जाता है। यह अंतर्ज्ञानवादी तर्क के संबंध में ध्वनि और पूर्ण है और एक समान    परिवर्तन -उन्मूलन प्रमाण को स्वीकार करता है। इसका उपयोग [[संयोजन और अस्तित्व गुण]]ों को     प्रमाणन      करने में किया जा सकता है।
-वास्तव में, एलके में एकमात्र नियम जिसे एकल-सूत्र परिणामों तक सीमित करने की आवश्यकता है <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}

Anonymous

Search

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

Namespaces

More

Page actions

Revision as of 13:01, 23 May 2023

Contents

अवलोकन

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

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

अनुक्रमिक अश्म सिस्टम

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

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

तार्किक सूत्र सिद्ध करना

निगमन वृक्ष

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

सिस्टम एलके

अनुमान नियम

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

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

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

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

वेरिएंट

मामूली संरचनात्मक विकल्प

बेतुकापन

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

अंतर्ज्ञानी अनुक्रम कलन: सिस्टम एलजे

यह भी देखें

टिप्पणियाँ

संदर्भ

बाहरी संबंध

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

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

Revision as of 13:01, 23 May 2023

अवलोकन

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

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

अनुक्रमिक अश्म सिस्टम

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

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

तार्किक सूत्र सिद्ध करना

निगमन वृक्ष

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

सिस्टम एलके

अनुमान नियम

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

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

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

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

वेरिएंट

मामूली संरचनात्मक विकल्प

बेतुकापन

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

अंतर्ज्ञानी अनुक्रम कलन: सिस्टम एलजे

यह भी देखें

टिप्पणियाँ

संदर्भ

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories