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

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

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

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

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

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

सिंहावलोकन

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

हिल्बर्ट-शैली कटौती प्रणाली

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

$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}$एस और घूमने वाला दरवाज़ा स्पष्ट रूप से नहीं लिखा गया है; इसके बजाय एक द्वि-आयामी संकेतन का उपयोग किया जाता है जिससे उनका अनुमान लगाया जा सकता है।)

प्राकृतिक कटौती में एक निर्णय का मानक शब्दार्थ यह है कि यह दावा करता है कि जब भी $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})$

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

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

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

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

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

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

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

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

अनुक्रमिक कलन द्वारा एक सबूत खोजने की प्रक्रिया का वर्णन करने वाला एक जड़ वाला पेड़

कटौती के पेड़

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

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

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

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

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

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

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

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

सिस्टम एलके

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

अनुमान नियम

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

• $\vdash$ टर्नस्टाइल (प्रतीक) के रूप में जाना जाता है, बाईं ओर की मान्यताओं को दाईं ओर के प्रस्तावों से अलग करता है
• $A$ और $B$ प्रथम-क्रम विधेय तर्क के सूत्रों को निरूपित करें (कोई इसे प्रस्तावपरक तर्क तक सीमित भी कर सकता है),
• $\Gamma ,\Delta ,\Sigma$, और $\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)$ $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 Hauptsatz (मुख्य प्रमेय) के रूप में भी जाना जाता है।

वेरिएंट

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

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

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

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

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