असमान नींव: Difference between revisions

From Vigyanwiki
(Created page with "असमान नींव गणित की नींव के लिए एक दृष्टिकोण है जिसमें गणितीय संर...")
 
No edit summary
Line 1: Line 1:
असमान नींव [[गणित की नींव]] के लिए एक दृष्टिकोण है जिसमें गणितीय [[संरचनावाद (गणित का दर्शन)]] 'प्रकार' नामक वस्तुओं से निर्मित होता है। असमान नींव के प्रकार सेट-सैद्धांतिक नींव में बिल्कुल किसी भी चीज़ के अनुरूप नहीं होते हैं, लेकिन उन्हें रिक्त स्थान के रूप में सोचा जा सकता है, [[होमोटॉपी]] समकक्ष रिक्त स्थान के समान समान प्रकार के साथ और एक पथ से जुड़े स्थान के बिंदुओं के समान प्रकार के समान तत्वों के साथ। . यूनिवेलेंट फ़ाउंडेशन गणित के पुराने दर्शनशास्त्र #[[हरमन ग्रासमैन]] और [[जॉर्ज कैंटर]] के प्लैटोनिज़्म विचारों और [[अलेक्जेंडर ग्रोथेंडिक]] की शैली में [[श्रेणी सिद्धांत]] गणित दोनों से प्रेरित हैं। अंतर्निहित औपचारिक कटौती प्रणाली के रूप में शास्त्रीय [[विधेय तर्क]] के उपयोग से असमान नींव (हालांकि इसके साथ भी संगत) निकलती है, इस समय इसे मार्टिन-लोफ प्रकार के सिद्धांत के एक संस्करण के साथ बदल दिया जाता है। असमान नींव का विकास होमोटॉपी प्रकार के सिद्धांत के विकास से निकटता से संबंधित है।
असमान नींव [[गणित की नींव]] के लिए दृष्टिकोण है जिसमें गणितीय [[संरचनावाद (गणित का दर्शन)]] 'प्रकार' नामक वस्तुओं से निर्मित होता है। असमान नींव के प्रकार सेट-सैद्धांतिक नींव में बिल्कुल किसी भी चीज़ के अनुरूप नहीं होते हैं, लेकिन उन्हें रिक्त स्थान के रूप में सोचा जा सकता है, [[होमोटॉपी]] समकक्ष रिक्त स्थान के समान समान प्रकार के साथ और पथ से जुड़े स्थान के बिंदुओं के समान प्रकार के समान तत्वों के साथ। . यूनिवेलेंट फ़ाउंडेशन गणित के पुराने दर्शनशास्त्र #[[हरमन ग्रासमैन]] और [[जॉर्ज कैंटर]] के प्लैटोनिज़्म विचारों और [[अलेक्जेंडर ग्रोथेंडिक]] की शैली में [[श्रेणी सिद्धांत]] गणित दोनों से प्रेरित हैं। अंतर्निहित औपचारिक कटौती प्रणाली के रूप में शास्त्रीय [[विधेय तर्क]] के उपयोग से असमान नींव (हालांकि इसके साथ भी संगत) निकलती है, इस समय इसे मार्टिन-लोफ प्रकार के सिद्धांत के संस्करण के साथ बदल दिया जाता है। असमान नींव का विकास होमोटॉपी प्रकार के सिद्धांत के विकास से निकटता से संबंधित है।


यदि गणितीय संरचना की एक उपयुक्त (अर्थात, श्रेणीबद्ध) धारणा को अपनाया जाता है, तो असमान नींव संरचनावाद (गणित के दर्शन) के अनुकूल हैं।<ref>{{Cite journal|url = https://www.andrew.cmu.edu/user/awodey/preprints/siu.pdf|title = संरचनावाद, अपरिवर्तनीयता और एकरूपता|last = Awodey|first = Steve|journal = [[Philosophia Mathematica]] |doi = 10.1093/philmat/nkt030|author-link = Steve Awodey|volume = 22|issue = 1|pages = 1–11|year = 2014 |citeseerx = 10.1.1.691.8113}}</ref>
यदि गणितीय संरचना की उपयुक्त (अर्थात, श्रेणीबद्ध) धारणा को अपनाया जाता है, तो असमान नींव संरचनावाद (गणित के दर्शन) के अनुकूल हैं।<ref>{{Cite journal|url = https://www.andrew.cmu.edu/user/awodey/preprints/siu.pdf|title = संरचनावाद, अपरिवर्तनीयता और एकरूपता|last = Awodey|first = Steve|journal = [[Philosophia Mathematica]] |doi = 10.1093/philmat/nkt030|author-link = Steve Awodey|volume = 22|issue = 1|pages = 1–11|year = 2014 |citeseerx = 10.1.1.691.8113}}</ref>




== इतिहास ==
== इतिहास ==


2006 से 2009 के दौरान [[ व्लादिमीर वोवोडस्की ]] द्वारा एकतरफा नींव के मुख्य विचार तैयार किए गए थे। एकतरफा नींव और पहले के विचारों के बीच दार्शनिक संबंधों के लिए एकमात्र संदर्भ वोवोडस्की के 2014 बर्नेज़ व्याख्यान हैं।<ref>{{cite journal |first=Vladimir |last=Voevodsky |title=Foundations of mathematics — their past, present and future |journal=The 2014 Paul Bernays Lectures |location=ETH Zurich |date=September 9–10, 2014}} See item 11 at [https://www.math.ias.edu/vladimir/lectures Voevodsky Lectures]</ref> एकरूपता नाम वोवोडस्की के कारण है।<ref>[https://ncatlab.org/nlab/show/univalence+axiom univalence axiom in nLab]</ref><ref name= Escardo >Martín Hötzel Escardó (October 18, 2018) [https://arxiv.org/pdf/1803.02294.pdf A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom]</ref> कुछ विचारों के इतिहास की एक अधिक विस्तृत चर्चा, जो वर्तमान स्थिति में एकतरफा नींव में योगदान करती है, होमोटॉपी टाइप थ्योरी (होमोटॉपी टाइप थ्योरी) पर पृष्ठ पर पाई जा सकती है।
2006 से 2009 के दौरान [[ व्लादिमीर वोवोडस्की |व्लादिमीर वोवोडस्की]] द्वारा एकतरफा नींव के मुख्य विचार तैयार किए गए थे। एकतरफा नींव और पहले के विचारों के बीच दार्शनिक संबंधों के लिए एकमात्र संदर्भ वोवोडस्की के 2014 बर्नेज़ व्याख्यान हैं।<ref>{{cite journal |first=Vladimir |last=Voevodsky |title=Foundations of mathematics — their past, present and future |journal=The 2014 Paul Bernays Lectures |location=ETH Zurich |date=September 9–10, 2014}} See item 11 at [https://www.math.ias.edu/vladimir/lectures Voevodsky Lectures]</ref> एकरूपता नाम वोवोडस्की के कारण है।<ref>[https://ncatlab.org/nlab/show/univalence+axiom univalence axiom in nLab]</ref><ref name= Escardo >Martín Hötzel Escardó (October 18, 2018) [https://arxiv.org/pdf/1803.02294.pdf A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom]</ref> कुछ विचारों के इतिहास की अधिक विस्तृत चर्चा, जो वर्तमान स्थिति में एकतरफा नींव में योगदान करती है, होमोटॉपी टाइप थ्योरी (होमोटॉपी टाइप थ्योरी) पर पृष्ठ पर पाई जा सकती है।


असमान नींवों की एक मूलभूत विशेषता यह है कि वे - जब मार्टिन-लोफ प्रकार के सिद्धांत (मार्टिन-लोफ प्रकार के सिद्धांत) के साथ संयुक्त होते हैं - आधुनिक गणित की औपचारिकता के लिए एक व्यावहारिक प्रणाली प्रदान करते हैं। इस प्रणाली और Coq (प्रूफ असिस्टेंट) और Agda (प्रोग्रामिंग लैंग्वेज) जैसे आधुनिक प्रूफ सहायकों का उपयोग करके गणित की काफी मात्रा को औपचारिक रूप दिया गया है। फाउंडेशन नामक इस तरह की पहली लाइब्रेरी 2010 में व्लादिमीर वोएवोडस्की द्वारा बनाई गई थी।<ref>Foundations library, see https://github.com/vladimirias/Foundations</ref> अब फ़ाउंडेशन एक बड़े विकास का एक हिस्सा है जिसमें कई लेखक हैं जिन्हें [[यूनीमैथ]] कहा जाता है।<ref>UniMath library, see https://github.com/UniMath/UniMath</ref> फाउंडेशन ने औपचारिक गणित के अन्य पुस्तकालयों को भी प्रेरित किया, जैसे कि HoTT Coq पुस्तकालय<ref>HoTT Coq library, see https://github.com/HoTT/HoTT</ref> और हॉट आज़ाद लाइब्रेरी,<ref>HoTT Agda library, see https://github.com/HoTT/HoTT-Agda</ref> जिसने नई दिशाओं में असमान विचारों को विकसित किया।
असमान नींवों की मूलभूत विशेषता यह है कि वे - जब मार्टिन-लोफ प्रकार के सिद्धांत (मार्टिन-लोफ प्रकार के सिद्धांत) के साथ संयुक्त होते हैं - आधुनिक गणित की औपचारिकता के लिए व्यावहारिक प्रणाली प्रदान करते हैं। इस प्रणाली और Coq (प्रूफ असिस्टेंट) और Agda (प्रोग्रामिंग लैंग्वेज) जैसे आधुनिक प्रूफ सहायकों का उपयोग करके गणित की काफी मात्रा को औपचारिक रूप दिया गया है। फाउंडेशन नामक इस तरह की पहली लाइब्रेरी 2010 में व्लादिमीर वोएवोडस्की द्वारा बनाई गई थी।<ref>Foundations library, see https://github.com/vladimirias/Foundations</ref> अब फ़ाउंडेशन बड़े विकास का हिस्सा है जिसमें कई लेखक हैं जिन्हें [[यूनीमैथ]] कहा जाता है।<ref>UniMath library, see https://github.com/UniMath/UniMath</ref> फाउंडेशन ने औपचारिक गणित के अन्य पुस्तकालयों को भी प्रेरित किया, जैसे कि HoTT Coq पुस्तकालय<ref>HoTT Coq library, see https://github.com/HoTT/HoTT</ref> और हॉट आज़ाद लाइब्रेरी,<ref>HoTT Agda library, see https://github.com/HoTT/HoTT-Agda</ref> जिसने नई दिशाओं में असमान विचारों को विकसित किया।


यूनीवैलेंट फ़ाउंडेशन के लिए एक महत्वपूर्ण मील का पत्थर थिएरी कोक्वांड द्वारा किया गया सेमिनायर निकोलस बॉरबाकी टॉक था<ref>Coquand's Bourbaki Lecture [http://www.cse.chalmers.se/~coquand/paperbourbaki.pdf Paper] and [http://www.cse.chalmers.se/~coquand/bourbaki.pdf Video]</ref> जून 2014 में।
यूनीवैलेंट फ़ाउंडेशन के लिए महत्वपूर्ण मील का पत्थर थिएरी कोक्वांड द्वारा किया गया सेमिनायर निकोलस बॉरबाकी टॉक था<ref>Coquand's Bourbaki Lecture [http://www.cse.chalmers.se/~coquand/paperbourbaki.pdf Paper] and [http://www.cse.chalmers.se/~coquand/bourbaki.pdf Video]</ref> जून 2014 में।


== मुख्य अवधारणाएँ ==
== मुख्य अवधारणाएँ ==
Line 16: Line 16:
उच्च श्रेणी के सिद्धांत के आधार पर गणित की नींव बनाने के कुछ प्रयासों से असमान नींव उत्पन्न हुई। असमान नींवों के निकटतम पहले के विचार वे विचार थे जिन्हें [[माइकल मक्काई]] 'आश्रित प्रकारों के साथ प्रथम-क्रम तर्क' (FOLDS) को दर्शाता है।<ref>{{cite web |title=डिपेंडेंट सॉर्ट के साथ फर्स्ट ऑर्डर लॉजिक, श्रेणी सिद्धांत के अनुप्रयोगों के साथ|first=M. |last=Makkai |year=1995 |work=FOLDS |url=http://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf}}</ref> असमान नींव और मक्काई द्वारा परिकल्पित नींव के बीच मुख्य अंतर यह मान्यता है कि सेट के उच्च आयामी एनालॉग [[अनंत समूह]] के अनुरूप होते हैं और श्रेणियों को आंशिक रूप से_ऑर्डर_सेट के उच्च-आयामी एनालॉग के रूप में माना जाना चाहिए।
उच्च श्रेणी के सिद्धांत के आधार पर गणित की नींव बनाने के कुछ प्रयासों से असमान नींव उत्पन्न हुई। असमान नींवों के निकटतम पहले के विचार वे विचार थे जिन्हें [[माइकल मक्काई]] 'आश्रित प्रकारों के साथ प्रथम-क्रम तर्क' (FOLDS) को दर्शाता है।<ref>{{cite web |title=डिपेंडेंट सॉर्ट के साथ फर्स्ट ऑर्डर लॉजिक, श्रेणी सिद्धांत के अनुप्रयोगों के साथ|first=M. |last=Makkai |year=1995 |work=FOLDS |url=http://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf}}</ref> असमान नींव और मक्काई द्वारा परिकल्पित नींव के बीच मुख्य अंतर यह मान्यता है कि सेट के उच्च आयामी एनालॉग [[अनंत समूह]] के अनुरूप होते हैं और श्रेणियों को आंशिक रूप से_ऑर्डर_सेट के उच्च-आयामी एनालॉग के रूप में माना जाना चाहिए।


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


मार्टिन-लोफ प्रकार के सिद्धांत और उसके वंश जैसे आगमनात्मक निर्माणों के कलन पर आधारित असमान नींव के लिए औपचारिकता प्रणाली में, सेट के उच्च आयामी एनालॉग्स को प्रकारों द्वारा दर्शाया जाता है। प्रकार का संग्रह एच-स्तर (या होमोटोपी स्तर) की अवधारणा द्वारा स्तरीकृत है।<ref name=PW>See {{harvnb|Pelayo|Warren|2014|p=611}}</ref>
मार्टिन-लोफ प्रकार के सिद्धांत और उसके वंश जैसे आगमनात्मक निर्माणों के कलन पर आधारित असमान नींव के लिए औपचारिकता प्रणाली में, सेट के उच्च आयामी एनालॉग्स को प्रकारों द्वारा दर्शाया जाता है। प्रकार का संग्रह एच-स्तर (या होमोटोपी स्तर) की अवधारणा द्वारा स्तरीकृत है।<ref name=PW>See {{harvnb|Pelayo|Warren|2014|p=611}}</ref>
एच-स्तर 0 के प्रकार वे हैं जो एक बिंदु प्रकार के बराबर हैं। उन्हें संविदात्मक प्रकार भी कहा जाता है।
एच-स्तर 0 के प्रकार वे हैं जो बिंदु प्रकार के बराबर हैं। उन्हें संविदात्मक प्रकार भी कहा जाता है।


एच-स्तर 1 के प्रकार वे हैं जिनमें कोई भी दो तत्व समान हैं। इस तरह के प्रकारों को असमान नींव में प्रस्ताव कहा जाता है।<ref name=PW/>एच-लेवल के संदर्भ में प्रस्तावों की परिभाषा अवोडी और बाउर द्वारा पहले सुझाई गई परिभाषा से सहमत है।<ref>{{cite journal |last1=Awodey |first1=Steven |last2=Bauer |first2=Andrej |title=Propositions as [types] |journal=J. Log. Comput. |volume=14
एच-स्तर 1 के प्रकार वे हैं जिनमें कोई भी दो तत्व समान हैं। इस तरह के प्रकारों को असमान नींव में प्रस्ताव कहा जाता है।<ref name=PW/>एच-लेवल के संदर्भ में प्रस्तावों की परिभाषा अवोडी और बाउर द्वारा पहले सुझाई गई परिभाषा से सहमत है।<ref>{{cite journal |last1=Awodey |first1=Steven |last2=Bauer |first2=Andrej |title=Propositions as [types] |journal=J. Log. Comput. |volume=14
|year=2004 |issue=4 |pages=447–471 |doi=10.1093/logcom/14.4.447 |url=http://repository.cmu.edu/philosophy/67/}}</ref> इसलिए, जबकि सभी प्रस्ताव प्रकार हैं, सभी प्रकार तर्क-वाक्य नहीं हैं। प्रस्ताव होना एक प्रकार का गुण है जिसके लिए प्रमाण की आवश्यकता होती है। उदाहरण के लिए, असमान नींव में पहला मौलिक निर्माण iscontr कहलाता है। यह प्रकार से प्रकार का एक कार्य है। यदि X एक प्रकार है तो iscontr X एक प्रकार है जिसमें एक वस्तु है यदि और केवल यदि X संविदात्मक है। यह एक प्रमेय है (जिसे यूनीमैथ लाइब्रेरी में, isapropiscontr कहा जाता है) कि किसी भी X के लिए प्रकार iscontr X का h-स्तर 1 है और इसलिए एक संविदात्मक प्रकार एक संपत्ति है। गुणों के बीच यह अंतर जो एच-लेवल 1 के प्रकार की वस्तुओं द्वारा देखा जाता है और संरचनाएं जो उच्च एच-स्तर के प्रकार की वस्तुओं द्वारा देखी जाती हैं, एकतरफा नींव में बहुत महत्वपूर्ण हैं।
|year=2004 |issue=4 |pages=447–471 |doi=10.1093/logcom/14.4.447 |url=http://repository.cmu.edu/philosophy/67/}}</ref> इसलिए, जबकि सभी प्रस्ताव प्रकार हैं, सभी प्रकार तर्क-वाक्य नहीं हैं। प्रस्ताव होना प्रकार का गुण है जिसके लिए प्रमाण की आवश्यकता होती है। उदाहरण के लिए, असमान नींव में पहला मौलिक निर्माण iscontr कहलाता है। यह प्रकार से प्रकार का कार्य है। यदि X प्रकार है तो iscontr X प्रकार है जिसमें वस्तु है यदि और केवल यदि X संविदात्मक है। यह प्रमेय है (जिसे यूनीमैथ लाइब्रेरी में, isapropiscontr कहा जाता है) कि किसी भी X के लिए प्रकार iscontr X का h-स्तर 1 है और इसलिए संविदात्मक प्रकार संपत्ति है। गुणों के बीच यह अंतर जो एच-लेवल 1 के प्रकार की वस्तुओं द्वारा देखा जाता है और संरचनाएं जो उच्च एच-स्तर के प्रकार की वस्तुओं द्वारा देखी जाती हैं, एकतरफा नींव में बहुत महत्वपूर्ण हैं।


एच-लेवल 2 के प्रकार को सेट कहा जाता है।<ref name=PW/>यह एक प्रमेय है कि प्राकृतिक संख्याओं के प्रकार में एच-स्तर 2 (यूनिमैथ में आईससेटनेट) होता है। असमान नींव के रचनाकारों द्वारा यह दावा किया जाता है कि मार्टिन-लोफ प्रकार के सिद्धांत में सेटों का असमान औपचारिकता सेट-सैद्धांतिक गणित, रचनात्मक और शास्त्रीय दोनों के सभी पहलुओं के बारे में औपचारिक तर्क के लिए वर्तमान में उपलब्ध सर्वोत्तम वातावरण है।<ref>{{harvnb|Voevodsky|2014|loc=Lecture 3, slide 11}}</ref>
एच-लेवल 2 के प्रकार को सेट कहा जाता है।<ref name=PW/>यह प्रमेय है कि प्राकृतिक संख्याओं के प्रकार में एच-स्तर 2 (यूनिमैथ में आईससेटनेट) होता है। असमान नींव के रचनाकारों द्वारा यह दावा किया जाता है कि मार्टिन-लोफ प्रकार के सिद्धांत में सेटों का असमान औपचारिकता सेट-सैद्धांतिक गणित, रचनात्मक और शास्त्रीय दोनों के सभी पहलुओं के बारे में औपचारिक तर्क के लिए वर्तमान में उपलब्ध सर्वोत्तम वातावरण है।<ref>{{harvnb|Voevodsky|2014|loc=Lecture 3, slide 11}}</ref>
श्रेणियों को एक अतिरिक्त संरचना के साथ एच-लेवल 3 के प्रकार के रूप में परिभाषित किया गया है (यूनीमैथ में RezkCompletion लाइब्रेरी देखें) जो एच-लेवल 2 के प्रकारों पर संरचना के समान है जो आंशिक रूप से ऑर्डर किए गए सेट को परिभाषित करता है। असमान नींव में श्रेणियों का सिद्धांत सेट-सैद्धांतिक दुनिया में श्रेणियों के सिद्धांत की तुलना में कुछ अलग और समृद्ध है, जिसमें प्रमुख नए भेद पूर्व-श्रेणियों और श्रेणियों के बीच हैं।<ref>See {{cite journal |first1=Benedikt |last1=Ahrens |first2=Chris |last2=Kapulkin |first3=Michael |last3=Shulman |title=Univalent categories and the Rezk completion |journal=Mathematical Structures in Computer Science |year=2015 |volume=25 |issue=5 |pages=1010–1039 |doi=10.1017/S0960129514000486 |arxiv=1303.0584|s2cid=1135785 }}</ref>
श्रेणियों को अतिरिक्त संरचना के साथ एच-लेवल 3 के प्रकार के रूप में परिभाषित किया गया है (यूनीमैथ में RezkCompletion लाइब्रेरी देखें) जो एच-लेवल 2 के प्रकारों पर संरचना के समान है जो आंशिक रूप से ऑर्डर किए गए सेट को परिभाषित करता है। असमान नींव में श्रेणियों का सिद्धांत सेट-सैद्धांतिक दुनिया में श्रेणियों के सिद्धांत की तुलना में कुछ अलग और समृद्ध है, जिसमें प्रमुख नए भेद पूर्व-श्रेणियों और श्रेणियों के बीच हैं।<ref>See {{cite journal |first1=Benedikt |last1=Ahrens |first2=Chris |last2=Kapulkin |first3=Michael |last3=Shulman |title=Univalent categories and the Rezk completion |journal=Mathematical Structures in Computer Science |year=2015 |volume=25 |issue=5 |pages=1010–1039 |doi=10.1017/S0960129514000486 |arxiv=1303.0584|s2cid=1135785 }}</ref>
थिएरी कोक्वांड द्वारा एक ट्यूटोरियल में असमान नींव के मुख्य विचारों और रचनात्मक गणित के साथ उनके संबंध का लेखा-जोखा पाया जा सकता है।{{efn|Thierry Coquand (2014) Univalent Foundation and Constructive
थिएरी कोक्वांड द्वारा ट्यूटोरियल में असमान नींव के मुख्य विचारों और रचनात्मक गणित के साथ उनके संबंध का लेखा-जोखा पाया जा सकता है।{{efn|Thierry Coquand (2014) Univalent Foundation and Constructive
Mathematics<ref>Coquand (2014) [http://www.cse.chalmers.se/~coquand/ober3.pdf  part 1]</ref> <ref>Coquand (2014) [http://www.cse.chalmers.se/~coquand/ober4.pdf part 2]</ref>}} अल्वारो पेलायो और माइकल वारेन द्वारा 2014 की समीक्षा में शास्त्रीय गणित के परिप्रेक्ष्य से मुख्य विचारों की प्रस्तुति देखी जा सकती है,<ref>{{cite journal |first1=Álvaro |last1=Pelayo |first2=Michael A. |last2=Warren |title=होमोटोपी प्रकार का सिद्धांत और वोवोडस्की की असमान नींव|journal=Bulletin of the American Mathematical Society |volume=51 |pages=597–648 |year=2014 |issue=4 |doi=10.1090/S0273-0979-2014-01456-9 |url=https://www.ams.org/journals/bull/2014-51-04/S0273-0979-2014-01456-9/home.html |doi-access=free }}</ref> साथ ही परिचय में<ref name=DG>{{cite journal |title=गणितज्ञों के लिए यूनिवेलेंट फाउंडेशन का परिचय|first=Daniel R. |last=Grayson |journal=Bulletin of the American Mathematical Society |year=2018 |volume=55 |issue=4 |pages=427–450 |doi=10.1090/bull/1616 |url=http://www.ams.org/journals/bull/0000-000-00/S0273-0979-2018-01616-9/home.html |arxiv=1711.01477|s2cid=32293255 }}</ref> डेनियल ग्रेसन द्वारा। इन्हें भी देखें: व्लादिमीर वोवोडस्की (2014)।<ref>Vladimir Voevodsky (2014) [https://arxiv.org/abs/1401.0053 Experimental library of univalent formalization of mathematics]</ref>
Mathematics<ref>Coquand (2014) [http://www.cse.chalmers.se/~coquand/ober3.pdf  part 1]</ref> <ref>Coquand (2014) [http://www.cse.chalmers.se/~coquand/ober4.pdf part 2]</ref>}} अल्वारो पेलायो और माइकल वारेन द्वारा 2014 की समीक्षा में शास्त्रीय गणित के परिप्रेक्ष्य से मुख्य विचारों की प्रस्तुति देखी जा सकती है,<ref>{{cite journal |first1=Álvaro |last1=Pelayo |first2=Michael A. |last2=Warren |title=होमोटोपी प्रकार का सिद्धांत और वोवोडस्की की असमान नींव|journal=Bulletin of the American Mathematical Society |volume=51 |pages=597–648 |year=2014 |issue=4 |doi=10.1090/S0273-0979-2014-01456-9 |url=https://www.ams.org/journals/bull/2014-51-04/S0273-0979-2014-01456-9/home.html |doi-access=free }}</ref> साथ ही परिचय में<ref name=DG>{{cite journal |title=गणितज्ञों के लिए यूनिवेलेंट फाउंडेशन का परिचय|first=Daniel R. |last=Grayson |journal=Bulletin of the American Mathematical Society |year=2018 |volume=55 |issue=4 |pages=427–450 |doi=10.1090/bull/1616 |url=http://www.ams.org/journals/bull/0000-000-00/S0273-0979-2018-01616-9/home.html |arxiv=1711.01477|s2cid=32293255 }}</ref> डेनियल ग्रेसन द्वारा। इन्हें भी देखें: व्लादिमीर वोवोडस्की (2014)।<ref>Vladimir Voevodsky (2014) [https://arxiv.org/abs/1401.0053 Experimental library of univalent formalization of mathematics]</ref>


Line 32: Line 32:
== वर्तमान घटनाक्रम ==
== वर्तमान घटनाक्रम ==


मार्टिन-लोफ प्रकार के सिद्धांत के एक असमान मॉडल के वोएवोडस्की के निर्माण का लेखा-जोखा कान सरल सेटों में मूल्यों के साथ क्रिस कपुल्किन, पीटर लेफानू लम्सडाइन और व्लादिमीर वोवोडस्की द्वारा एक पेपर में पाया जा सकता है।<ref>{{cite arXiv |first1=Chris |last1=Kapulkin |first2=Peter LeFanu |last2=Lumsdaine |first3=Vladimir |last3=Voevodsky |title=यूनिवेलेंट फाउंडेशन का सरल मॉडल|year=2012 |class=math.LO |eprint=1211.2851}}</ref> [[माइकल शुलमैन (गणितज्ञ)]] द्वारा [[सरल सेट]] के व्युत्क्रम [[आरेख (श्रेणी सिद्धांत)]] की श्रेणियों में मूल्यों के साथ असमान मॉडल का निर्माण किया गया था।<ref>{{cite journal |first=Michael |last=Shulman |title=व्युत्क्रम आरेखों और समरूपता विहितता के लिए एकरूपता|journal=Mathematical Structures in Computer Science |year=2015 |volume=25 |issue=5 |pages=1203–1277 |doi=10.1017/S0960129514000565 |arxiv=1203.3253|s2cid=13595170 }}</ref> इन मॉडलों ने दिखाया है कि प्रस्तावों के लिए अपवर्जित मध्य स्वयंसिद्ध से एकरूपता अभिगृहीत स्वतंत्र है।
मार्टिन-लोफ प्रकार के सिद्धांत के असमान मॉडल के वोएवोडस्की के निर्माण का लेखा-जोखा कान सरल सेटों में मूल्यों के साथ क्रिस कपुल्किन, पीटर लेफानू लम्सडाइन और व्लादिमीर वोवोडस्की द्वारा पेपर में पाया जा सकता है।<ref>{{cite arXiv |first1=Chris |last1=Kapulkin |first2=Peter LeFanu |last2=Lumsdaine |first3=Vladimir |last3=Voevodsky |title=यूनिवेलेंट फाउंडेशन का सरल मॉडल|year=2012 |class=math.LO |eprint=1211.2851}}</ref> [[माइकल शुलमैन (गणितज्ञ)]] द्वारा [[सरल सेट]] के व्युत्क्रम [[आरेख (श्रेणी सिद्धांत)]] की श्रेणियों में मूल्यों के साथ असमान मॉडल का निर्माण किया गया था।<ref>{{cite journal |first=Michael |last=Shulman |title=व्युत्क्रम आरेखों और समरूपता विहितता के लिए एकरूपता|journal=Mathematical Structures in Computer Science |year=2015 |volume=25 |issue=5 |pages=1203–1277 |doi=10.1017/S0960129514000565 |arxiv=1203.3253|s2cid=13595170 }}</ref> इन मॉडलों ने दिखाया है कि प्रस्तावों के लिए अपवर्जित मध्य स्वयंसिद्ध से एकरूपता अभिगृहीत स्वतंत्र है।


वोएवोडस्की के मॉडल को गैर-रचनात्मक माना जाता है क्योंकि यह पसंद के स्वयंसिद्ध का उपयोग एक अपरिहार्य तरीके से करता है।
वोएवोडस्की के मॉडल को गैर-रचनात्मक माना जाता है क्योंकि यह पसंद के स्वयंसिद्ध का उपयोग अपरिहार्य तरीके से करता है।


मार्टिन-लोफ प्रकार के सिद्धांत के नियमों की एक रचनात्मक व्याख्या खोजने की समस्या जो अतिरिक्त रूप से [[एकरूपता स्वयंसिद्ध]] को संतुष्ट करती है{{efn|name= 2018formulation |1= But see Martín Hötzel Escardó's approach.<ref name= HotzelEscardo >Martín Hötzel Escardó (October 18, 2018) [https://arxiv.org/pdf/1803.02294.pdf A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom]</ref>{{rp|4-6}}}} और प्राकृत संख्याओं के लिए प्रामाणिकता खुली रहती है। [[मार्क ब्रूम]], [[थिएरी कोक्वांड]] और [[साइमन ह्यूबर]] द्वारा एक पेपर में एक आंशिक समाधान की रूपरेखा दी गई है<ref>{{cite web |first1=M. |last1=Bezem |first2=T. |last2=Coquand |first3=S. |last3=Huber |title=क्यूबिकल सेट में टाइप थ्योरी का एक मॉडल|url=http://www.cse.chalmers.se/~coquand/mod1.pdf}}</ref> पहचान प्रकारों के लिए एलिमिनेटर की कम्प्यूटेशनल संपत्ति होने के साथ प्रमुख शेष मुद्दा। इस पेपर के विचारों को अब कई दिशाओं में विकसित किया जा रहा है जिसमें क्यूबिकल टाइप थ्योरी का विकास भी शामिल है।<ref>{{citation|first1=Thorsten|last1=Altenkirch|author-link=Thorsten Altenkirch|first2=Ambrus|last2=Kaposi|title=A syntax for cubical type theory |url=http://www.cs.nott.ac.uk/~txa/publ/ctt.pdf}}</ref>
मार्टिन-लोफ प्रकार के सिद्धांत के नियमों की रचनात्मक व्याख्या खोजने की समस्या जो अतिरिक्त रूप से [[एकरूपता स्वयंसिद्ध]] को संतुष्ट करती है{{efn|name= 2018formulation |1= But see Martín Hötzel Escardó's approach.<ref name= HotzelEscardo >Martín Hötzel Escardó (October 18, 2018) [https://arxiv.org/pdf/1803.02294.pdf A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom]</ref>{{rp|4-6}}}} और प्राकृत संख्याओं के लिए प्रामाणिकता खुली रहती है। [[मार्क ब्रूम]], [[थिएरी कोक्वांड]] और [[साइमन ह्यूबर]] द्वारा पेपर में आंशिक समाधान की रूपरेखा दी गई है<ref>{{cite web |first1=M. |last1=Bezem |first2=T. |last2=Coquand |first3=S. |last3=Huber |title=क्यूबिकल सेट में टाइप थ्योरी का एक मॉडल|url=http://www.cse.chalmers.se/~coquand/mod1.pdf}}</ref> पहचान प्रकारों के लिए एलिमिनेटर की कम्प्यूटेशनल संपत्ति होने के साथ प्रमुख शेष मुद्दा। इस पेपर के विचारों को अब कई दिशाओं में विकसित किया जा रहा है जिसमें क्यूबिकल टाइप थ्योरी का विकास भी शामिल है।<ref>{{citation|first1=Thorsten|last1=Altenkirch|author-link=Thorsten Altenkirch|first2=Ambrus|last2=Kaposi|title=A syntax for cubical type theory |url=http://www.cs.nott.ac.uk/~txa/publ/ctt.pdf}}</ref>




Line 46: Line 46:


# अर्ध-सरल प्रकारों के प्रकारों को परिभाषित करने के लिए, एच-प्रकार या (इन्फ्टी, 1) -श्रेणी संरचनाओं पर प्रकार।
# अर्ध-सरल प्रकारों के प्रकारों को परिभाषित करने के लिए, एच-प्रकार या (इन्फ्टी, 1) -श्रेणी संरचनाओं पर प्रकार।
# सीआईसी को एक ब्रह्मांड प्रबंधन प्रणाली के साथ विस्तारित करने के लिए जो आकार बदलने के नियमों के कार्यान्वयन की अनुमति देगा।
# सीआईसी को ब्रह्मांड प्रबंधन प्रणाली के साथ विस्तारित करने के लिए जो आकार बदलने के नियमों के कार्यान्वयन की अनुमति देगा।
# यूनीवैलेंस एक्सिओम का एक रचनात्मक संस्करण विकसित करना<ref>[http://www.math.ias.edu/vladimir/Univalent_Foundations V. Voevodsky, Univalent Foundations Project (a modified version of an NSF grant application), p. 9]</ref>
# यूनीवैलेंस एक्सिओम का रचनात्मक संस्करण विकसित करना<ref>[http://www.math.ias.edu/vladimir/Univalent_Foundations V. Voevodsky, Univalent Foundations Project (a modified version of an NSF grant application), p. 9]</ref>
इन अनसुलझी समस्याओं से संकेत मिलता है कि जबकि सीआईसी एकतरफा नींव के विकास के प्रारंभिक चरण के लिए एक अच्छी प्रणाली है, इसके अधिक परिष्कृत पहलुओं पर काम में कंप्यूटर प्रूफ सहायकों के उपयोग की ओर बढ़ने के लिए औपचारिक कटौती की एक नई पीढ़ी के विकास की आवश्यकता होगी। और संगणना प्रणाली।
इन अनसुलझी समस्याओं से संकेत मिलता है कि जबकि सीआईसी एकतरफा नींव के विकास के प्रारंभिक चरण के लिए अच्छी प्रणाली है, इसके अधिक परिष्कृत पहलुओं पर काम में कंप्यूटर प्रूफ सहायकों के उपयोग की ओर बढ़ने के लिए औपचारिक कटौती की नई पीढ़ी के विकास की आवश्यकता होगी। और संगणना प्रणाली।


== यह भी देखें ==
== यह भी देखें ==
Line 68: Line 68:
* {{Citation|title =HoTT library (2011-current) |date=27 January 2022|url=https://github.com/HoTT/HoTT}}
* {{Citation|title =HoTT library (2011-current) |date=27 January 2022|url=https://github.com/HoTT/HoTT}}
* [https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html Introduction to Univalent Foundations of Mathematics with Agda]
* [https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html Introduction to Univalent Foundations of Mathematics with Agda]
{{Foundations-footer}}
[[Category: गणित की नींव]]  
[[Category: गणित की नींव]]  


Revision as of 23:47, 26 May 2023

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

यदि गणितीय संरचना की उपयुक्त (अर्थात, श्रेणीबद्ध) धारणा को अपनाया जाता है, तो असमान नींव संरचनावाद (गणित के दर्शन) के अनुकूल हैं।[1]


इतिहास

2006 से 2009 के दौरान व्लादिमीर वोवोडस्की द्वारा एकतरफा नींव के मुख्य विचार तैयार किए गए थे। एकतरफा नींव और पहले के विचारों के बीच दार्शनिक संबंधों के लिए एकमात्र संदर्भ वोवोडस्की के 2014 बर्नेज़ व्याख्यान हैं।[2] एकरूपता नाम वोवोडस्की के कारण है।[3][4] कुछ विचारों के इतिहास की अधिक विस्तृत चर्चा, जो वर्तमान स्थिति में एकतरफा नींव में योगदान करती है, होमोटॉपी टाइप थ्योरी (होमोटॉपी टाइप थ्योरी) पर पृष्ठ पर पाई जा सकती है।

असमान नींवों की मूलभूत विशेषता यह है कि वे - जब मार्टिन-लोफ प्रकार के सिद्धांत (मार्टिन-लोफ प्रकार के सिद्धांत) के साथ संयुक्त होते हैं - आधुनिक गणित की औपचारिकता के लिए व्यावहारिक प्रणाली प्रदान करते हैं। इस प्रणाली और Coq (प्रूफ असिस्टेंट) और Agda (प्रोग्रामिंग लैंग्वेज) जैसे आधुनिक प्रूफ सहायकों का उपयोग करके गणित की काफी मात्रा को औपचारिक रूप दिया गया है। फाउंडेशन नामक इस तरह की पहली लाइब्रेरी 2010 में व्लादिमीर वोएवोडस्की द्वारा बनाई गई थी।[5] अब फ़ाउंडेशन बड़े विकास का हिस्सा है जिसमें कई लेखक हैं जिन्हें यूनीमैथ कहा जाता है।[6] फाउंडेशन ने औपचारिक गणित के अन्य पुस्तकालयों को भी प्रेरित किया, जैसे कि HoTT Coq पुस्तकालय[7] और हॉट आज़ाद लाइब्रेरी,[8] जिसने नई दिशाओं में असमान विचारों को विकसित किया।

यूनीवैलेंट फ़ाउंडेशन के लिए महत्वपूर्ण मील का पत्थर थिएरी कोक्वांड द्वारा किया गया सेमिनायर निकोलस बॉरबाकी टॉक था[9] जून 2014 में।

मुख्य अवधारणाएँ

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

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

मार्टिन-लोफ प्रकार के सिद्धांत और उसके वंश जैसे आगमनात्मक निर्माणों के कलन पर आधारित असमान नींव के लिए औपचारिकता प्रणाली में, सेट के उच्च आयामी एनालॉग्स को प्रकारों द्वारा दर्शाया जाता है। प्रकार का संग्रह एच-स्तर (या होमोटोपी स्तर) की अवधारणा द्वारा स्तरीकृत है।[11] एच-स्तर 0 के प्रकार वे हैं जो बिंदु प्रकार के बराबर हैं। उन्हें संविदात्मक प्रकार भी कहा जाता है।

एच-स्तर 1 के प्रकार वे हैं जिनमें कोई भी दो तत्व समान हैं। इस तरह के प्रकारों को असमान नींव में प्रस्ताव कहा जाता है।[11]एच-लेवल के संदर्भ में प्रस्तावों की परिभाषा अवोडी और बाउर द्वारा पहले सुझाई गई परिभाषा से सहमत है।[12] इसलिए, जबकि सभी प्रस्ताव प्रकार हैं, सभी प्रकार तर्क-वाक्य नहीं हैं। प्रस्ताव होना प्रकार का गुण है जिसके लिए प्रमाण की आवश्यकता होती है। उदाहरण के लिए, असमान नींव में पहला मौलिक निर्माण iscontr कहलाता है। यह प्रकार से प्रकार का कार्य है। यदि X प्रकार है तो iscontr X प्रकार है जिसमें वस्तु है यदि और केवल यदि X संविदात्मक है। यह प्रमेय है (जिसे यूनीमैथ लाइब्रेरी में, isapropiscontr कहा जाता है) कि किसी भी X के लिए प्रकार iscontr X का h-स्तर 1 है और इसलिए संविदात्मक प्रकार संपत्ति है। गुणों के बीच यह अंतर जो एच-लेवल 1 के प्रकार की वस्तुओं द्वारा देखा जाता है और संरचनाएं जो उच्च एच-स्तर के प्रकार की वस्तुओं द्वारा देखी जाती हैं, एकतरफा नींव में बहुत महत्वपूर्ण हैं।

एच-लेवल 2 के प्रकार को सेट कहा जाता है।[11]यह प्रमेय है कि प्राकृतिक संख्याओं के प्रकार में एच-स्तर 2 (यूनिमैथ में आईससेटनेट) होता है। असमान नींव के रचनाकारों द्वारा यह दावा किया जाता है कि मार्टिन-लोफ प्रकार के सिद्धांत में सेटों का असमान औपचारिकता सेट-सैद्धांतिक गणित, रचनात्मक और शास्त्रीय दोनों के सभी पहलुओं के बारे में औपचारिक तर्क के लिए वर्तमान में उपलब्ध सर्वोत्तम वातावरण है।[13] श्रेणियों को अतिरिक्त संरचना के साथ एच-लेवल 3 के प्रकार के रूप में परिभाषित किया गया है (यूनीमैथ में RezkCompletion लाइब्रेरी देखें) जो एच-लेवल 2 के प्रकारों पर संरचना के समान है जो आंशिक रूप से ऑर्डर किए गए सेट को परिभाषित करता है। असमान नींव में श्रेणियों का सिद्धांत सेट-सैद्धांतिक दुनिया में श्रेणियों के सिद्धांत की तुलना में कुछ अलग और समृद्ध है, जिसमें प्रमुख नए भेद पूर्व-श्रेणियों और श्रेणियों के बीच हैं।[14] थिएरी कोक्वांड द्वारा ट्यूटोरियल में असमान नींव के मुख्य विचारों और रचनात्मक गणित के साथ उनके संबंध का लेखा-जोखा पाया जा सकता है।[lower-alpha 1] अल्वारो पेलायो और माइकल वारेन द्वारा 2014 की समीक्षा में शास्त्रीय गणित के परिप्रेक्ष्य से मुख्य विचारों की प्रस्तुति देखी जा सकती है,[17] साथ ही परिचय में[18] डेनियल ग्रेसन द्वारा। इन्हें भी देखें: व्लादिमीर वोवोडस्की (2014)।[19]


वर्तमान घटनाक्रम

मार्टिन-लोफ प्रकार के सिद्धांत के असमान मॉडल के वोएवोडस्की के निर्माण का लेखा-जोखा कान सरल सेटों में मूल्यों के साथ क्रिस कपुल्किन, पीटर लेफानू लम्सडाइन और व्लादिमीर वोवोडस्की द्वारा पेपर में पाया जा सकता है।[20] माइकल शुलमैन (गणितज्ञ) द्वारा सरल सेट के व्युत्क्रम आरेख (श्रेणी सिद्धांत) की श्रेणियों में मूल्यों के साथ असमान मॉडल का निर्माण किया गया था।[21] इन मॉडलों ने दिखाया है कि प्रस्तावों के लिए अपवर्जित मध्य स्वयंसिद्ध से एकरूपता अभिगृहीत स्वतंत्र है।

वोएवोडस्की के मॉडल को गैर-रचनात्मक माना जाता है क्योंकि यह पसंद के स्वयंसिद्ध का उपयोग अपरिहार्य तरीके से करता है।

मार्टिन-लोफ प्रकार के सिद्धांत के नियमों की रचनात्मक व्याख्या खोजने की समस्या जो अतिरिक्त रूप से एकरूपता स्वयंसिद्ध को संतुष्ट करती है[lower-alpha 2] और प्राकृत संख्याओं के लिए प्रामाणिकता खुली रहती है। मार्क ब्रूम, थिएरी कोक्वांड और साइमन ह्यूबर द्वारा पेपर में आंशिक समाधान की रूपरेखा दी गई है[23] पहचान प्रकारों के लिए एलिमिनेटर की कम्प्यूटेशनल संपत्ति होने के साथ प्रमुख शेष मुद्दा। इस पेपर के विचारों को अब कई दिशाओं में विकसित किया जा रहा है जिसमें क्यूबिकल टाइप थ्योरी का विकास भी शामिल है।[24]


नई दिशाएं

असमान नींव के ढांचे में गणित की औपचारिकता पर अधिकांश कार्य विभिन्न उप-प्रणालियों और आगमनात्मक निर्माणों (सीआईसी) के कलन के विस्तार का उपयोग करके किया जा रहा है।

तीन मानक समस्याएं हैं जिनका समाधान, कई प्रयासों के बावजूद, CIC का उपयोग करके नहीं बनाया जा सका:

  1. अर्ध-सरल प्रकारों के प्रकारों को परिभाषित करने के लिए, एच-प्रकार या (इन्फ्टी, 1) -श्रेणी संरचनाओं पर प्रकार।
  2. सीआईसी को ब्रह्मांड प्रबंधन प्रणाली के साथ विस्तारित करने के लिए जो आकार बदलने के नियमों के कार्यान्वयन की अनुमति देगा।
  3. यूनीवैलेंस एक्सिओम का रचनात्मक संस्करण विकसित करना[25]

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

यह भी देखें

  • होमोटोपी प्रकार सिद्धांत

टिप्पणियाँ

  1. ↑ Thierry Coquand (2014) Univalent Foundation and Constructive Mathematics[15] [16]
  2. ↑ But see Martín Hötzel Escardó's approach.[22]: 4–6 


संदर्भ

  1. ↑ Awodey, Steve (2014). "संरचनावाद, अपरिवर्तनीयता और एकरूपता" (PDF). Philosophia Mathematica. 22 (1): 1–11. CiteSeerX 10.1.1.691.8113. doi:10.1093/philmat/nkt030.
  2. ↑ Voevodsky, Vladimir (September 9–10, 2014). "Foundations of mathematics — their past, present and future". The 2014 Paul Bernays Lectures. ETH Zurich. See item 11 at Voevodsky Lectures
  3. ↑ univalence axiom in nLab
  4. ↑ Martín Hötzel Escardó (October 18, 2018) A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom
  5. ↑ Foundations library, see https://github.com/vladimirias/Foundations
  6. ↑ UniMath library, see https://github.com/UniMath/UniMath
  7. ↑ HoTT Coq library, see https://github.com/HoTT/HoTT
  8. ↑ HoTT Agda library, see https://github.com/HoTT/HoTT-Agda
  9. ↑ Coquand's Bourbaki Lecture Paper and Video
  10. ↑ Makkai, M. (1995). "डिपेंडेंट सॉर्ट के साथ फर्स्ट ऑर्डर लॉजिक, श्रेणी सिद्धांत के अनुप्रयोगों के साथ" (PDF). FOLDS.
  11. ↑ 11.0 11.1 11.2 See Pelayo & Warren 2014, p. 611
  12. ↑ Awodey, Steven; Bauer, Andrej (2004). "Propositions as [types]". J. Log. Comput. 14 (4): 447–471. doi:10.1093/logcom/14.4.447.
  13. ↑ Voevodsky 2014, Lecture 3, slide 11
  14. ↑ See Ahrens, Benedikt; Kapulkin, Chris; Shulman, Michael (2015). "Univalent categories and the Rezk completion". Mathematical Structures in Computer Science. 25 (5): 1010–1039. arXiv:1303.0584. doi:10.1017/S0960129514000486. S2CID 1135785.
  15. ↑ Coquand (2014) part 1
  16. ↑ Coquand (2014) part 2
  17. ↑ Pelayo, Álvaro; Warren, Michael A. (2014). "होमोटोपी प्रकार का सिद्धांत और वोवोडस्की की असमान नींव". Bulletin of the American Mathematical Society. 51 (4): 597–648. doi:10.1090/S0273-0979-2014-01456-9.
  18. ↑ Grayson, Daniel R. (2018). "गणितज्ञों के लिए यूनिवेलेंट फाउंडेशन का परिचय". Bulletin of the American Mathematical Society. 55 (4): 427–450. arXiv:1711.01477. doi:10.1090/bull/1616. S2CID 32293255.
  19. ↑ Vladimir Voevodsky (2014) Experimental library of univalent formalization of mathematics
  20. ↑ Kapulkin, Chris; Lumsdaine, Peter LeFanu; Voevodsky, Vladimir (2012). "यूनिवेलेंट फाउंडेशन का सरल मॉडल". arXiv:1211.2851 [math.LO].
  21. ↑ Shulman, Michael (2015). "व्युत्क्रम आरेखों और समरूपता विहितता के लिए एकरूपता". Mathematical Structures in Computer Science. 25 (5): 1203–1277. arXiv:1203.3253. doi:10.1017/S0960129514000565. S2CID 13595170.
  22. ↑ Martín Hötzel Escardó (October 18, 2018) A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom
  23. ↑ Bezem, M.; Coquand, T.; Huber, S. "क्यूबिकल सेट में टाइप थ्योरी का एक मॉडल" (PDF).
  24. ↑ Altenkirch, Thorsten; Kaposi, Ambrus, A syntax for cubical type theory (PDF)
  25. ↑ V. Voevodsky, Univalent Foundations Project (a modified version of an NSF grant application), p. 9


बाहरी संबंध

  • The dictionary definition of univalent at Wiktionary
Libraries of formalized mathematics
Retrieved from ‘https://www.vigyanwiki.in/index.php?title=असमान_नींव&oldid=172648’