प्रमाण सिद्धांत
प्रमाण सिद्धांत औपचारिक प्रमाणों को उनके अपने गणितीय वस्तुओं के रूप में अध्ययन करता है, उनकी संरचना, परिवर्तनों और उन्हें उत्पन्न करने वाले सिद्धांतों की शक्ति का विश्लेषण करता है।
Definition
प्रमाण सिद्धांत गणितीय तर्कशास्त्र की वह शाखा है जो औपचारिक प्रणालियों में प्रमाणों को परिमित संयोजनात्मक वस्तुओं के रूप में मानती है, यह अध्ययन करती है कि उन्हें कैसे रूपांतरित और सामान्यीकृत किया जा सकता है और उनके अस्तित्व से अंतर्निहित सिद्धांतों की संगति और शक्ति के बारे में क्या पता चलता है।
Scope
यह क्षेत्र प्राकृतिक निगमन (natural deduction) और अनुक्रम कैलकुलस (sequent calculus) जैसे औपचारिक कैलकुलस, कट-एलिमिनेशन (cut-elimination) और सामान्यीकरण (normalization) प्रमेयों, गोडेल के अपूर्णता प्रमेयों, क्रमिक विश्लेषण (ordinal analysis) द्वारा सिद्धांतों की शक्ति के मापन, और प्रमाणों तथा कार्यक्रमों के बीच पत्राचार द्वारा प्रकट किए गए प्रमाणों की रचनात्मक और संगणनात्मक सामग्री को शामिल करता है।
Sub-topics
Core questions
- औपचारिक प्रमाणों को संयोजनात्मक वस्तुओं के रूप में कैसे दर्शाया और हेरफेर किया जा सकता है?
- प्रमाणों में किन चक्करों को व्यवस्थित रूप से हटाया जा सकता है, और इससे क्या पता चलता है?
- एक औपचारिक सिद्धांत अपने बारे में क्या सिद्ध कर सकता है, इसकी अंतर्निहित सीमाएँ क्या हैं?
- एक सिद्धांत की शक्ति को सटीक रूप से कैसे मापा जा सकता है?
Key theories
- कट-एलिमिनेशन प्रमेय
- जेंट्ज़ेन ने दिखाया कि अनुक्रम कैलकुलस में किसी भी प्रमाण को कट नियम के बिना एक में रूपांतरित किया जा सकता है, जिससे सबफॉर्मूला गुण (subformula property) और प्रत्यक्ष संगति परिणाम वाले प्रमाण प्राप्त होते हैं।
- गोडेल के अपूर्णता प्रमेय
- कोई भी सुसंगत औपचारिक सिद्धांत जो अंकगणित को व्यक्त करने के लिए पर्याप्त मजबूत है, उसमें ऐसे सत्य वाक्य होते हैं जिन्हें वह सिद्ध नहीं कर सकता है और अपनी स्वयं की संगति को सिद्ध नहीं कर सकता है, जिससे औपचारिकीकरण पर मौलिक सीमाएँ तय होती हैं।
- करी-हावर्ड पत्राचार
- प्राकृतिक निगमन में प्रमाण टाइप किए गए लैम्डा कैलकुलस (typed lambda calculus) के पदों के अनुरूप होते हैं और प्रमाण सामान्यीकरण संगणना के अनुरूप होता है, जो प्रमाण सिद्धांत को प्रोग्रामिंग भाषाओं के सिद्धांत से जोड़ता है।
Clinical relevance
प्रमाण सिद्धांत गणित में संगति और रचनात्मक सामग्री के विश्लेषण का आधार है और प्रकार सिद्धांत (type theory), कार्यात्मक प्रोग्रामिंग (functional programming) और स्वचालित प्रमाण सहायकों (automated proof assistants) के लिए सैद्धांतिक आधार प्रदान करता है, जहाँ प्रमाण सत्यापन योग्य कार्यक्रमों के रूप में भी कार्य करते हैं।
History
प्रमाण सिद्धांत की स्थापना हिल्बर्ट ने अपने कार्यक्रम के हिस्से के रूप में की थी ताकि परिमित संगति प्रमाणों द्वारा गणित को सुरक्षित किया जा सके। 1931 के गोडेल के अपूर्णता प्रमेयों ने दिखाया कि मूल कार्यक्रम पूरी तरह से सफल नहीं हो सकता है, और जेंट्ज़ेन के कट-एलिमिनेशन और ट्रांसफिनिट इंडक्शन (transfinite induction) के माध्यम से अंकगणित के लिए संगति प्रमाण ने इस क्षेत्र को क्रमिक विश्लेषण और, बाद में, प्रमाण-के-रूप-में-कार्यक्रम (proofs-as-programs) प्रतिमान की ओर निर्देशित किया।
Key figures
- David Hilbert
- Gerhard Gentzen
- Kurt Goedel
- Jean-Yves Girard
Related topics
Seminal works
- troelstra2000
- takeuti1987
- girard1989
Frequently asked questions
- प्रमाण सिद्धांत मॉडल सिद्धांत से कैसे भिन्न है?
- मॉडल सिद्धांत संरचनाओं और उनमें वाक्यों की सत्यता का अध्ययन करता है, जो एक अर्थ संबंधी परिप्रेक्ष्य है, जबकि प्रमाण सिद्धांत औपचारिक व्युत्पत्तियों और उनके वाक्यात्मक परिवर्तनों का अध्ययन करता है। गोडेल का पूर्णता प्रमेय दोनों को जोड़ता है, लेकिन उनकी विधियाँ और प्रश्न भिन्न हैं।
- हिल्बर्ट का कार्यक्रम क्या है?
- यह केवल परिमित, निर्विवाद तर्क का उपयोग करके गणित की सभी संगति को सिद्ध करने का प्रस्ताव था। गोडेल के दूसरे अपूर्णता प्रमेय ने दिखाया कि कोई भी पर्याप्त मजबूत सिद्धांत अपनी स्वयं की संगति को सिद्ध नहीं कर सकता है, इसलिए कार्यक्रम को उसके मूल रूप में पूरा नहीं किया जा सकता है, हालांकि संशोधित संस्करण प्रभावशाली बने हुए हैं।