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

Latest revision as of 16:56, 12 June 2023

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

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

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

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

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

अवलोकन

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

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

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

B

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

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

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

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

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

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

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

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

और

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

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

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

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

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

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

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

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

और

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

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

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

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

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

अथवा रूप में

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

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

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

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

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

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

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

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

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

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

रिडक्शन ट्री

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

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

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

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

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

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

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

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

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

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

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

p\rightarrow r,p,q\vdash r

q\rightarrow r,p,q\vdash r

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

\lnot p,p,q\vdash r

r,p,q\vdash r

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

p,q\vdash p,r

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

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

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

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

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

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

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

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

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

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

प्रणाली LK

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

अनुमान नियम

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(\lor L)

B\lor C\vdash B,C

(PR)

B\lor C\vdash C,B

(\lnot L)

B\lor C,\lnot C\vdash B

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

(I)

\lnot A\vdash \lnot A

(\rightarrow L)

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

(\land L_{1})

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

(PL)

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

(\land L_{2})

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

(CL)

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

(PL)

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

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

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

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

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

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

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

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

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

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

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

रूपांतर

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

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

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

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

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

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

असंगति

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

यह भी देखें

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

संदर्भ

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

बाहरी संबंध

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

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

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

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

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

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

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

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

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

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

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

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

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

[14] Buss 1998, p. 10

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

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

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

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

[19] Kleene 2002, p. 441.

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

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

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

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

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

[25] Smullyan 1995, p. 107

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

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

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

@@ Line 718: / Line 718: @@
 * [http://scienceblogs.com/goodmath/2006/07/17/a-brief-diversion-sequent-calc/ A Brief Diversion: Sequent Calculus]
 * [http://logitext.mit.edu/logitext.fcgi/tutorial Interactive tutorial of the Sequent Calculus]
-[[Category: सबूत सिद्धांत]] [[Category: तार्किक गणना]] [[Category: स्वचालित प्रमेय साबित करना]]
+[[Category:Articles with hatnote templates targeting a nonexistent page]]
-[[Category: Machine Translated Page]]
 [[Category:Created On 18/05/2023]]
-[[Category:Vigyan Ready]]
+[[Category:Lua-based templates]]
+[[Category:Machine Translated Page]]
+[[Category:Pages that use a deprecated format of the math tags]]
+[[Category:Pages with script errors]]
+[[Category:Templates Vigyan Ready]]
+[[Category:Templates that add a tracking category]]
+[[Category:Templates that generate short descriptions]]
+[[Category:Templates using TemplateData]]
+[[Category:तार्किक गणना]]
+[[Category:सबूत सिद्धांत]]
+[[Category:स्वचालित प्रमेय साबित करना]]

Anonymous

Search

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

Namespaces

More

Page actions

Latest revision as of 16:56, 12 June 2023

Contents

अवलोकन

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

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

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

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

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

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

रिडक्शन ट्री

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

प्रणाली LK

अनुमान नियम

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

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

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

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

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

रूपांतर

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

असंगति

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

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

यह भी देखें

टिप्पणियाँ

संदर्भ

बाहरी संबंध

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

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

Latest revision as of 16:56, 12 June 2023

अवलोकन

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

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

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

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

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

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

रिडक्शन ट्री

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

प्रणाली LK

अनुमान नियम

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

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

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

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

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

रूपांतर

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

असंगति

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

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

यह भी देखें

टिप्पणियाँ

संदर्भ

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories