हेटिंग अंकगणित

गणितीय तर्क में, हेटिंग अंकगणित ${\mathsf {HA}}$ अंतर्ज्ञानवाद के दर्शन के अनुसार अंकगणित का स्वयंसिद्ध है। इसका नाम एंड्रयू हेटिंग के नाम पर रखा गया है, जिन्होंने इसे पहली बार प्रस्तावित किया था।

स्वयंसिद्धीकरण

पहले क्रम के पियानो अंकगणित के साथ ${\mathsf {PA}}$, इस सिद्धांत का इच्छित मॉडल प्राकृतिक संख्या एँ हैं ${\mathbb {N} }$ और सिद्धांत जोड़ और गुणा की विशेषता बताते हैं। हेयटिंग अंकगणित पीनो अंकगणित के सिद्धांतों को अपनाता है, जिसमें शून्य के साथ हस्ताक्षर शामिल हैं$0$और उत्तराधिकारी$S$, लेकिन अनुमान के लिए अंतर्ज्ञानवादी तर्क का उपयोग करता है। विशेष रूप से, बहिष्कृत मध्य का सिद्धांत ${\mathrm {PEM} }$ सामान्य रूप से नहीं रखता।

मेटालॉजिक और प्रमेय

अंतर्ज्ञानवादी तर्क पर अन्य सिद्धांतों के साथ, के विभिन्न उदाहरण ${\mathrm {PEM} }$ सिद्ध किया जा सकता है। उदाहरण के लिए, ${\mathsf {HA}}$ समानता सिद्ध करता है$=$सभी नंबरों के लिए निर्णायक है,

${\mathsf {HA}}\vdash \forall n.\forall m.{\big (}(n=m)\lor \neg (n=m){\big )}$

वास्तव में, चूंकि हेटिंग अंकगणित में समानता ही एकमात्र विधेय (गणित) प्रतीक है, इसलिए यह किसी भी परिमाणक (तर्क) तर्क) -मुक्त सूत्र के लिए इसका अनुसरण करता है। $\phi$, कहां $n,\dots ,m$ में मुक्त चर हैं $\phi$,

${\mathsf {HA}}\vdash \forall n.\cdots \forall m.{\big (}\phi \lor \neg \phi {\big )}$

प्रेरण (गणित) के माध्यम से, असीम रूप से कई गैर-तुच्छ बयान उदाहरण प्राप्त किए जा सकते हैं। वास्तव में, ${\mathsf {PA}}$ अंकगणितीय पदानुक्रम है|$\Pi _{2}^{0}$-रूढ़िवादी खत्म ${\mathsf {HA}}$, जैसा कि फ्रीडमैन अनुवाद के माध्यम से दिखाया गया है। रिकर्सिव के लिए $\varphi$,

${\mathsf {PA}}\vdash \forall n.\exists m.\varphi (n,m)\implies {\mathsf {HA}}\vdash \forall n.\exists m.\varphi (n,m)$

मोटे तौर पर, इसका मतलब यह है कि क्लासिकल अंकगणितीय सिद्धांत में सिद्ध सरल मैपिंग के बारे में सभी कथन रचनात्मक में पहले से ही साबित हो चुके हैं।

इसके अलावा, में साबित किसी भी सूत्र के लिए ${\mathsf {PA}}$, उस सूत्र का शास्त्रीय रूप से समतुल्य गोडेल-जेंटज़ेन नकारात्मक अनुवाद पहले से ही में सिद्ध हो चुका है ${\mathsf {HA}}$. कहने का मतलब यह है कि, सभी पियानो अंकगणितीय प्रमेय में एक प्रमाण होता है जिसमें एक रचनात्मक प्रमाण होता है जिसके बाद शास्त्रीय तार्किक पुनर्लेखन होता है। मोटे तौर पर, अंतिम चरण के प्रकारों के अनुप्रयोगों के लिए होता है $\neg \forall n.\psi (n)\vdash _{\mathsf {PA}}\exists n.\neg \psi (n)$ और दोहरा-नकारात्मक उन्मूलन $\neg \neg \psi \vdash _{\mathsf {PA}}\psi$.

हिल्बर्ट की दसवीं समस्या में अंतर्दृष्टि शास्त्रीय रूप से तुच्छ सिद्ध करने योग्य गणितीय कथन प्रदान करती है, जो नीचे दिए गए प्रत्यक्ष सूत्रीकरण में, रचनात्मक रूप से सिद्ध करने योग्य नहीं है। हिल्बर्ट के प्रश्न का समाधान बताता है कि एक बहुपद है $f$ और एक संगत बहुपद समीकरण जैसे कि यह अनिर्णीत समस्या है कि बाद वाले का कोई हल है या नहीं। निर्णयनीयता को प्रस्ताव के लिए बहिष्कृत मध्य कथन के रूप में व्यक्त किया जा सकता है $\exists n.\cdots \exists m.f(n,\dots ,m)=0$.

संगति

कर्ट गोडेल ने उपरोक्त नकारात्मक अनुवाद पेश किया और साबित किया कि यदि हेटिंग अंकगणित सुसंगत है, तो पीनो अंकगणित भी संगत है। कहने का तात्पर्य यह है कि उसने निरंतरता के कार्य को कम कर दिया ${\mathsf {PA}}$ उसके वहां के लिए ${\mathsf {HA}}$.

हालांकि, गोडेल की अपूर्णता प्रमेय हेटिंग अंकगणित पर भी लागू होती है।

वास्तव में, उन सिद्धांतों की असंगति की खोज को पीआनो अंकगणित में औपचारिक रूप दिया जा सकता है। जैसा कि गोडेल द्वारा स्थापित किया गया है, यदि सिद्धांत सुसंगत है, तो इसमें कोई प्रमाण नहीं है ${\mathsf {PA}}$ कि यह खोज रुकती (सफल) होती है, न ही इसमें कोई प्रमाण है ${\mathsf {PA}}$ कि यह तलाश थम न जाए। फिर भी, में ${\mathsf {PA}}$, एक (शास्त्रीय रूप से तुच्छ और गैर-रचनात्मक) प्रमाण है कि यह खोज या तो रुकती है या नहीं रुकती है।

एंटी-क्लासिकल एक्सटेंशन

संबंधित, विधेय हैं $A$ ऐसा सिद्धांत ${\mathsf {HA}}+{\mathsf {U}}_{A}$ संगत है, कहाँ ${{\mathsf {U}}_{A}}$ है

$\neg \forall n.{\big (}A(n)\lor \neg A(n){\big )}$

संयोजन के रचनात्मक पठन के साथ, यह विधेय के दावे का एक आंतरिक संस्करण है $A$ निर्णय लेने योग्य नहीं है। ध्यान दें कि रचनात्मक रूप से, उपरोक्त किसी विशेष प्रति-उदाहरण के बहिष्कृत मध्य के अस्तित्व के बराबर नहीं है, जैसा कि में है $\exists n.\neg {\big (}A(n)\lor \neg A(n){\big )}$.

दरअसल, पहले से ही न्यूनतम तर्क सभी प्रस्तावों के लिए डबल-नकारात्मक बहिष्कृत मध्य साबित करता है, और इसी तरह $\forall n.\neg \neg {\big (}P(n)\lor \neg P(n))$, जो बराबर है $\neg \exists n.\neg {\big (}P(n)\lor \neg P(n){\big )}$.

हेटिंग अंकगणित में चर्च का नियम एक स्वीकार्य नियम है। चर्च की थीसिस (रचनात्मक गणित) | चर्च के थीसिस सिद्धांत को अपनाया जा सकता है ${\mathsf {HA}}$, जबकि ${\mathsf {PA}}$ इसे अस्वीकार करता है। यह कथन के लिए अनिर्णीत समस्या के कारण है $A$ क्लेन के टी विधेय के विकर्ण के रूप में परिभाषित किया गया है (देखें रुकने की समस्या ), जिसे चर्च का सिद्धांत तब भी उपरोक्त अर्थ में स्थापित करता है।

मॉडल

वास्तविकता

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

उन्होंने यह भी स्थापित किया, अनौपचारिक रूप से यहां व्यक्त किया गया कि यदि

${\mathsf {PA}}\vdash \forall n.\exists m.\varphi (n,m)$

सरल के लिए $\varphi$, में फिर ${\mathsf {HA}}$ एक को साकार करने वाला एक सामान्य पुनरावर्ती कार्य है $m$ प्रत्येक के लिए $n$ ताकि $\varphi (n,m)$. इसे फ़ंक्शन तर्कों की किसी भी परिमित संख्या तक बढ़ाया जा सकता है $n$.

संयोजन और अस्तित्व गुण देखें।

हेटिंग अंकगणित में मार्कोव का नियम एक स्वीकार्य नियम है। जॉर्ज क्रेसेल द्वारा वास्तविकता के टाइप किए गए संस्करणों को पेश किया गया है। इसके साथ उन्होंने अंतर्ज्ञानवादी सिद्धांतों के लिए शास्त्रीय रूप से मान्य मार्कोव के सिद्धांत की स्वतंत्रता का प्रदर्शन किया।

सेट सिद्धांत

पूर्ण के लिए रचनात्मक सेट थ्योरी मॉडल हैं ${\mathsf {HA}}$ और इसके इच्छित शब्दार्थ। अपेक्षाकृत कमजोर सेट सिद्धांत पर्याप्त हैं: वे अंकगणितीय सूत्रों के प्रेरण को साबित करने के लिए अनंतता के स्वयंसिद्ध, विधेय पृथक्करण के स्वयंसिद्ध स्कीमा को अपनाएंगे। $\omega$, साथ ही Recursion#The_recursion_theorem के लिए परिमित डोमेन पर समारोह रिक्त स्थान का अस्तित्व। विशेष रूप से, उन सिद्धांतों की आवश्यकता नहीं है ${\mathrm {PEM} }$, पृथक्करण या एप्सिलॉन प्रेरण का पूर्ण स्वयंसिद्ध (अकेले नियमितता का स्वयंसिद्ध ), और न ही सामान्य कार्य स्थान (अकेले शक्ति सेट का पूर्ण स्वयंसिद्ध)।

${\mathsf {HA}}$ इसके अलावा व्याख्या_(मॉडल_सिद्धांत)#द्वि-व्याख्यात्मकता|द्वि-व्याख्यात्मक एक कमजोर रचनात्मक सेट सिद्धांत के साथ है जिसमें अध्यादेशों का वर्ग है $\omega$, ताकि सिद्धांत में एक सेट के रूप में वॉन न्यूमैन नैचुरल मौजूद न हों। मेटा-सैद्धांतिक रूप से, उस सिद्धांत का डोमेन उसके अध्यादेशों के वर्ग जितना बड़ा होता है और अनिवार्य रूप से कक्षा के माध्यम से दिया जाता है ${\mathrm {Fin} }$ उन सभी सेटों में से जो एक प्राकृतिक के साथ आपत्ति में हैं $n\in \omega$. एक स्वयंसिद्ध के रूप में इसे कहा जाता है $V={\mathrm {Fin} }$ और अन्य स्वयंसिद्ध वे हैं जो सेट बीजगणित और क्रम से संबंधित हैं: संघ और बाइनरी इंटरसेक्शन, जो कि प्रेडीकेटिव सेपरेशन स्कीमा, एक्सटेंशनलिटी, पेयरिंग और एप्सिलॉन इंडक्शन स्कीमा से संबंधित है। यह सिद्धांत तब पहले से ही द्वारा दिए गए सिद्धांत के समान है ${\mathsf {CZF}}$ स्ट्रॉन्ग इन्फिनिटी के बिना और परिमित स्वयंसिद्ध के साथ जोड़ा गया। की चर्चा ${\mathsf {HA}}$ इस सेट सिद्धांत में मॉडल सिद्धांत के समान है। और दूसरी दिशा में, आदिम पुनरावर्ती संबंध के संबंध में सेट सैद्धांतिक स्वयंसिद्ध सिद्ध होते हैं

$x\in y\iff \exists (r<2^{x}).\exists (s<y).{\big (}2^{x}(2s+1)+r=y{\big )}$

सेट के उस छोटे ब्रह्मांड को परिमित बाइनरी संख्या के क्रमबद्ध संग्रह के रूप में समझा जा सकता है जो उनकी पारस्परिक सदस्यता को कूटबद्ध करता है। उदाहरण के लिए, द $100_{2}$वें सेट में एक और सेट होता है और $110101_{2}$वें समुच्चय में चार अन्य समुच्चय हैं। बीआईटी विधेय देखें।

शास्त्रीय प्रथम-क्रम सिद्धांत का मानक मॉडल ${\mathsf {PA}}$ साथ ही साथ इसका कोई भी गैर-मानक मॉडल हेटिंग अंकगणित के लिए भी एक मॉडल है ${\mathsf {HA}}$. का कोई सुसंगत पुनरावर्ती विस्तार ${\mathsf {ZF}}$ लोवेनहेम-स्कोलेम प्रमेय के गैर-मानक मॉडल द्वारा फिर से एकरमैन कोडिंग के माध्यम से भी मॉडलिंग की जाती है ${\mathsf {PA}}$ - हालाँकि, जिस तरह वाक्य-विन्यास अंकगणितीय सिद्धांत स्वयं संख्याओं की गैर-मानकता के बारे में नहीं जान सकता है, वह इस तरह के शब्दार्थों में सेटों की अनंतता के बारे में नहीं जानता है।

प्रकार सिद्धांत

सबूत सहायक में इंट्रेंस रूल्स पर आधारित लॉजिक औपचारिकताओं को प्रतिबिंबित करने वाले आश्रित प्रकार रियलाइजेशन को लागू किया गया है।

एक्सटेंशन

के कई टाइप किए गए एक्सटेंशन ${\mathsf {HA}}$ सबूत सिद्धांत में बड़े पैमाने पर अध्ययन किया गया है, उदा। समारोह प्रकार के साथ।

प्रारंभ में, गहन समानता और शराब की भठ्ठी पसंद अनुक्रम वाले वेरिएंट की जांच की गई।

इतिहास

सिद्धांत का औपचारिक स्वयंसिद्धीकरण हेटिंग (1930), जैक्स हर्ब्रांड और क्लेन तक वापस जाता है। गोडेल ने संबंधित परिणाम को साबित कर दिया ${\mathsf {PA}}$ 1933 में।

संबंधित अवधारणाएं

हेटिंग अंकगणित को हेयटिंग बीजगणित के साथ भ्रमित नहीं होना चाहिए, जो बूलियन बीजगणित (संरचना) के अंतर्ज्ञानवादी एनालॉग हैं।

यह भी देखें

• बीएचके व्याख्या
• रचनात्मक विश्लेषण
• रचनात्मक सेट सिद्धांत
• हैरोप सूत्र
• वास्तविकता

संदर्भ

• Ulrich Kohlenbach (2008), Applied proof theory, Springer.
• Anne S. Troelstra, ed. (1973), Metamathematical investigation of intuitionistic arithmetic and analysis, Springer, 1973.

इस पेज में लापता आंतरिक लिंक की सूची

• सहज-ज्ञान
• फ्राइडमैन अनुवाद
• डबल-निषेध उन्मूलन
• वसूली
• क्लीन
• रचनात्मक सेट सिद्धांत
• अनंत का स्वयंसिद्ध
• विधेय पृथक्करण की स्वयंसिद्ध स्कीमा
• शक्ति सेट का स्वयंसिद्ध
• जुदाई का स्वयंसिद्ध
• बिट विधेय
• गैर मानक मॉडल
• पसंद का क्रम
• आकस्मिक समानता
• हेटिंग बीजगणित

बाहरी कड़ियाँ

• Stanford Encyclopedia of Philosophy: "Intuitionistic Number Theory" by Joan Moschovakis.
• Fragments of Heyting Arithmetic by Wolfgang Burr