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

Revision as of 00:09, 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$

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

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

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

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

सीक्वेंट अश्म प्रोपोज़िशनल अश्म के अन्य स्वयंसिद्धों से संबंधित है, जैसे कि फ़्रीज का प्रोपोज़ल अश्म या प्रोपोज़िशनल अश्म # उदाहरण 1। एक आभाव का पेड़।

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

सिस्टम एलके

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

अनुमान नियम

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

$\vdash$ चक्रद्वार (प्रतीक) के रूप में जाना जाता है, बाईं ओर की मान्यताओं को दाईं ओर के प्रस्तावों से अलग करता है
$A$ और $B$ प्रथम-क्रम विधेय तर्क के सूत्रों को निरूपित करें (कोई इसे प्रस्तावपरक तर्क तक सीमित भी कर सकता है),
$\Gamma ,\Delta ,\Sigma$ $\Gamma ,\Delta ,\Sigma$ , और $\Pi$ $\Pi$ सूत्रों के परिमित (संभवतः रिक्त ) अनुक्रम हैं (वास्तव में, सूत्रों का क्रम मायने नहीं रखता; देखें § Structural rules), संदर्भ कहा जाता है,
- जब बाईं ओर $\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$ : ये छह तीन संरचनात्मक नियमों में से प्रत्येक के दो संस्करणों के लिए खड़े हैं; a के बाईं ओर ('L') उपयोग के लिए एक $\vdash$ , और दूसरा इसके दाईं ओर ('आर')। नियमों को कमजोर करने के लिए 'डब्ल्यू' (बाएं / दाएं), संकुचन के लिए 'सी' और क्रमचय के लिए 'पी' संक्षिप्त किया गया है।

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

Axiom:	Cut:
${\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}})$
Left logical rules:	Right logical rules:
${\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)$
Left structural rules:	Right structural rules:
${\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 1: / Line 1: @@
 {{Short description|Style of formal logical argumentation}}
-गणितीय [[तर्क]] में, अनुक्रमिक कलन औपचारिक तार्किक तर्क की एक शैली है जिसमें एक [[औपचारिक प्रमाण]] की प्रत्येक पंक्ति एक  नियमबद्ध    नियमबद्ध पुनरुक्ति के बजाय एक     नियमबद्ध पुनरुक्ति (तर्क) ([[गेरहार्ड जेंटजन]]    के अनुसार  अनुक्रम कहा जाता है) है। नियमों और [[अनुमान]] की प्रक्रियाओं के अनुसार एक [[औपचारिक तर्क]] में पहले की पंक्तियों पर अन्य     नियमबद्ध  पुनरुक्ति  से प्रत्येक     नियमबद्ध  पुनरुक्ति  का अनुमान लगाया जाता है, जो गणितज्ञों    के अनुसार  डेविड हिल्बर्ट की तुलना में     निगमन की प्राकृतिक शैली के लिए एक    श्रेष्ठतर सन्निकटन देता है। डेविड हिल्बर्ट की औपचारिक तर्क की पहले की शैली, जिसमें हर पंक्ति एक  नियमबद्ध    नियमबद्ध पुनरुक्ति थी। अधिक सूक्ष्म     मुख्यता मौजूद हो सकते हैं; उदाहरण के लिए, प्रस्ताव अंतर्निहित रूप से     अतार्किक सिद्धांतों पर निर्भर हो सकते हैं। उस मामले में, अनुक्रम पहले क्रम के तर्क में     नियमबद्ध [[प्रमेय]] को     प्रकट करते हैं |     नियमबद्ध पुनरुक्ति के बजाय प्रथम-क्रम की भाषा।
+गणितीय [[तर्क]] में, अनुक्रमिक कलन औपचारिक तार्किक तर्क की एक शैली है जिसमें एक [[औपचारिक प्रमाण]] की प्रत्येक पंक्ति एक  नियमबद्ध    नियमबद्ध पुनरुक्ति के बजाय एक     नियमबद्ध पुनरुक्ति (तर्क) ([[गेरहार्ड जेंटजन]]    के अनुसार  अनुक्रम कहा जाता है) है। नियमों और [[अनुमान]] की प्रक्रियाओं के अनुसार एक [[औपचारिक तर्क]] में पहले की पंक्तियों पर अन्य     नियमबद्ध  पुनरुक्ति  से प्रत्येक     नियमबद्ध  पुनरुक्ति  का अनुमान लगाया जाता है, जो गणितज्ञों    के अनुसार  डेविड हिल्बर्ट की तुलना में     निगमन की प्राकृतिक शैली के लिए एक    श्रेष्ठतर सन्निकटन देता है। डेविड हिल्बर्ट की औपचारिक तर्क की पहले की शैली, जिसमें     प्रतिएक  पंक्ति एक  नियमबद्ध    नियमबद्ध पुनरुक्ति थी। अधिक सूक्ष्म     मुख्यता मौजूद हो सकते हैं; उदाहरण के लिए, प्रस्ताव अंतर्निहित रूप से     अतार्किक सिद्धांतों पर निर्भर हो सकते हैं। उस मामले में, अनुक्रम पहले क्रम के तर्क में     नियमबद्ध [[प्रमेय]] को     प्रकट करते हैं |     नियमबद्ध पुनरुक्ति के बजाय प्रथम-क्रम की भाषा।
 पंक्ति-दर-पंक्ति तार्किक तर्कों को व्यक्त करने के लिए अनुक्रम कलन, प्रमाण कलन की कई मौजूदा शैलियों में से एक है।
-* [[हिल्बर्ट प्रणाली|हिल्बर्ट शैली]]। हर पंक्ति एक  नियमबद्ध    नियमबद्ध पुनरुक्ति (या प्रमेय) है।
+* [[हिल्बर्ट प्रणाली|हिल्बर्ट शैली]]।     प्रतिएक  पंक्ति एक  नियमबद्ध    नियमबद्ध पुनरुक्ति (या प्रमेय) है।
 * जेंटजन     शैली। प्रत्येक पंक्ति बाईं ओर शून्य या अधिक     नियमों के साथ एक     नियमबद्ध पुनरुक्ति (या प्रमेय) है।
 ** [[प्राकृतिक कटौती|प्राकृतिक     निगमन]]। प्रत्येक (    नियमबद्ध) पंक्ति में दाईं ओर एक निश्चित प्रस्ताव है।
 ** अनुक्रमिक कलन। प्रत्येक (    नियमबद्ध) रेखा में दाईं ओर शून्य या अधिक मुखर प्रस्ताव होते हैं।
-दूसरे शब्दों में, प्राकृतिक     निगमन और अनुक्रमिक कलन प्रणालियाँ विशेष रूप से विशिष्ट प्रकार की जेंटजन-शैली प्रणालियाँ हैं। हिल्बर्ट-शैली प्रणालियों में आमतौर पर बहुत कम संख्या में अनुमान नियम होते हैं, जो [[स्वयंसिद्ध]] के सेट पर अधिक निर्भर करते हैं। जेंटजन-शैली प्रणालियों में आमतौर पर बहुत कम स्वयं सिद्ध होते हैं, यदि कोई हो, तो नियमों के सेट पर अधिक निर्भर करते हैं।
+दूसरे शब्दों में, प्राकृतिक     निगमन और अनुक्रमिक कलन प्रणालियाँ विशेष रूप से विशिष्ट प्रकार की जेंटजन-शैली प्रणालियाँ हैं। हिल्बर्ट-शैली प्रणालियों में आमतौर पर   अति  कम संख्या में अनुमान नियम होते हैं, जो [[स्वयंसिद्ध]] के सेट पर अधिक निर्भर करते हैं। जेंटजन-शैली प्रणालियों में आमतौर पर   अति  कम स्वयं सिद्ध होते हैं, यदि कोई हो, तो नियमों के सेट पर अधिक निर्भर करते हैं।
-हिल्बर्ट-शैली प्रणालियों की तुलना में जेंटजन-शैली प्रणालियों के महत्वपूर्ण व्यावहारिक और सैद्धांतिक लाभ हैं। उदाहरण के लिए, दोनों प्राकृतिक     निगमन और अनुक्रमिक कलन प्रणालियाँ सार्वभौमिक और अस्तित्वगत [[परिमाणीकरण (तर्क)]] के उन्मूलन और परिचय की सुविधा प्रदान करती हैं ताकि प्रस्तावात्मक कलन के बहुत सरल नियमों के अनुसार अगणित तार्किक अभिव्यक्तियों में हेरफेर किया जा सके। एक विशिष्ट तर्क में, क्वांटिफायर्स को समाप्त कर दिया जाता है, फिर [[प्रस्तावक गणना]] को अनक्वांटिफाइड एक्सप्रेशंस (जिसमें आमतौर पर फ्री वेरिएबल्स होते हैं) पर लागू किया जाता है, और फिर क्वांटिफायर्स को फिर से प्रस्तुत किया जाता है। यह बहुत हद तक उस तरीके से मेल खाता है जिसमें गणितज्ञों    के अनुसार  अभ्यास में गणितीय प्रमाणों का प्रयोग किया जाता है। विधेय कलन प्रमाण आमतौर पर इस दृष्टिकोण के साथ खोजने में बहुत आसान होते हैं, और अक्सर छोटे होते हैं। प्राकृतिक निगमन प्रणालियाँ व्यावहारिक प्रमेय सिद्ध करने के लिए अधिक अनुकूल हैं। सैद्धांतिक विश्लेषण के लिए अनुक्रमिक कलन प्रणाली अधिक अनुकूल हैं।
+हिल्बर्ट-शैली प्रणालियों की तुलना में जेंटजन-शैली प्रणालियों के महत्वपूर्ण व्यावहारिक और सैद्धांतिक लाभ हैं। उदाहरण के लिए, दोनों प्राकृतिक     निगमन और अनुक्रमिक कलन प्रणालियाँ सार्वभौमिक और अस्तित्वगत [[परिमाणीकरण (तर्क)]] के उन्मूलन और परिचय की सुविधा प्रदान करती हैं ताकि प्रस्तावात्मक कलन के   अति  सरल नियमों के अनुसार अगणित तार्किक अभिव्यक्तियों में परिवर्तन किया जा सके। एक विशिष्ट तर्क में,   परिमाणकों को समाप्त कर दिया जाता है, फिर [[प्रस्तावक गणना]] को   अपरिमित   अभिव्यक्ति (जिसमें आमतौर पर   स्वतंत्र   परिवर्तनशील  होते हैं) पर लागू किया जाता है, और फिर   परिमाणकों को फिर से प्रस्तुत किया जाता है। यह   अति    स्तर  तक उस तरीके से   अनुकूल    होता  है जिसमें गणितज्ञों    के अनुसार  अभ्यास में गणितीय प्रमाणों का प्रयोग किया जाता है। विधेय कलन प्रमाण आमतौर पर इस दृष्टिकोण के साथ    प्रकट करने  में   अति  आसान होते हैं, और अक्सर छोटे होते हैं। प्राकृतिक निगमन प्रणालियाँ व्यावहारिक प्रमेय सिद्ध करने के लिए अधिक अनुकूल हैं। सैद्धांतिक विश्लेषण के लिए अनुक्रमिक कलन प्रणाली अधिक अनुकूल हैं।
-== सिंहावलोकन==
+== अवलोकन ==
-[[सबूत सिद्धांत]] और गणितीय तर्क में, अनुक्रमिक कलन औपचारिक प्रणालियों का एक परिवार है जो अनुमान की एक निश्चित शैली और कुछ औपचारिक गुणों को साझा करता है। पहली अनुक्रमिक गणना प्रणाली, एलके और एलजे, 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> दूरगामी [[मेटाथ्योरी]]|मेटा-सैद्धांतिक परिणामों के साथ संगति सहित एक परिणाम। जेंटजन ने कुछ साल बाद इस तकनीक की शक्ति और लचीलेपन का प्रदर्शन किया, गोडेल के अपूर्णता प्रमेय के आश्चर्यजनक जवाब में, एक (ट्रांसफिनिट) जेंटजेन की स्थिरता प्रमाण देने के लिए एक कट-उन्मूलन तर्क लागू किया। इस प्रारंभिक कार्य के बाद से, अनुक्रमिक कैलकुली, जिसे जेंटजेन सिस्टम भी कहा जाता है,<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> और उनसे संबंधित सामान्य अवधारणाओं को प्रमाण सिद्धांत, गणितीय तर्क और [[स्वचालित कटौती|स्वचालित     निगमन]] के क्षेत्र में व्यापक रूप से लागू किया गया है।
 === [[हिल्बर्ट-शैली कटौती प्रणाली|हिल्बर्ट-शैली     निगमन प्रणाली]] ===
@@ Line 19: / Line 19: @@
 निगमन प्रणालियों की विभिन्न शैलियों को वर्गीकृत करने का एक तरीका सिस्टम में [[निर्णय (गणितीय तर्क)]] के रूप को देखना है, यानी, कौन सी चीजें एक (उप) प्रमाण के निष्कर्ष के रूप में प्रकट हो सकती हैं। हिल्बर्ट-शैली की     निगमन प्रणालियों में सबसे सरल निर्णय प्रपत्र का उपयोग किया जाता है, जहाँ एक निर्णय का रूप होता है
 :<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>
 (कम से कम एक असत्य है, या बीएस में से एक सत्य है)
-: या के रूप में
+: या रूप में
 :: <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 असत्य हैं)।
+(ऐसा नहीं हो सकता कि सभी एअइस सत्य हैं और सभी बीएस असत्य हैं)।
-इन योगों में, घूमने वाले दरवाज़े के दोनों ओर के सूत्रों के बीच एकमात्र अंतर यह है कि एक पक्ष को नकारा गया है। इस प्रकार, एक क्रम में बाएं से दाएं की अदला-बदली सभी घटक सूत्रों को नकारने के अनुरूप है। इसका मतलब यह है कि एक समरूपता जैसे डी मॉर्गन के कानून, जो सिमेंटिक स्तर पर खुद को तार्किक निषेध के रूप में प्रकट करते हैं, अनुक्रमों के बाएं-दाएं समरूपता में सीधे अनुवाद करते हैं- और वास्तव में, संयोजन (∧) से निपटने के लिए अनुक्रमिक कलन में अनुमान नियम हैं संयोजन से निपटने वालों की दर्पण छवियां (∨)।
+इन     परिणाम में,     चक्र द्वार  दोनों ओर के सूत्रों के बीच एकमात्र अंतर यह है कि एक पक्ष को     अस्वीकार करा गया है। इस प्रकार, एक क्रम में बाएं से दाएं की     परिवर्तन सभी घटक सूत्रों को     अस्वीकार के अनुरूप है। इसका     अर्थ यह है कि एक समरूपता जैसे डी मॉर्गन के कानून, जो सिमेंटिक स्तर पर खुद को तार्किक निषेध के रूप में प्रकट करते हैं, अनुक्रमों के बाएं-दाएं समरूपता में सीधे अनुवाद करते हैं- और वास्तव में, संयोजन (∧) से निपटने के लिए अनुक्रमिक कलन में निष्कर्ष नियम संयोजन (∨) से निपटने वालों की दर्पण छवियां  है।
-कई तर्कशास्त्री महसूस करते हैं {{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>
+जेंटजन ने अपने एकल-    उत्पादन   प्राकृतिक     निगमन प्रणाली (एनके और एनजे) और उनके बहु-    उत्पादन   सीक्वेंट     अश्म   सिस्टम (एलके और एलजे) के बीच एक     त्वरित्र   अंतर पर     बल   दिया। उन्होंने लिखा है कि अंतर्ज्ञानवादी प्राकृतिक     निगमन प्रणाली एनजे कुछ     कुरूप   थी।<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>
 === शब्द अनुक्रम की उत्पत्ति ===
-अनुक्रम शब्द Gentzen के 1934 के पेपर में Sequenz शब्द से लिया गया है।<ref name=gentzen19341935 />[[स्टीफन कोल क्लेन]] अंग्रेजी में अनुवाद पर निम्नलिखित टिप्पणी करते हैं: जेंटजन 'सीक्वेंज' कहते हैं, जिसे हम 'अनुक्रम' के रूप में अनुवादित करते हैं, क्योंकि हम पहले से ही वस्तुओं के किसी भी उत्तराधिकार के लिए 'अनुक्रम' का उपयोग कर चुके हैं, जहां जर्मन 'फोल्गे' है।<ref>{{harvnb|Kleene|2002|p=441}}.</ref>
+अनुक्रम शब्द    जेंटजन  के 1934 के     लेख्य   में     अनुक्रम   शब्द से लिया गया है।<ref name=gentzen19341935 />[[स्टीफन कोल क्लेन]] अंग्रेजी में अनुवाद पर निम्नलिखित टिप्पणी करते हैं: जेंटजन '    अनुक्रम  ' कहते हैं, जिसे हम 'अनुक्रम' के रूप में अनुवादित करते हैं, क्योंकि हम पहले से ही वस्तुओं के किसी भी उत्तराधिकार के लिए 'अनुक्रम' का उपयोग कर चुके हैं, जहां जर्मन 'फोल्गे' है।<ref>{{harvnb|Kleene|2002|p=441}}.</ref>
 == तार्किक सूत्र सिद्ध करना ==
-[[File:Sequent calculus proof tree example.png|thumb|अनुक्रमिक कलन    के अनुसार  एक सबूत खोजने की प्रक्रिया का वर्णन करने वाला एक जड़ वाला पेड़]]
+[[File:Sequent calculus proof tree example.png|thumb|अनुक्रमिक कलन    के अनुसार  एक    प्रमाण     प्रकट करने  की प्रक्रिया का वर्णन करने वाला एक जड़ वाला पेड़]]
 === निगमन के पेड़ ===
@@ Line 76: / Line 75: @@
 निम्नलिखित सूत्र पर विचार करें:
 :<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> इसलिए एक निम्नलिखित अनुक्रम में जाता है:
 :<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>
 चूँकि बाईं ओर के तर्कों को [[तार्किक संयोजन]]    के अनुसार  संबंधित माना जाता है, इसे निम्नलिखित    के अनुसार  प्रतिस्थापित किया जा सकता है:
@@ Line 92: / Line 91: @@
 दूसरा क्रम किया जाता है; पहले अनुक्रम को और सरल बनाया जा सकता है:
 :<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"/>
@@ Line 139: / Line 138: @@
 |}
-प्रोपोज़िशनल लॉजिक में किसी भी सूत्र से शुरू करके, चरणों की एक श्रृंखला    के अनुसार , घूमने वाले दरवाज़े के दाईं ओर संसाधित किया जा सकता है जब तक कि इसमें केवल परमाणु प्रतीक शामिल न हों। फिर, बाईं ओर के लिए भी ऐसा ही किया जाता है। चूँकि प्रत्येक तार्किक संकारक ऊपर दिए गए नियमों में से एक में प्रकट होता है, और नियम    के अनुसार  हटा दिया जाता है, जब कोई तार्किक संकारक नहीं रह जाता है तो प्रक्रिया समाप्त हो जाती है: सूत्र विघटित हो गया है।
+प्रोपोज़िशनल लॉजिक में किसी भी सूत्र से शुरू करके, चरणों की एक श्रृंखला    के अनुसार ,     चक्र द्वार  दाईं ओर संसाधित किया जा सकता है जब तक कि इसमें    मात्र  परमाणु प्रतीक शामिल न हों। फिर, बाईं ओर के लिए भी ऐसा ही किया जाता है। चूँकि प्रत्येक तार्किक संकारक ऊपर दिए गए नियमों में से एक में प्रकट होता है, और नियम    के अनुसार  हटा दिया जाता है, जब कोई तार्किक संकारक नहीं रह जाता है तो प्रक्रिया समाप्त हो जाती है: सूत्र विघटित हो गया है।
-इस प्रकार, पेड़ों की पत्तियों में अनुक्रमों में केवल परमाणु प्रतीक शामिल होते हैं, जो या तो स्वयंसिद्ध    के अनुसार  सिद्ध होते हैं या नहीं, इसके अनुसार दाईं ओर के प्रतीकों में से एक बाईं ओर भी दिखाई देता है।
+इस प्रकार, पेड़ों की पत्तियों में अनुक्रमों में    मात्र  परमाणु प्रतीक शामिल होते हैं, जो या तो स्वयंसिद्ध    के अनुसार  सिद्ध होते हैं या नहीं, इसके अनुसार दाईं ओर के प्रतीकों में से एक बाईं ओर भी दिखाई देता है।
-यह देखना आसान है कि पेड़ के चरण उनके    के अनुसार  निहित सूत्रों के सिमेंटिक ट्रुथ वैल्यू को संरक्षित करते हैं, जब भी कोई विभाजन होता है तो पेड़ की विभिन्न शाखाओं के बीच संयोजन को समझा जाता है। यह भी स्पष्ट है कि एक अभिगृहीत सिद्ध होता है यदि और केवल यदि यह परमाणु प्रतीकों के सत्य मानों के प्रत्येक आबंटन के लिए सत्य है। इस प्रकार शास्त्रीय प्रस्तावपरक तर्क के लिए यह प्रणाली सु[[दृढ़ता]] और [[पूर्णता (तर्क)]] है।
+यह देखना आसान है कि पेड़ के चरण उनके    के अनुसार  निहित सूत्रों के सिमेंटिक ट्रुथ वैल्यू को संरक्षित करते हैं, जब भी कोई विभाजन होता है तो पेड़ की विभिन्न शाखाओं के बीच संयोजन को समझा जाता है। यह भी स्पष्ट है कि एक अभिगृहीत सिद्ध होता है यदि और    मात्र  यदि यह परमाणु प्रतीकों के सत्य मानों के प्रत्येक आबंटन के लिए सत्य है। इस प्रकार शास्त्रीय प्रस्तावपरक तर्क के लिए यह प्रणाली सु[[दृढ़ता]] और [[पूर्णता (तर्क)]] है।
 === मानक स्वयंसिद्धीकरणों से संबंध ===
-सीक्वेंट कैलकुलस प्रोपोज़िशनल कैलकुलस के अन्य स्वयंसिद्धों से संबंधित है, जैसे कि फ़्रीज का प्रोपोज़ल कैलकुलस या प्रोपोज़िशनल कैलकुलस # उदाहरण 1। एक कमी का पेड़।
+सीक्वेंट     अश्म   प्रोपोज़िशनल     अश्म   के अन्य स्वयंसिद्धों से संबंधित है, जैसे कि फ़्रीज का प्रोपोज़ल     अश्म   या प्रोपोज़िशनल     अश्म   # उदाहरण 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>\vdash</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||Structural rules}}), संदर्भ कहा जाता है,
 ** जब बाईं ओर <math>\vdash</math>, सूत्रों के अनुक्रम को संयोजन के रूप में माना जाता है (सभी को एक ही समय में माना जाता है),
 ** जबकि के दाईं ओर <math>\vdash</math>, सूत्रों के अनुक्रम को वियोगात्मक रूप से माना जाता है (चर के किसी भी असाइनमेंट के लिए कम से कम एक सूत्र को धारण करना चाहिए),
@@ Line 278: / Line 277: @@
 === एक सहज व्याख्या ===
-उपरोक्त नियमों को दो प्रमुख समूहों में विभाजित किया जा सकता है: तार्किक और संरचनात्मक। प्रत्येक तार्किक नियम टर्नस्टाइल (प्रतीक) के बाईं ओर या दाईं ओर एक नया तार्किक सूत्र प्रस्तुत करता है। <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> यह निहितार्थ का डी मॉर्गन दोहरा होगा। इस तरह के संयोजन को अपने प्राकृतिक नियमों के साथ जोड़ने से कलन पूरी तरह से बाएँ-दाएँ सममित हो जाएगा।
@@ Line 684: / Line 683: @@
 |}
-ये व्युत्पत्ति अनुक्रमिक कलन की सख्त औपचारिक संरचना पर भी जोर देती हैं। उदाहरण के लिए, ऊपर परिभाषित तार्किक नियम हमेशा घूमने वाले दरवाज़े से सटे सूत्र पर कार्य करते हैं, जैसे कि क्रमचय नियम आवश्यक हैं। हालाँकि, ध्यान दें कि यह जेंटज़ेन की मूल शैली में प्रस्तुति का एक हिस्सा है। एक सामान्य सरलीकरण में एक स्पष्ट क्रमपरिवर्तन नियम की आवश्यकता को समाप्त करते हुए अनुक्रम के बजाय अनुक्रम की व्याख्या में सूत्रों के [[ multiset ]] का उपयोग शामिल है। यह अनुक्रम कलन के बाहर मान्यताओं और व्युत्पत्तियों की कम्यूटेटिविटी को स्थानांतरित करने के अनुरूप है, जबकि एलके इसे सिस्टम के भीतर ही एम्बेड करता है।
+ये व्युत्पत्ति अनुक्रमिक कलन की सख्त औपचारिक संरचना पर भी     बल   देती हैं। उदाहरण के लिए, ऊपर परिभाषित तार्किक नियम    सदैव घूमने वाले दरवाज़े से सटे सूत्र पर कार्य करते हैं, जैसे कि क्रमचय नियम आवश्यक हैं। हालाँकि, ध्यान दें कि यह जेंटज़ेन की मूल शैली में प्रस्तुति का एक हिस्सा है। एक सामान्य सरलीकरण में एक स्पष्ट क्रमपरिवर्तन नियम की आवश्यकता को समाप्त करते हुए अनुक्रम के बजाय अनुक्रम की व्याख्या में सूत्रों के [[ multiset ]] का उपयोग शामिल है। यह अनुक्रम कलन के बाहर मान्यताओं और व्युत्पत्तियों की कम्यूटेटिविटी को स्थानांतरित करने के अनुरूप है, जबकि एलके इसे सिस्टम के भीतर ही एम्बेड करता है।
 === विश्लेषणात्मक झांकी से संबंध ===
-अनुक्रमिक कैलकुस के कुछ फॉर्मूलेशन (यानी वेरिएंट) के लिए, इस तरह के कैलकुस में एक प्रमाण विश्लेषणात्मक झांकी के उल्टा, बंद विधि के लिए आइसोमोर्फिक है।<ref>{{harvnb|Smullyan|1995|p=107}}</ref>
+अनुक्रमिक     अश्म   के कुछ फॉर्मूलेशन (यानी वेरिएंट) के लिए, इस तरह के     अश्म   में एक प्रमाण विश्लेषणात्मक झांकी के उल्टा, बंद विधि के लिए आइसोमोर्फिक है।<ref>{{harvnb|Smullyan|1995|p=107}}</ref>
@@ Line 694: / Line 693: @@
 संरचनात्मक नियम कुछ अतिरिक्त चर्चा के पात्र हैं।
-कमजोर करना (डब्ल्यू) मनमाना तत्वों को [[अनुक्रम]] में जोड़ने की अनुमति देता है। सहज रूप से, पूर्ववर्ती में इसकी अनुमति है क्योंकि हम हमेशा अपने प्रमाण के दायरे को सीमित कर सकते हैं (यदि सभी कारों में पहिए हैं, तो यह कहना सुरक्षित है कि सभी काली कारों में पहिए हैं); और उत्तरवर्ती में क्योंकि हम हमेशा वैकल्पिक निष्कर्ष की अनुमति दे सकते हैं (यदि सभी कारों में पहिए हैं, तो यह कहना सुरक्षित है कि सभी कारों में पहिए या पंख होते हैं)।
+कमजोर करना (डब्ल्यू) मनमाना तत्वों को [[अनुक्रम]] में जोड़ने की अनुमति देता है। सहज रूप से, पूर्ववर्ती में इसकी अनुमति है क्योंकि हम    सदैव अपने प्रमाण के दायरे को सीमित कर सकते हैं (यदि सभी कारों में पहिए हैं, तो यह कहना सुरक्षित है कि सभी काली कारों में पहिए हैं); और उत्तरवर्ती में क्योंकि हम    सदैव वैकल्पिक निष्कर्ष की अनुमति दे सकते हैं (यदि सभी कारों में पहिए हैं, तो यह कहना सुरक्षित है कि सभी कारों में पहिए या पंख होते हैं)।
 संकुचन (सी) और क्रमचय (पी) आश्वस्त करते हैं कि अनुक्रम के तत्वों के न तो आदेश (पी) और न ही घटनाओं की बहुलता (सी) मायने रखती है। इस प्रकार, अनुक्रमों के बजाय [[सेट (गणित)]] पर भी विचार किया जा सकता है।
@@ Line 702: / Line 701: @@
 === सिस्टम एलके === के गुण
-नियमों की इस प्रणाली को प्रथम-क्रम तर्क के संबंध में सुदृढ़ता और पूर्णता (तर्क) दोनों के रूप में दिखाया जा सकता है, अर्थात एक कथन <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>
+नियमों की इस प्रणाली को प्रथम-क्रम तर्क के संबंध में सुदृढ़ता और पूर्णता (तर्क) दोनों के रूप में दिखाया जा सकता है, अर्थात एक कथन <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 />
+अनुक्रमिक कलन में,    [[कट-उन्मूलन|परिवर्तन -उन्मूलन]] का नियम। इस परिणाम को Gentzen's    हॉपट॒सत्ज़  (मुख्य प्रमेय) के रूप में भी जाना जाता है।<ref name=curry_cut_elimination /><ref name=kleene_cut_elimination />
@@ Line 716: / Line 715: @@
 सबसे पहले, जैसा कि ऊपर उल्लेख किया गया है, अनुक्रमों को सेट या मल्टीसेट से मिलकर देखा जा सकता है। इस मामले में, अनुमत करने के नियम और (सेट का उपयोग करते समय) अनुबंध सूत्र अप्रचलित हैं।
-कमजोर करने का नियम स्वीकार्य हो जाएगा, जब स्वयंसिद्ध (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> ऊपर जाने पर। चूंकि संकुचन इनके दोहराव की अनुमति देता है, कोई यह मान सकता है कि व्युत्पत्ति की दोनों शाखाओं में पूर्ण संदर्भ का उपयोग किया जाता है। ऐसा करने से, यह सुनिश्चित होता है कि कोई भी महत्वपूर्ण परिसर गलत शाखा में खो न जाए। कमजोर पड़ने का उपयोग करके, संदर्भ के अप्रासंगिक भागों को बाद में समाप्त किया जा सकता है।
@@ Line 745: / Line 744: @@
    \cfrac{\Gamma, A \vdash C \qquad \Sigma, B \vdash C }{\Gamma, \Sigma, A \lor B \vdash C} \quad ({\lor}L)
 </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> बनना
@@ Line 761: / Line 760: @@
 * [[नेस्टेड अनुक्रम कलन]]
 * [[संकल्प (तर्क)]]
-* सबूत सिद्धांत
+* प्रमाण  सिद्धांत
 ==टिप्पणियाँ==

Anonymous

Search

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

Namespaces

More

Page actions

Revision as of 00:09, 23 May 2023

Contents

अवलोकन

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

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

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

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

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

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

निगमन के पेड़

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

सिस्टम एलके

अनुमान नियम

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

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

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

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

वेरिएंट

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

बेतुकापन

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

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

यह भी देखें

टिप्पणियाँ

संदर्भ

बाहरी संबंध

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

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

Revision as of 00:09, 23 May 2023

अवलोकन

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

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

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

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

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

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

निगमन के पेड़

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

सिस्टम एलके

अनुमान नियम

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

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

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

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

वेरिएंट

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

बेतुकापन

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

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

यह भी देखें

टिप्पणियाँ

संदर्भ

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories