New Foundations की संगति – Lean से सत्यापित एक जटिल गणितीय प्रमाण
(leanprover-community.github.io)- 1937 में Quine द्वारा प्रस्तावित set theory New Foundations की संगति के प्रमाण का कठिन हिस्सा Lean से सत्यापित किया गया है, और मुख्य theorem
ConNF/Model/Result.leanमें संकलित है - यह approach उस परिणाम का उपयोग करती है कि New Foundations और Tangled Type Theory(TTT) की संगति समतुल्य है, और Lean के भीतर TTT का एक model औपचारिक रूप से निर्मित किया जाता है
- TTT model को बनाना extensionality के कारण कठिन है, क्योंकि निचले type के अवयवों से set uniquely निर्धारित होना चाहिए
- model निर्माण में base type, t-set, allowable permutations, small support, और preferred extension का उपयोग होता है, और type के आकार को μ से नियंत्रित करने के लिए freedom of action theorem की आवश्यकता होती है
- Lean kernel औपचारिक प्रमाण की जाँच करता है, लेकिन यह गारंटी नहीं देता कि औपचारिक कथन का आशय इच्छित अंग्रेज़ी अर्थ से पूरी तरह मेल खाता है, इसलिए परिणाम की व्याख्या में translation review आवश्यक है
Lean से पूरा किया गया New Foundations की संगति का सत्यापन
- 1937 में Quine ने set theory New Foundations प्रस्तावित की थी, और Randall Holmes 2010 से इसके संगति-प्रमाण का दावा करते रहे हैं
- यह project Holmes के प्रमाण के कठिन हिस्सों को interactive theorem prover Lean से सत्यापित कर New Foundations की संगति दिखाने पर केंद्रित है
- प्रमाण पूरा हो चुका है, और theorem statement
ConNF/Model/Result.leanमें देखा जा सकता है - संबंधित सामग्री भी उपलब्ध कराई गई है
लोकल में कोड चलाना
- लोकल execution के लिए elan इंस्टॉल करें, repository clone करें, और repository root में यह command चलाएँ
lake exe cache get
- इसके बाद कोड को Visual Studio Code जैसे editor में देखा जा सकता है, और command line पर
lake buildसे सीधे compile भी किया जा सकता है
New Foundations और TTT का संबंध
- यह ज्ञात है कि New Foundations तभी और केवल तभी consistent है जब Tangled Type Theory(TTT) consistent हो
- संबंधित परिणाम Holmes के theorem 1 में है
- project ने Lean में TTT model को औपचारिक रूप से बनाया, और इससे कागज़ी निष्कर्ष के रूप में New Foundations की consistency, यानी Con(NF), प्राप्त की
- यह काम Holmes के कई proof documents पर आधारित था, लेकिन Lean की type theory के अनुरूप बहुत से बदलाव और अतिरिक्त कार्य करने पड़े
Lean सत्यापन की नींव और व्याख्या संबंधी सावधानियाँ
- project, Lean में लिखी गई community mathematics library mathlib पर निर्भर करता है
- mathlib की वजह से cardinals और groups जैसे परिचित परिणामों को project के भीतर फिर से सिद्ध करने की ज़रूरत नहीं पड़ती
- mathlib और इस project की definitions तथा theorems की जाँच Lean के trusted kernel द्वारा की जाती है
- Lean kernel निर्मित proofs की वास्तविक शुद्धता को computational रूप से verify करता है
- लेकिन Lean यह नहीं जाँच सकता कि औपचारिक कथन इच्छित अंग्रेज़ी समकक्ष से पूरी तरह मेल खाता है या नहीं
- इसलिए कोड से निष्कर्ष निकालते समय अंग्रेज़ी विवरण और formal statement के बीच के translation को सावधानी से देखना ज़रूरी है
Tangled Type Theory की संरचना और कठिनाइयाँ
- TTT, equality
=और membership∈वाली एक many-sorted set theory है - sorts को एक limit ordinal λ से index किया जाता है, और λ के अवयव type indices कहलाते हैं
- expressions के निर्माण की शर्तें type द्वारा सीमित होती हैं
x = yतभी well-formed है जबxऔरyका type समान होx ∈ yतभी well-formed है जबxका type,yके type से कम हो
- मुख्य कठिनाई TTT के extensionality axiom से आती है
- type α का एक set, किसी भी type β < α के elements द्वारा uniquely निर्धारित होना चाहिए
- उदाहरण के लिए, यदि type α के दो sets अलग हों, तो हर β < α के लिए उनके पास अलग-अलग type β elements होने चाहिए
- इस आवश्यकता के कारण TTT model का निर्माण सामान्य set-theoretic model निर्माण से अधिक जटिल हो जाता है
model निर्माण के मुख्य चरण
-
base type का निर्माण
- λ को limit ordinal, κ > λ को regular ordinal, और μ > κ को ऐसा strong limit cardinal माना जाता है जिसकी cofinality कम-से-कम κ हो
- जिन sets का आकार κ से छोटा हो, उन्हें small कहा जाता है
- पहले level -1 का base type बनाया जाता है, जो model के सभी types के नीचे एक auxiliary type है
- इस type के elements को atoms कहा जाता है, लेकिन यह ZFU या NFU के अर्थ में atom नहीं हैं
- atoms की संख्या μ है, और उन्हें आकार κ के litters में विभाजित किया गया है
-
t-set और allowable permutations
- हर type level α पर TTT model के elements बनने वाली collection बनाई जाती है, जिसे t-set कहा जाता है
- साथ ही उन t-sets पर क्रिया करने वाला permutation group भी बनाया जाता है, जिसे allowable permutations कहा जाता है
- membership relation, allowable permutations की action के तहत संरक्षित रहती है
- हर t-set को allowable permutations की action के सापेक्ष एक support के साथ निर्धारित किया जाता है
- support, addresses कहलाने वाली वस्तुओं का एक small set होता है
- यदि कोई allowable permutation support के सभी elements को स्थिर रखता है, तो वह उस t-set को भी स्थिर रखता है
-
preferred extension से extensionality को संतुष्ट करना
- हर level α के t-set का किसी type β < α पर एक preferred extension होता है
- t-set के elements से यह पुनर्निर्मित किया जा सकता है कि कौन-सा extension preferred है, और अन्य निचले types के extensions उसी β-extension से निकाले जाते हैं
- इसी संरचना का उपयोग TTT के extensionality axiom को संतुष्ट करने के लिए किया जाता है
-
type के आकार का नियंत्रण
- हर type α के निर्माण के लिए यह मान्यता चाहिए कि सभी β < α types का आकार ठीक μ है
- यह सिद्ध करना आसान है कि level α की t-set collection का आकार कम-से-कम μ है, इसलिए यह दिखाना होता है कि वह अधिक-से-अधिक μ ही है
- इसके लिए दिखाया जाता है कि allowable permutations की action के तहत tangles के मूलतः अलग-अलग descriptions बहुत अधिक नहीं हैं
- इस चरण के लिए freedom of action theorem की आवश्यकता होती है, जो allowable permutations के निर्माण को संभव बनाने वाला एक तकनीकी lemma है
- इस खंड का मुख्य परिणाम ConNF.mk_tSet में है
-
induction का समापन और axioms की जाँच
- ऊपर की प्रक्रिया को recursive रूप से चलाकर हर type level α पर tangles का type बनाया जाता है
- set theory में यह अपेक्षाकृत आसान चरण है, लेकिन type theory में कई आवश्यक inductive assumptions के आपस में उलझे होने के कारण बहुत काम करना पड़ता है
- इसके बाद यह जाँचा जाता है कि निर्मित संरचना TTT का model है या नहीं, इसके लिए theory की finite axiomatization को satisfy कराया जाता है
- project ने Hailperin की NF comprehension scheme की finite axiomatization को TTT की finite axiomatization में बदलकर उपयोग किया है
- परिणाम फ़ाइल results file में है
- यह चयन मनमाना है, और पहले से बनी infrastructure का उपयोग कर अन्य finite axiomatizations को भी आसानी से सिद्ध किया जा सकता है
1 टिप्पणियां
Hacker News की राय
Lean में किए गए proof के गलत होने का जोखिम मुझे बहुत कम लगता है
हालांकि Lean bug से अलग, software verification और गणित दोनों में एक जाना-पहचाना जोखिम है: निष्कर्ष को ठीक से पढ़कर यह पक्का करना कि सच में वही proposition साबित हुआ है जिसकी जरूरत थी
मैंने Wilshaw का अंतिम निष्कर्ष ध्यान से पढ़ा है, और मेरा आकलन है कि उन्होंने वही साबित किया है जो वास्तव में साबित करना था
पेपर भी कुछ ऐसा ही कहता है: mathlib और इस project की सभी definitions और theorems को Lean के trusted kernel ने check किया, और हमने जो proof बनाया है वह सच में सही है या नहीं, इसे computationally verify किया
लेकिन Lean यह verify नहीं कर सकता कि definitions और theorems के propositions उनके intended English expressions से मेल खाते हैं या नहीं, इसलिए इस project के code से निष्कर्ष निकालते समय English के साथ translation को लेकर सावधान रहना होगा
मैं जिस समस्या की बात कर रहा हूं वह libraries से जुड़ी चिंता से संबंधित है: अगर कोई defined concept इस्तेमाल किया जाता है, तो यह भरोसा होना चाहिए कि उसकी definition सही है, यानी वास्तव में वही साबित हुआ है जिसकी जरूरत थी
Wilshaw की formalization ने libraries का इस्तेमाल जरूर किया है, लेकिन यह objection उस पर असरदार नहीं है। जो साबित हुआ है वह यह है कि कोई defined concept first-order logic formulas के एक खास bundle को satisfy करता है, और अगर उन formulas को satisfy करने वाला predicate मौजूद है, तो NF consistent है
एक और जोखिम खुद Lean में bug का है। theorem provers में ऐसा पहले कभी नहीं हुआ हो, ऐसा भी नहीं है 1
गलती से उस पर पड़ जाना शायद मुश्किल हो, लेकिन 3 की तरह arbitrary लोग steps भरते हैं ऐसी बड़े पैमाने की collaborations बढ़ती जा रही हैं। किसी के खोजे हुए bug से एक step भरकर sabotage करने की स्थिति चिंता का विषय बन सकती है
foundations के नजरिए से यह भी महत्वपूर्ण है कि यह proof NF और Lean kernel के बीच equiconsistency का proof है। Lean kernel को खुद इंसानों ने review किया है
mechanized theorem prover सहीपन के उस स्तर को preserve करने का तरीका है जो इंसानों या दूसरे external systems के जरिए inject किया गया हो
अगर मैं गलत नहीं समझ रहा, तो यह शायद पहला मामला है जहां proof assistant ने ऐसे कठिन proof की स्थिति साफ की है जो कई सालों से अस्पष्ट बनी हुई थी
Coq के four color theorem जैसे projects रहे हैं जिन्होंने ऐसे मौजूदा proofs verify किए जिनमें untrusted software ने बड़ा computational हिस्सा संभाला था, लेकिन ऐसा मामला जहां व्यापक mathematical community में result की epistemological status ही uncertain थी, शायद पहली बार है
Liquid Tensor Experiment भी याद आता है
https://www.nature.com/articles/d41586-021-01627-2
https://leanprover-community.github.io/blog/posts/lte-final/
यह Kepler conjecture जैसी स्थिति है (https://en.m.wikipedia.org/wiki/Kepler_conjecture)
proof पहले से ज्ञात था, लेकिन formalize होने तक यह भरोसा नहीं था कि वह सही है
अगला शायद abc conjecture होगा
2012 में इसे prove करने का दावा किया गया था और 400 से अधिक pages का paper online है, लेकिन लगता है कि उस proof को स्वीकार करने वाले लोग ज्यादा नहीं हैं
क्या कोई मोटे तौर पर समझा सकता है कि “New Foundations” set theory की formalization दूसरी formalizations की तुलना में खास या नई कैसे है?
या फिर math undergraduate या engineering professional के पढ़ने लायक कोई explanation link भी ठीक रहेगा
मेरे हिसाब से मुख्य बात universal set का अस्तित्व है। मेरे use case, यानी programming languages के type systems में, ऐसा universal set बहुत उपयोगी है
existing systems में cumulative universes या type-in-type जैसे कई workarounds संतोषजनक नहीं हैं। इसके बजाय बस यह check किया जा सकता है कि type signature stratified है या नहीं, और फिर यह बात भूल सकते हैं कि types के numeric levels होते हैं
मूल रूप से यह require करता है कि subset चुनने के लिए इस्तेमाल होने वाला predicate एक बहुत हल्के type system का पालन करे। “x खुद का element नहीं है” किसी reasonable type system में well-typed question नहीं है, और खासकर NF की “stratifiability” requirement भी satisfy नहीं करता, इसलिए Russell paradox वाला वह set—सभी ऐसे sets का set जो खुद को include नहीं करते—बनाया नहीं जा सकता
“stratifiable” की definition भी ज्यादा complex नहीं है। इसके उलट ZF में आठ axioms/axiom schemata हैं, जो काफी ad hoc जैसे लगते हैं
Coq और Lean के fundamental differences क्या हैं, और क्या वे same kind की logic पर काम करते हैं, यह जानने के लिए मुझे यह post मिला 1
वह discussion मुझे लगभग समझ नहीं आई और मैंने दोनों में से किसी को practically use नहीं किया है। इस बारे में और explanation या दूसरे proof assistants से comparison हो तो सुनना चाहूंगा
1 https://proofassistants.stackexchange.com/questions/153/what...
फर्क है, और यह discussion भी देखने लायक है 1
1 https://github.com/coq/coq/issues/10871
लगता है Lean के समर्थक अपनी भाषा थोड़ी बढ़ा-चढ़ाकर इस्तेमाल करते हैं। Lean, जैसा अक्सर संकेत दिया जाता है, कोई ज़्यादा बेहतर proof method नहीं, बल्कि एक वैकल्पिक proof style है
Lean सीखने की कोशिश करें तो जल्द ही पता चलता है कि यह अपने bugs वाला एक programming language और system है, और दूसरे इंसानों द्वारा लिखे गए कई library stacks पर काफी निर्भर करता है। उन libraries में choices शामिल हैं, और उनमें gaps या bugs भी हो सकते हैं
इसलिए “Lean ने कहा कि वह proof सही है” जैसी अभिव्यक्ति से मुझे असहमति है। ज़्यादा सटीक और ईमानदार बात यह होगी कि लिखे गए proof को मानव mathematicians ने verify किया, और उस proof को इंसान ने Lean में translate किया और वहां भी verify किया गया। यह कहना कि Lean ही अकेला golden verification देता है, जरूरी नहीं कि ठीक हो, या कम से कम मैंने ऐसा कोई स्पष्टीकरण नहीं देखा। उपशीर्षक “Randall Holmes proof का digitalization” सबसे सटीक अभिव्यक्ति लगता है
Lean जैसे मजबूत system में machine-verified proof मुझे केवल इंसानों द्वारा verified proof से कहीं बेहतर लगता है। इंसान अद्भुत होते हैं, लेकिन ऊबते हैं और details miss कर देते हैं
यह सिर्फ theoretical दावा नहीं है। लोगों ने Euclid के Elements को 2,000 साल से भी ज्यादा पढ़ने के बाद जाकर missing axioms पर ध्यान दिया। यह ऐसी basic गलती थी जिसे ठीक से काम करने वाला machine proof verification system तुरंत दिखा देता
Published mathematical proofs भी बाद में गलत साबित होते रहते हैं। Mathematics जैसे-जैसे अधिक sophisticated हो रहा है, इंसानों के लिए हर step को सही से verify करना उतना ही कठिन होता जा रहा है। Machines अभी proof generation में इंसानों जितनी अच्छी नहीं हैं, लेकिन verification में उनका कोई मुकाबला नहीं
Lean से “compete” करने वाले systems भी हैं, इसलिए मैं यह नहीं कहूंगा कि Lean ही “एकमात्र सच्चा रास्ता” है। उदाहरण के लिए, मुझे Metamath भी पसंद है। हालांकि इन systems के बीच “competition” को quotes में रखना चाहिए। हर एक के अपने फायदे-नुकसान हैं, और कई लोग कई systems को पसंद करते, इस्तेमाल करते या contribute करते हैं। सभी theorems को ऐसी rigor के साथ verify कर सकते हैं जो इंसानों के लिए व्यावहारिक नहीं
bugs हो सकते हैं, लेकिन मेरी समझ में भरोसा सिर्फ kernel पर करना होता है
अगर “दूसरे इंसानों द्वारा लिखे गए कई library stacks” से मतलब mathlib है, तो मुझे यह बात सही नहीं लगती। क्योंकि mathlib code भी आखिरकार kernel द्वारा process किए जाने वाले code में compile होता है
वेबसाइट पर paper draft 0 भी इसी बात को मजबूत करता है: Lean एक बड़ा project है, लेकिन accepted proof सही है यह guarantee करने के लिए सिर्फ kernel पर भरोसा करना होता है। tactics अगर गलत proof term output करें, तब भी kernel के पास proof accept करने से पहले उस गलती को पकड़ने का मौका होता है
फर्क यह है कि Lean में सिर्फ kernel पर भरोसा करना होता है। बाकी सब उसी के ऊपर बना है। अगर kernel sound है, तो बाकी सब भी sound है
यह सामान्य programming languages से काफी अलग है। सामान्य languages में कभी भी bug आ सकता है। यह mathematics से भी काफी अलग है, जहां कोई भी lemma गलती समेटे हो सकता है
theorem prover की शानदार बात यह है कि, kernel सही है यह मानते हुए, गलत proof compile भी नहीं होता
proofs के मामले में traditional software जैसे runtime पर ही आने वाले bugs नहीं होते। क्योंकि runtime होता ही नहीं
Lean को “सामान्य” programming language की तरह भी इस्तेमाल किया जा सकता है, और तब runtime bugs का risk होता है, लेकिन यहां मामला वह नहीं है
आप theorem provers को गलत समझ रहे हैं। यह “सभी abstractions leak करती हैं” वाली बात नहीं है। Libraries पर भरोसा करने की जरूरत नहीं, सिर्फ kernel पर भरोसा करना होता है
kernel पर भरोसा करना भी मामूली बात नहीं है, लेकिन informal proof की तुलना में यह बहुत बड़ी छलांग है। Informal proof में वास्तव में “libraries”, यानी culture और दूसरे लोगों के knowledge पर भरोसा करना पड़ता है। क्योंकि axioms तक सचमुच boil down करने का कोई practical तरीका नहीं होता
क्या ZFC खत्म और NF अमर रहे?
एक amateur mathematician के तौर पर, जो sets को मुख्यतः दूसरी चीजों को समझाने की common language के रूप में इस्तेमाल करता है, मुझे ठीक से नहीं पता कि wider mathematics के लिए इसका क्या implication है। खासकर अगर NF की उपयोगिता मौजूदा ZFC और उसके variants जैसी ही हो
क्या उम्मीद है कि machine proof में NF, ZFC जितना popular होगा? universal set का अस्तित्व ज्यादा intuitive लगता है, इसलिए कम से कम इस proof की वजह से formalization में मेरी निजी दिलचस्पी फिर से जाग गई है
एक naive amateur नज़रिए से, चूंकि हर ZFC model को NF model में extend किया जा सकता है, इसलिए relative consistency result NF को कम से कम ZFC जितना useful बनाता लगता है
लेकिन नीचे में से कोई एक बात न हो तो NF शायद बहुत useful नहीं बनेगा
यह prove हो कि NF inconsistent है। तब ZFC भी inconsistent होगा। रात के आसमान के तारे एक-एक करके बुझने लगेंगे ;)
यह prove हो कि ZFC inconsistent है। तब NF के consistent होने की संभावना अभी भी बची रहेगी। बस किस्मत साथ देनी होगी
बेशक, मुमकिन है कि मैं NF के ज्यादा practical “quality of life” advantages miss कर रहा हूं, जैसे proper classes के बारे में बात कर पाना, या stratified formulas के जरिए Russell's paradox से बच निकलना
NF को independent foundational system के रूप में आगे बढ़ाने का मेरा बिल्कुल इरादा नहीं है। NF काफी अजीब system है
फिर भी अगर कोई इसे आगे बढ़ाना चाहे, तो यह consistency result कम से कम इतना कहने देता है कि ZFC में contradiction तक पहुंचने के risk से बड़ा risk नहीं है
यह मुझे सच में बहुत पसंद है
सोचता हूं कि आखिरकार यह collaborative proof और “bug fixing” तक पहुंचेगा, और mathematics GitHub पर code जैसी process बन जाएगी या नहीं
काश मेरे पास mathlib project follow करने के लिए free time होता। यह सच में शानदार है
क्या बहुत loosely ही सही, इसमें participate करने का कोई तरीका है?
Natural numbers game से शुरुआत कर सकते हैं
https://adam.math.hhu.de/#/g/leanprover-community/NNG4
मैं इस क्षेत्र का व्यक्ति नहीं हूँ, लेकिन क्या Gödel theorem नहीं था कि हर पर्याप्त रूप से शक्तिशाली system अपनी ही consistency नहीं दिखा सकता?
हालांकि system X अपनी खुद की consistency prove नहीं कर सकता, लेकिन उससे ज्यादा शक्तिशाली system Y, X की consistency prove कर सकता है। और कोई दूसरा, उससे भी ज्यादा शक्तिशाली system Y की consistency prove कर सकता है। इस तरह एक chain बनती है जिसमें हर system अपने से कमजोर system की consistency prove करता है
यह prove नहीं करता कि वह system absolute रूप से consistent है। क्योंकि अगर Y contradictory है, तो वह यह भी prove कर सकता है कि X consistent है, और यह भी कि X contradictory है। फिर भी इसकी value है। आखिर हम Y का इस्तेमाल जिन कारणों से करते हैं, उनमें से एक यह है कि हमें उसके अंदर कोई contradiction पता नहीं है। Formal systems अक्सर subtle तरीके से contradictory हो सकते हैं, इसलिए “किसी दूसरे system के consistent होने की assumption के तहत consistent” होना “consistency का कोई proof न होना” से कहीं बेहतर है
एक contradictory system भी अपनी खुद की consistency prove कर सकता है। इसलिए अगर किसी system के पास अपने consistent होने का proof हो, तब भी हमें यह नहीं पता चलता कि वह सच में consistent है या नहीं
इसे बनाने वालों में से एक के शामिल होने वाली Reddit discussion भी देखने लायक है 0
https://old.reddit.com/r/math/comments/1ca6bj8/new_foundatio...