अनुक्रमिक गणना

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

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

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

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

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

अवलोकन

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

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

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

$B$

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

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

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

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

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

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

प्राकृतिक निगमन में एक निर्णय का मानक शब्दार्थ यह है कि यह अनुरोध करता है कि जब भी $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},$

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

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

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

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

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

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

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

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

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

अनुक्रम शब्द जेंटजन के 1934 के लेख्य में अनुक्रम शब्द से लिया गया है।स्टीफन कोल क्लेन अंग्रेजी में अनुवाद पर निम्नलिखित टिप्पणी करते हैं: जेंटजन ' अनुक्रम ' कहते हैं, जिसे हम 'अनुक्रम' के रूप में अनुवादित करते हैं, क्योंकि हम पहले से ही वस्तुओं के किसी भी उत्तराधिकार के लिए 'अनुक्रम' का उपयोग कर चुके हैं, जहां जर्मन 'फोल्गे' है।

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

अनुक्रमिक कलन के अनुसार एक प्रमाण प्रकट करने की प्रक्रिया का वर्णन करने वाला एक जड़ वाला वृक्ष

निगमन वृक्ष

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

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

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

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

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

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

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

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

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

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

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

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

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

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

सिस्टम एलके

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

अनुमान नियम

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

$(I)$ $A\vdash A$     $(\lnot R)$ $\vdash \lnot A,A$     $(PR)$ $\vdash A,\lnot A$           $(I)$ $B\vdash B$           $(I)$ $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 का उपयोग शामिल है। यह अनुक्रम कलन के बाहर मान्यताओं और व्युत्पत्तियों की कम्यूटेटिविटी को स्थानांतरित करने के अनुरूप है, यद्यपि एलके इसे सिस्टम के भीतर ही एम्बेड करता है।

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

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

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

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

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

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

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

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

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

वेरिएंट

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

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

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

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

अदृढ़ करने का नियम स्वीकार्य हो जाएगा, जब स्वयंसिद्ध (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 )$.

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

Main article: Substructural logic

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

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

आश्चर्यजनक रूप से, एलके के नियमों में कुछ छोटे बदलाव इसे अंतर्ज्ञानवादी तर्क के लिए एक प्रमाण प्रणाली में बदलने के लिए पर्याप्त हैं। इसके लिए, किसी को दाहिनी ओर अधिक से अधिक एक सूत्र वाले अनुक्रमों तक सीमित करना होगा, और इस अपरिवर्तनीय को बनाए रखने के लिए नियमों को संशोधित करना होगा। उदाहरण के लिए, $({\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}}.$

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

यह भी देखें

• चक्रीय कलन
• नेस्टेड अनुक्रम कलन
• संकल्प (तर्क)
• प्रमाण सिद्धांत

संदर्भ

• 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.

बाहरी संबंध

• "Sequent calculus", Encyclopedia of Mathematics, EMS Press, 2001 [1994]
• A Brief Diversion: Sequent Calculus
• Interactive tutorial of the Sequent Calculus