ब्रौवर-हेटिंग-कोलमोगोरोव व्याख्या

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

व्याख्या

व्याख्या बताती है कि किसी दिए गए सूत्रों (गणितीय तर्क) का प्रमाण क्या होना चाहिए। यह उस सूत्र की संरचना पर प्रेरण द्वारा निर्दिष्ट किया गया है:

• $P\wedge Q$ का प्रमाण एक जोड़ी $\langle a,b\rangle$ है जहां $a$, $P$का प्रमाण है और $b$, $Q$ का प्रमाण है।
• इसका एक प्रमाण $P\vee Q$ भी है $\langle 0,a\rangle$ जहाँ $a$ का प्रमाण है $P$ या $\langle 1,b\rangle$ जहाँ $b$ ,$Q$ का प्रमाण है .
• इसका एक प्रमाण $P\to Q$ एक फलन है $f$ जो एक प्रमाण को परिवर्तित करता है $P$ , $Q$ के प्रमाण में है
• इसका एक प्रमाण $(\exists x{\in }S)(Px)$ एक जोड़ी है $\langle x,a\rangle$ जहाँ $x$ का एक तत्व है $S$ और $a$, $Px$ का प्रमाण है
• इसका एक प्रमाण $(\forall x{\in }S)(Px)$ एक फलन है $f$ जो एक तत्व को परिवर्तित करता है $x$ का $S$, $Px$ के प्रमाण में है
• सूत्र $\neg P$ को $P\to \bot$ के रूप में परिभाषित किया गया है, इसलिए इसका एक प्रमाण एक फलन $f$ है जो $P$ के प्रमाण को $\bot$ के प्रमाण में परिवर्तित करता है।
• $\bot$ असंगति या निचला प्रकार (कुछ प्रोग्रामिंग भाषाओं में नॉनटर्मिनेशन) का कोई प्रमाण नहीं है।

किसी प्राचीन प्रस्ताव की व्याख्या संदर्भ से ज्ञात होनी चाहिए। अंकगणित के सन्दर्भ में सूत्र का एक प्रमाण $x=y$ यह दो पदों को एक ही अंक में घटाने वाली एक गणना है।

कोलमोगोरोव ने भी उसी पंक्ति का अनुसरण किया किंतु अपनी व्याख्या को समस्याओं और समाधानों के संदर्भ में व्यक्त किया। किसी सूत्र पर ज़ोर देना उस सूत्र द्वारा प्रस्तुत समस्या का समाधान जानने का प्रमाणित करना है। उदाहरण के लिए $P\to Q$, $Q$ को $P$; तक कम करने की समस्या है; इसे हल करने के लिए समस्या को हल करने के लिए एक विधि की आवश्यकता है $Q$ ने समस्या $P$ का समाधान दिया है।

उदाहरण

पहचान फलन सूत्र $P\to P$ का प्रमाण है, या फिर P कुछ भी हो।

गैर-विरोधाभास का नियम $\neg (P\wedge \neg P)$ का विस्तार $(P\wedge (P\to \bot ))\to \bot$ तक होता है:

• $(P\wedge (P\to \bot ))\to \bot$ का एक प्रमाण एक फलन $f$ है जो $(P\wedge (P\to \bot ))$ के प्रमाण को $\bot$ के प्रमाण में परिवर्तित करता है।
• $(P\wedge (P\to \bot ))$ का एक प्रमाण, प्रमाणों की एक जोड़ी है <a, b>, जहां a, P का प्रमाण है, और b, $P\to \bot$ का प्रमाण है।
• $P\to \bot$ का प्रमाण एक फलन है जो P के प्रमाण को $\bot$ के प्रमाण में परिवर्तित करता है।

इन सबको एक साथ रखने पर, $(P\wedge (P\to \bot ))\to \bot$ का एक प्रमाण एक फलन $f$ है जो एक जोड़ी <a, b> को परिवर्तित करता है - जहां a, P का प्रमाण है, और b एक फलन है जो P के प्रमाण को $\bot$ के प्रमाण में -$\bot$ के प्रमाण में परिवर्तित करता है। एक फलन $f$ है जो ऐसा करता है, जहां $f(\langle a,b\rangle )=b(a)$, गैर-विरोधाभास के नियम को सिद्ध करता है, चाहे P कुछ भी हो।

इसलिए विचार की यही पंक्ति $(P\wedge (P\to Q))\to Q$ के लिए भी एक प्रमाण प्रदान करती है, जहां $Q$ कोई प्रस्ताव है।

दूसरी ओर, बहिष्कृत मध्य $P\vee (\neg P)$ का नियम $P\vee (P\to \bot )$ तक विस्तारित होता है, और सामान्य रूप से इसका कोई प्रमाण नहीं है। व्याख्या के अनुसार, $P\vee (\neg P)$ का एक प्रमाण एक युग्म <a, b> है जहां a 0 है और b, P का प्रमाण है, या a 1 है और b, $P\to \bot$ का प्रमाण है। इस प्रकार यदि न तो P और न ही $P\to \bot$ सिद्ध है तो दोनों में से कोई भी $P\vee (\neg P)$ नहीं है।

असंगति की परिभाषा

सामान्य रूप से, एक तार्किक प्रणाली के लिए औपचारिक निषेध ऑपरेटर का होना संभव नहीं है, जैसे कि "नहीं" $P$ का प्रमाण हो, जब $P$ का कोई प्रमाण न हो; गोडेल की अपूर्णता प्रमेय देखें। बीएचके की व्याख्या इसके अतिरिक्त "नहीं" $P$ लेती है, जिसका अर्थ यह है कि $P$ असंगति की ओर ले जाता है, जिसे $\bot$ नामित किया गया है, जिससे नहीं $\lnot P$ का प्रमाण, $P$ के प्रमाण को असंगति के प्रमाण में परिवर्तित करने वाला एक कार्य होता है ।

अंकगणित से निपटने में असंगति का एक मानक उदाहरण पाया जाता है। मान लें कि 0 = 1, और गणितीय प्रेरण द्वारा आगे बढ़ें: 0 = 0 समानता के सिद्धांत द्वारा अब (आगमन परिकल्पना), यदि 0 एक निश्चित प्राकृतिक संख्या n के समान होता, तो 1 n + 1 के समान होता, (पीनो अंकगणित: 'S'm' = 'S'n यदि और केवल यदि m = n), किंतु चूँकि 0 = 1, इसलिए 0 भी n+ 1 के समान होगा। प्रेरण द्वारा, 0 सभी संख्याओं के समान है, और इसलिए कोई भी दो प्राकृतिक संख्याएँ समान हो जाती हैं।

इसलिए, 0 = 1 के प्रमाण से किसी मूलभूत अंकगणितीय समानता के प्रमाण तक, और इस प्रकार किसी भी समष्टि अंकगणितीय प्रस्ताव के प्रमाण तक जाने का एक विधि है। इसके अतिरिक्त , इस परिणाम को प्राप्त करने के लिए पीनो सिद्धांत को प्रयुक्त करना आवश्यक नहीं था जो बताता है कि 0 किसी भी प्राकृतिक संख्या का उत्तराधिकारी नहीं है। यह हेटिंग अंकगणित में 0 = 1 को $\bot$ के रूप में उपयुक्त बनाता है (और पीनो स्वयंसिद्ध को 0 = Sn → 0 = S0 को फिर से लिखा गया है)। 0 = 1 का यह प्रयोग विस्फोट के सिद्धांत को मान्य करता है।

फलन की परिभाषा

बीएचके की व्याख्या उस दृष्टिकोण पर निर्भर करेगी जो एक फलन का गठन करता है जो एक प्रमाण को दूसरे में परिवर्तित करता है, या जो एक डोमेन के एक तत्व को प्रमाण में परिवर्तित करता है। रचनावाद (गणित) के विभिन्न संस्करण इस बिंदु पर भिन्न होंगे।

क्लेन का यथार्थता सिद्धांत गणना योग्य कार्य के साथ कार्यों की पहचान करता है। यह हेयटिंग अंकगणित से संबंधित है, जहां परिमाणीकरण का क्षेत्र प्राकृतिक संख्याएं हैं और प्राचीन प्रस्ताव x = y के रूप में हैं। यदि x उसी संख्या पर मूल्यांकन करता है जो y करता है (जो प्राकृतिक संख्याओं के लिए सदैव निर्णय लेने योग्य होता है), तो x = y का प्रमाण केवल तुच्छ एल्गोरिथ्म है, अन्यथा कोई प्रमाण नहीं है। इन्हें फिर अधिक समष्टि एल्गोरिदम में सम्मिलित करके बनाया जाता है।

यदि कोई फलन की धारणा को परिभाषित करने के लिए लैम्ब्डा कैलकुलस लेता है, तो बीएचके व्याख्या प्राकृतिक कमी और कार्यों के बीच करी-हावर्ड पत्राचार का वर्णन करती है।

संदर्भ

• Troelstra, A. (1991). "History of Constructivism in the Twentieth Century" (PDF).
• Troelstra, A. (2003). "Constructivism and Proof Theory (draft)". CiteSeerX 10.1.1.10.6972.