New Foundations की सुसंगतता – Lean का उपयोग करके सिद्ध एक कठिन गणितीय प्रमाण

 (leanprover-community.github.io)
1 पॉइंट द्वारा GN⁺ 2024-04-24 | 1 टिप्पणियां | WhatsApp पर शेयर करें

Here is a summary of the key points from the given article, organized using Markdown:

New Foundations समुच्चय सिद्धांत की सुसंगतता का प्रमाण

  • 1937 में Quine द्वारा प्रस्तावित "New Foundations(NF)" समुच्चय सिद्धांत की सुसंगतता Randall Holmes 2010 के बाद से सिद्ध करने का दावा करते रहे हैं
  • यह repository interactive theorem prover Lean का उपयोग करके Holmes के प्रमाण के कठिन हिस्सों का सत्यापन करती है, और इस तरह यह सिद्ध करती है कि NF वास्तव में असंगत नहीं है
  • प्रमाण अब पूरा हो चुका है, और theorem statement ConNF/Model/Result.lean में पाया जा सकता है

लक्ष्य

  • यह ज्ञात है कि NF तभी और केवल तभी सुसंगत है जब Tangled Type Theory(TTT) सुसंगत हो
  • Lean में TTT का एक model औपचारिक रूप से निर्मित करके NF की सुसंगतता सिद्ध की जाती है
  • काम Holmes के प्रमाण के कई संस्करणों पर आधारित है, लेकिन Lean की type theory के साथ संगत बनाने के लिए कई बदलाव और अतिरिक्त बातें जोड़ी गई हैं
  • यह project Lean में लिखी गई community mathematics library mathlib पर निर्भर करता है, जिससे cardinal या group जैसी परिचित बातों के परिणामों को स्वयं सिद्ध किए बिना उपयोग किया जा सकता है
  • Lean के विश्वसनीय kernel द्वारा mathlib और इस project की सभी definitions और theorems सत्यापित किए गए हैं, लेकिन Lean यह जांच नहीं सकता कि definitions और theorems का वर्णन इच्छित English व्याख्या से मेल खाता है या नहीं; इसलिए इस project के code से निष्कर्ष निकालते समय English के साथ अनुवाद पर सावधानी जरूरी है

Tangled Type Theory(TTT)

  • TTT एक many-sorted set theory है जिसमें समानता संबंध "=" और सदस्यता संबंध "∈" होते हैं
  • sorts को एक limit ordinal λ द्वारा index किया जाता है, और λ के अवयवों को type indices कहा जाता है
  • सूत्र "x = y" तब well-formed होता है जब x और y का type समान हो, और "x ∈ y" तब well-formed होता है जब x का type, y के type से छोटा कोई भी type हो
  • TTT के axioms में से एक extensionality है, जिसके अनुसार type α का एक set, किसी भी β < α type के elements द्वारा uniquely निर्धारित होता है
  • उदाहरण के लिए, यदि type α के दो sets अलग हैं, तो हर β < α के लिए उनमें अलग β-type elements होंगे; यही गुण TTT के models बनाना कठिन बनाता है

रणनीति

  • model निर्माण मोटे तौर पर निम्नलिखित रणनीति का उपयोग करता है:

    • आधार type का निर्माण

      • λ को एक limit ordinal, κ > λ को एक regular ordinal, और μ > κ को ऐसा strong limit cardinal माना जाता है जिसकी cofinality कम से कम κ हो
      • κ से छोटे sets को छोटा कहा जाता है
      • level -1 पर basic type नाम का एक auxiliary type बनाया जाता है, जो अंततः model का हिस्सा बनने वाले सभी types के नीचे स्थित होता है
      • इस type के elements को atoms कहा जाता है (ZFU या NFU के अर्थ में atoms नहीं), और μ atoms होते हैं, जिन्हें आकार κ के litters में विभाजित किया जाता है

    • प्रत्येक type का निर्माण

      • हर type level α पर TTT के इच्छित model के लिए model elements का एक collection बनाया जाता है, जिन्हें कभी-कभी t-sets कहा जाता है
      • allowed permutations नाम का एक permutation group बनाया जाता है, जो t-sets पर क्रिया करता है
      • सदस्यता संबंध allowed permutations की क्रिया के तहत संरक्षित रहता है
      • प्रत्येक t-set को allowed permutations की क्रिया के तहत support रखने की शर्त दी जाती है; support addresses कहलाने वाली छोटी वस्तुओं का एक set है, और जब भी कोई allowed permutation support के सभी elements को स्थिर रखता है, t-set भी स्थिर रहता है
      • level α के प्रत्येक t-set को β < α type की एक preferred extension दी जाती है, और t-set के elements से यह पुनर्प्राप्त किया जा सकता है कि कौन-सी extension preferred है
      • अन्य lower types में इन t-sets की extensions को β-extension से निकाला जा सकता है, और इससे TTT का extensionality axiom संतुष्ट किया जा सकता है

    • प्रत्येक type के आकार का नियंत्रण

      • हर type α केवल इस मान्यता (और अन्य hypotheses) के तहत बनाया जा सकता है कि सभी β < α types का आकार ठीक μ है
      • यह सिद्ध करना आसान है कि level α पर t-sets का collection कम से कम cardinality μ रखता है, इसलिए यह दिखाना आवश्यक है कि इसके अधिकतम μ elements ही हैं
      • यह इस तरह किया जाता है कि allowed permutations की क्रिया के तहत tangled वस्तुओं के मूलतः भिन्न विवरण बहुत अधिक नहीं हैं
      • इसके लिए action freedom theorem की आवश्यकता होती है, जो एक तकनीकी lemma है और allowed permutations का निर्माण संभव बनाती है
      • इस section का मुख्य परिणाम यहीं है

    • induction को पूरा करना

      • ऊपर की प्रक्रिया को recursively चलाकर हर type level α पर tangled types उत्पन्न किए जा सकते हैं
      • set theory में यह आसान कदम है, लेकिन आवश्यक विभिन्न induction hypotheses की परस्पर जुड़ाव के कारण type theory में इसमें काफी काम लगता है
      • इसके बाद यह जाँचा जाता है कि हमारा construction वास्तव में TTT का model बनाता है या नहीं और क्या यह theory की finite axiomatization को संतुष्ट करता है
      • हमने NF की comprehension scheme के लिए Hailperin की finite axiomatization को TTT की finite axiomatization में बदलने का विकल्प चुना, और इसे result file में प्रस्तुत किया है
      • हालांकि यह विकल्प मनमाना है, और पहले से तैयार infrastructure का उपयोग करके अन्य finite axiomatizations को भी आसानी से सिद्ध किया जा सकता है

GN⁺ की राय

  • यह प्रमाण इस अर्थ में अत्यंत महत्वपूर्ण परिणाम है कि यह NF समुच्चय सिद्धांत की सुसंगतता को औपचारिक रूप से सिद्ध करता है, जो अब तक केवल बहुत अमूर्त स्तर पर ही ज्ञात थी। यह न केवल शुद्ध गणित के लिए महत्वपूर्ण है, बल्कि proof assistant tools के विकास और automated theorem proving में वास्तविक प्रगति का उदाहरण भी है
  • Lean का उपयोग करके किया गया यह formalization प्रमाण की शुद्धता और पूर्णता सुनिश्चित करता है, लेकिन साथ ही यह गणितज्ञों के लिए समझना कठिन हो सकता है क्योंकि यह ऐसी भाषा में लिखा गया है जिससे वे परिचित नहीं होते। प्रमाण के मुख्य विचारों को natural language में स्पष्ट रूप से समझाने का काम भी साथ-साथ होना चाहिए
  • TTT का यह विचित्र extensionality axiom क्यों आवश्यक है, और इसका अन्य set theories से क्या संबंध है, जैसी पृष्ठभूमि संबंधी सहज व्याख्या भी कुछ कम है। यदि औपचारिक प्रमाण के साथ दार्शनिक और ऐतिहासिक संदर्भों की चर्चा भी जोड़ी जाए, तो NF सिद्धांत की समझ और बेहतर हो सकती है
  • निर्मित model का मानक ZFC set theory के models से क्या संबंध है, और NF की सुसंगतता अन्य axiom systems की सुसंगतता से कैसे जुड़ती है, जैसे आगे के शोध विषय भी रोचक लगते हैं
  • Lean में ऐसे जटिल प्रमाण का formalization, गणित के अन्य क्षेत्रों में proof automation के लिए भी एक उदाहरण बन सकता है। यदि उन theorems पर भी इसी तरह का काम किया जाए जिनकी proof process पहले अच्छी तरह ज्ञात नहीं थी, तो गणित जगत पर इसका बड़ा प्रभाव पड़ सकता है

संबंधित पढ़ाई

1 टिप्पणियां

 
GN⁺ 2024-04-24
Hacker News राय
  • Lean का उपयोग करके किए गए proof के गलत होने का जोखिम बहुत कम है। लेकिन Lean के bug से अलग, software verification और mathematics में यह एक ज्ञात समस्या है कि निष्कर्षों को ध्यान से पढ़ा जाए और यह पक्का किया जाए कि वास्तव में वही सिद्ध किया गया है जो दावा किया गया है।
  • यह मामला कठिन proof की स्थिति को सुलझाने के लिए proof assistant के उपयोग का पहला उदाहरण प्रतीत होता है। इससे पहले ऐसे प्रोजेक्ट रहे हैं जिन्होंने मौजूदा proofs को verify किया था, जिनमें बड़े पैमाने की computation शामिल थी और जिन्हें अविश्वसनीय software से संभाला गया था, लेकिन यह मामला पहला था जिसमें परिणाम की epistemic status गणित समुदाय में अनिश्चित थी।
  • Coq और Lean के बुनियादी अंतर और क्या वे एक ही तरह की logic पर काम करते हैं, इस बारे में जिज्ञासा व्यक्त की गई। संबंधित चर्चा में ऐसी बातें कही गईं जिन्हें समझना कठिन है।
  • Lean के समर्थक अक्सर इस बात का बहुत ज़ोर से उपयोग करते हैं कि Lean एक श्रेष्ठ proof method है। Lean सिर्फ एक वैकल्पिक proof method है; एक programming language और system के रूप में इसके अपने bug हैं और यह दूसरे लोगों द्वारा लिखी गई कई library stacks पर बहुत अधिक निर्भर करता है।
  • "Lean ने कहा कि proof अच्छा है" ऐसा कहने की बजाय यह कहना अधिक सटीक और ईमानदार होगा कि लिखे गए proof को मानव गणितज्ञों ने verify किया, और उस proof को Lean में रूपांतरित किया गया जहाँ उसे भी verify किया गया। यह कहना कि Lean ही एकमात्र और स्वर्णिम verification देता है, सही नहीं है, या कम से कम ऐसी व्याख्या नहीं देखी गई।
  • अनुरोध किया गया कि "New Foundations" set theory की formalization अन्य formalizations की तुलना में किस तरह विशेष या नई है, इसका एक मोटा स्पष्टीकरण ऐसा दिया जाए जिसे गणित के undergraduate छात्र या engineering professionals पढ़ सकें।
  • जिज्ञासा जताई गई कि क्या यह तरीका अंततः collaborative proof और 'bug fixing' की ओर ले जाएगा, जिससे mathematics GitHub पर code जैसी प्रक्रिया बन जाएगी।
  • पूछा गया कि Gödel के theorem के अनुसार हर पर्याप्त रूप से शक्तिशाली system अपनी ही consistency नहीं दिखा सकता, तो इस पर क्या कहा जाए।
  • mathlib project को आगे भी follow करना चाहते हैं, लेकिन समय नहीं है। क्या इसमें बहुत निष्क्रिय तरीके से भाग लेने का कोई तरीका है, इस पर जिज्ञासा जताई गई।