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

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

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

इतिहास

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1-CA₀ की संगति का प्रमाण ¹
₁ह₀ क्रमिक आरेखों की विधि का उपयोग करना है।

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

Main article: Provability logic

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

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

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

उल्टा गणित

Main article: Reverse mathematics

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

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

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

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

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

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

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

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

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

औपचारिक और अनौपचारिक प्रमाण

Main article: Formal proof

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

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

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

Main articles: Proof-theoretic semantics and Logical harmony

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

यह भी देखें

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

संदर्भ

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