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

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

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

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

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

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

अवलोकन

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

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

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

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

(कम से कम एक 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})$