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

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

व्याख्या

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

• इसका एक प्रमाण $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 का प्रमाण है $P\to \bot$. इस प्रकार यदि न तो पी और न ही $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.