प्रमाण (प्रूफ) सिद्धांत

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

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

इतिहास

यद्यपि गोटलोब फ्रेज, ग्यूसेप पीनो, बर्ट्रेंड रसेल और रिचर्ड डेडेकाइंड जैसी हस्तियों के काम से लॉजिक की औपचारिकता बहुत आगे बढ़ गई थी, आधुनिक प्रूफ सिद्धांत की कहानी को प्रायः डेविड हिल्बर्ट द्वारा स्थापित किया गया माना जाता है, जिन्होंने हिल्बर्ट की आरंभ की थी। गणित की नींव में कार्यक्रम इस कार्यक्रम का केंद्रीय विचार यह था कि यदि हम गणितज्ञों के लिए आवश्यक सभी परिष्कृत औपचारिक सिद्धांतों के लिए स्थिरता के अंतिम प्रूफ दे सकते हैं, तो हम इन सिद्धांतों को एक मेटामैथमैटिकल लॉजिक के माध्यम से आधार बना सकते हैं, जो दर्शाता है कि सभी उनके विशुद्ध रूप से सार्वभौमिक दावे (अधिक तकनीकी रूप से उनके सिद्ध $\Pi _{1}^{0}$ वाक्य) अंतिम रूप से सत्य हैं; एक बार इस तरह से स्थापित हो जाने पर हमें उनके अस्तित्व संबंधी प्रमेयों के गैर-अंतहीन अर्थ की परवाह नहीं है, इन्हें आदर्श संस्थाओं के अस्तित्व की छद्म-अर्थपूर्ण शर्तों के रूप में माना जाता है।

कार्यक्रम की विफलता कर्ट गोडेल के गोडेल के अपूर्णता प्रमेय से प्रेरित थी, जिससे पता चला कि कोई भी ω-संगत सिद्धांत जो कुछ सरल अंकगणितीय सत्य को व्यक्त करने के लिए पर्याप्त रूप से प्रबल है, अपनी स्वयं की स्थिरता सिद्ध नहीं कर सकता है, जो गोडेल के सूत्रीकरण पर एक है $\Pi _{1}^{0}$ वाक्य। हालाँकि, हिल्बर्ट के कार्यक्रम के संशोधित संस्करण सामने आए और संबंधित विषयों पर शोध किया गया है। इसके कारण विशेष रूप से निम्नलिखित उत्पन्न हुआ:

• गोडेल के परिणाम का परिशोधन, विशेष रूप से जे. बार्कले रोसेर का परिशोधन, ω-संगति की उपरोक्त आवश्यकता को सरल संगति में अशक्त करना;
• मॉडल भाषा, प्रयोज्यता लॉजिक के संदर्भ में गोडेल के परिणाम के मूल का स्वयंसिद्धीकरण;
• एलन ट्यूरिंग और सोलोमन फ़ेफ़रमैन के कारण सिद्धांतों की अनंत पुनरावृत्ति;
• स्व-सत्यापन सिद्धांतों की खोज, प्रणालियाँ अपने बारे में बात करने के लिए काफी प्रबल हैं, लेकिन विकर्ण लेम्मा को पूरा करने के लिए बहुत अशक्त हैं जो गोडेल के अप्राप्य लॉजिक की कुंजी है।

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

संरचनात्मक प्रूफ सिद्धांत

Main article: संरचनात्मक प्रमाण सिद्धांत

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

• हिल्बर्ट प्रणाली
• प्राकृतिक घटाव कलन
• क्रमिक गणना

इनमें से प्रत्येक प्रस्तावात्मक लॉजिक या मूलभूत लॉजिक या अंतर्ज्ञानवादी लॉजिक स्वाद, लगभग किसी भी मोडल लॉजिक, और कई उप-संरचनात्मक लॉजिक, जैसे प्रासंगिक लॉजिक या रैखिक लॉजिक का पूर्ण और स्वयंसिद्ध औपचारिकीकरण दे सकता है। वास्तव में, ऐसा लॉजिक खोजना असामान्य है जो इन गणनाओं में से किसी एक में प्रस्तुत किए जाने का विरोध करता है।

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

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

रिडक्टिव लॉजिक में उत्पन्न होने वाले विश्लेषणात्मक प्रूफों का एक विशेष परिवार केंद्रित प्रूफ है जो लक्ष्य-निर्देशित प्रूफ-खोज प्रक्रियाओं के एक बड़े परिवार की विशेषता बताता है। एक प्रूफ़ सिस्टम को एक केंद्रित रूप में बदलने की क्षमता इसकी वाक्यात्मक गुणवत्ता का एक अच्छा संकेत है, उसी तरह जैसे कट की स्वीकार्यता से पता चलता है कि एक प्रूफ़ सिस्टम वाक्यात्मक रूप से सुसंगत है।

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

संरचनात्मक सिद्धांत में अन्य शोध विषयों में विश्लेषणात्मक झांकी सम्मिलित है, जो लॉजिकों की एक विस्तृत श्रृंखला के लिए निर्णय प्रक्रियाएं और अर्ध-निर्णय प्रक्रियाएं प्रदान करने के लिए संरचनात्मक प्रूफ सिद्धांत से विश्लेषणात्मक प्रूफ के केंद्रीय विचार को लागू करती है, और उप-संरचनात्मक लॉजिक के प्रूफ सिद्धांत को लागू करती है। एक बड़ी चुनौती अव्यावहारिक सिद्धांतों का क्रमिक विश्लेषण रही है। इस दिशा में पहली सफलता ताकेउटी द्वारा Π1 की संगति का प्रूफ था 1-CA0 क्रमसूचक आरेख की विधि का उपयोग करते हुए।

सामान्य विश्लेषण

Main article: सामान्य विश्लेषण

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

क्रमिक विश्लेषण के परिणामों में सम्मिलित हैं (1) रचनात्मक सिद्धांतों के सापेक्ष मूलभूत दूसरे क्रम अंकगणित और सेट सिद्धांत के उपप्रणालियों की स्थिरता, (2) संयुक्त स्वतंत्रता परिणाम, और (3) सिद्ध कुल पुनरावर्ती कार्यों और सिद्ध रूप से अच्छी तरह से स्थापित अध्यादेशों का वर्गीकरण है।

ऑर्डिनल विश्लेषण की आरंभ जेंटज़ेन द्वारा की गई थी, जिन्होंने ऑर्डिनल ε तक अनंत प्रेरण का उपयोग करके पीनो अंकगणित की स्थिरता को ε₀ सिद्ध किया था। क्रमसूचक विश्लेषण को पहले और दूसरे क्रम के अंकगणित और सेट सिद्धांत के कई टुकड़ों तक विस्तारित किया गया है। एक बड़ी चुनौती अव्यावहारिक सिद्धांतों का क्रमिक विश्लेषण रही है। इस दिशा में पहली सफलता टेकुटी द्वारा Π11-CA₀ की संगति का प्रूफ ¹
₁₀ क्रमिक आरेखों की विधि का उपयोग करना है।

प्रोवेबिलिटी लॉजिक

Main article: प्रोवेबिलिटी लॉजिक

व्याख्यात्मकता लॉजिक एक मोडल लॉजिक है, जिसमें बॉक्स ऑपरेटर की व्याख्या 'यह सिद्ध करने योग्य है' के रूप में की जाती है। मुद्दा एक यथोचित समृद्ध सिद्धांत (गणितीय लॉजिक) के प्रूफ विधेय की धारणा को पकड़ना है। प्रोवेबिलिटी लॉजिक जीएल (कर्ट गोडेल|गोडेल-मार्टिन ह्यूगो लोब|लोब) के मूल सिद्धांतों के रूप में, जो पीनो अंकगणित में सिद्ध करने योग्य को पकड़ता है, कोई हिल्बर्ट-बर्नेज़ व्युत्पत्ति स्थितियों और लोब के प्रमेय के मोडल एनालॉग्स लेता है (यदि यह सिद्ध करने योग्य है कि प्रोवेबिलिटी A का तात्पर्य A से है, तो A सिद्ध है)।

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

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

प्रतिलोम गणित

Main article: प्रतिलोम गणित

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

रिवर्स गणित में, कोई व्यक्ति एक फ्रेमवर्क भाषा और एक आधार सिद्धांत - एक मूल स्वयंसिद्ध प्रणाली - से प्रारंभ होता है, जो उन अधिकांश प्रमेयों को सिद्ध करने के लिए बहुत अशक्त है, जिनमें किसी की रुचि हो सकती है, लेकिन फिर भी इन प्रमेयों को बताने के लिए आवश्यक परिभाषाएँ विकसित करने के लिए पर्याप्त शक्तिशाली है। उदाहरण के लिए, प्रमेय का अध्ययन करने के लिए "वास्तविक संख्याओं के प्रत्येक बंधे हुए अनुक्रम का एक सर्वोच्च होता है" एक आधार प्रणाली का उपयोग करना आवश्यक है जो वास्तविक संख्याओं और वास्तविक संख्याओं के अनुक्रमों के बारे में बात कर सके।

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

रिवर्स गणित में एक उल्लेखनीय घटना बिग फाइव स्वयंसिद्ध प्रणालियों की प्रबली है। बढ़ती ताकत के क्रम में, इन प्रणालियों को प्रारंभिक शब्दों आरसीए द्वारा नाम दिया गया है₀, RCA₀, WKL₀, ACA₀, ATR₀ और Π11-CA₀ साधारण गणित का लगभग हर प्रमेय जिसका उलटा गणितीय विश्लेषण किया गया है, इन पाँच प्रणालियों में से एक के बराबर सिद्ध हुआ है। हाल के शोध में संयोजन सिद्धांतों पर ध्यान केंद्रित किया गया है जो आरटी की तरह इस फ्रेमवर्क में अच्छी तरह से फिट नहीं होते हैं, जैसे RT22(जोड़ियों के लिए रैमसे का प्रमेय)।

रिवर्स गणित में अनुसंधान में प्रायः पुनरावर्तन सिद्धांत के साथ-साथ प्रूफ सिद्धांत के तरीकों और तकनीकों को सम्मिलित किया जाता है।

कार्यात्मक व्याख्याएँ

कार्यात्मक व्याख्याएँ कार्यात्मक सिद्धांतों में गैर-रचनात्मक सिद्धांतों की व्याख्याएँ हैं। कार्यात्मक व्याख्याएँ प्रायःदो चरणों में आगे बढ़ती हैं। सबसे पहले, एक मूलभूत सिद्धांत C को एक अंतर्ज्ञानवादी एक I में कम कर देता है। यानी, एक एक रचनात्मक मानचित्रण प्रदान करता है जो सी के प्रमेयों को I के प्रमेयों में अनुवादित करता है। दूसरा, एक एक अंतर्ज्ञानवादी सिद्धांत I को कार्यात्मकता एफ के एक क्वांटिफायर मुक्त सिद्धांत में कम कर देता है। ये व्याख्याएँ हिल्बर्ट के कार्यक्रम के एक रूप में योगदान करती हैं, क्योंकि वे रचनात्मक सिद्धांतों के सापेक्ष मूलभूत सिद्धांतों की स्थिरता को सिद्ध करती हैं। सफल कार्यात्मक व्याख्याओं ने अनंत सिद्धांतों को अंतिम सिद्धांतों में बदल दिया है और अव्यावहारिक सिद्धांतों को विधेय सिद्धांतों में बदल दिया है।

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

कार्यात्मक व्याख्याओं का अध्ययन कर्ट गोडेल की परिमित प्रकार के कार्यात्मकताओं के क्वांटिफायर-मुक्त सिद्धांत में अंतर्ज्ञानवादी अंकगणित की व्याख्या के साथ प्रारंभ हुआ। इस व्याख्या को प्रायःडायलेक्टिका व्याख्या के रूप में जाना जाता है। अंतर्ज्ञानवादी लॉजिक में मूलभूत लॉजिक की दोहरी-नकारात्मक व्याख्या के साथ, यह मूलभूत अंकगणित को अंतर्ज्ञानवादी अंकगणित में कमी प्रदान करता है।

औपचारिक और अनौपचारिक प्रूफ

Main article: औपचारिक प्रूफ

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

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

प्रूफ-सैद्धांतिक शब्दार्थ

Main articles: प्रमाण-सैद्धांतिक शब्दार्थ and तार्किक सद्भाव (हॉर्मोनी)

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

यह भी देखें

• मध्यवर्ती लॉजिक
• मॉडल सिद्धांत
• प्रूफ (सत्य)
• प्रूफ तकनीक
• अनुक्रमिक गणना

संदर्भ

• J. Avigad and E.H. Reck (2001). "'Clarifying the nature of the infinite': the development of metamathematics and proof theory". Carnegie-Mellon Technical Report CMU-PHIL-120.
• J. Barwise, ed. (1978). Handbook of Mathematical Logic. North-Holland.
• S. Buss, ed. (1998) Handbook of Proof Theory. Elsevier.
• G. Gentzen (1935/1969). "Investigations into logical deduction". In M. E. Szabo, ed. Collected Papers of Gerhard Gentzen. North-Holland. Translated by Szabo from "Untersuchungen über das logische Schliessen", Mathematisches Zeitschrift v. 39, pp. 176–210, 405 431.
• J.-Y. Girard, P. Taylor, Y. Lafont (1988). "Proofs and types". Cambridge University Press. ISBN 0-521-37181-3
• D. Prawitz (1965). Natural deduction: A proof-theoretical study, Dover Publications, ISBN 978-0-486-44655-4
• S.G. Simpson (2010). Subsystems of Second-order Arithmetic, second edition. Cambridge University Press, ISBN 978-0521150149.
• A. S. Troelstra and H. Schwichtenberg (1996). Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, ISBN 0-521-77911-1.
• H. Wang (1981). Popular Lectures on Mathematical Logic, Van Nostrand Reinhold Company, ISBN 0-442-23109-1.

बाहरी संबंध

• "Proof theory", Encyclopedia of Mathematics, EMS Press, 2001 [1994]
• J. von Plato (2008). The Development of Proof Theory. Stanford Encyclopedia of Philosophy.