🔢 mathematics

Schemata, Cyclic Proofs and Herbrand Systems

यह शोध पत्र पॉइंट ट्रांज़िशन सिस्टम्स पर आधारित एक नए प्रकार के प्रूफ़ स्कीमा (proof schema) को प्रस्तुत करता है जो इंडक्टिव प्रूफ़्स के लिए हर्ब्रैंड सिस्टम्स (Herbrand systems) की गणना करने में सक्षम बनाता है, साइक्लिकिक प्रूफ़्स से इन स्कीमा में एक रूपांतरण स्थापित करता है, और 2-हाइड्रा (2-Hydra) कथन को सिद्ध करके उनकी उत्कृष्ट अभिव्यंजक शक्ति का प्रदर्शन करता है, जो मानक LKID में अप्रमाणित है।

मूल लेखक: Alexander Leitsch, Anela Lolic, Stella Mahler

प्रकाशित 2026-06-23

📖 6 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Alexander Leitsch, Anela Lolic, Stella Mahler

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

कल्पना कीजिए कि आप एक ऐसे गणितीय कथन को सिद्ध करने की कोशिश कर रहे हैं जिसमें एक कभी न खत्म होने वाली प्रक्रिया शामिल है, जैसे कि अनंत तक गिनती करना या एक ऐसी पहेली को हल करना जहाँ हर बार कदम उठाने पर नियम थोड़े बदल जाते हैं। पारंपरिक गणित में, इन चीजों को सिद्ध करने के लिए आमतौर पर एक विशेष "आगमन नियम" (Induction Rule) की आवश्यकता होती है—एक जादुई छड़ी जो कहती है, "यदि यह चरण 1 के लिए काम करता है, और यदि चरण $n$ का काम करना यह दर्शाता है कि यह चरण $n+1$ के लिए भी काम करेगा, तो यह सभी चरणों के लिए काम करता है।"

हालाँकि, इस शोध पत्र के लेखक इन प्रमाणों को देखने के एक अलग तरीके में रुचि रखते हैं। वे इन प्रमाणों को एक "प्रमाण स्कीमाटा" (Proof Schemata) के रूप में वर्णित करना चाहते हैं, जो एक विशिष्ट, परिमित (finite) प्रमाणों के अनंत अनुक्रम को उत्पन्न करने वाली एक नुस्खा (recipe) या एक ब्लूप्रिंट (blueprint) है।

यहाँ उनके कार्य का सरल उपमाओं का उपयोग करके विवरण दिया गया है:

1. समस्या: "अनंत पुस्तकालय" (The Infinite Library)

एक पुस्तकालय की कल्पना करें जहाँ प्रत्येक पुस्तक किसी विशिष्ट गणितीय समस्या का प्रमाण है। यदि आपके पास एक समस्या है जिसके लिए आगमन (induction) की आवश्यकता है, तो आपको एक अनंत पुस्तकालय की आवश्यकता हो सकती है: $n=1$ के लिए एक पुस्तक, $n=2$ के लिए एक, $n=3$ के लिए एक, और इसी तरह, अनंत तक।

पारंपरिक प्रमाण (Traditional Proofs): एक नियम का उपयोग करते हैं जो कहता है, "हमें हर किताब लिखने की आवश्यकता नहीं है; हमें बस एक नियम चाहिए जो उन्हें उत्पन्न कर सके।"
लेखकों का दृष्टिकोण: वे एक मास्टर ब्लूप्रिंट (Master Blueprint) बनाते हैं। यह ब्लूप्रिंट कोई एकल प्रमाण नहीं है; यह निर्देशों का एक सेट है जो आपको किसी भी संख्या $n$ के लिए विशिष्ट प्रमाण बनाने का तरीका बताता है। यह एक कंप्यूटर प्रोग्राम की तरह है जो आपकी मांग पर $n=100$ या $n=1,000,000$ के लिए प्रमाण प्रिंट करता है।

2. नया उपकरण: "पॉइंट ट्रांज़िशन सिस्टम्स" (Point Transition Systems)

इन ब्लूप्रिंट्स को अधिक शक्तिशाली बनाने के लिए, लेखक निर्देशों को व्यवस्थित करने का एक नया तरीका पेश करते हैं जिसे पॉइंट ट्रांज़िशन सिस्टम्स कहा जाता है।

उपमा: एक बोर्ड गेम के बारे में सोचें। आप एक विशिष्ट वर्ग (एक "पॉइंट") पर हैं। पासे के रोल (एक "कंडीशन") के आधार पर, आप एक नए वर्ग पर जाते हैं।
शोध पत्र में: पासे के बजाय, "कंडीशन्स" गणितीय नियम हैं (जैसे, "यदि $x$ , 0 से बड़ा है")। "वर्ग" (squares) प्रमाण के विभिन्न भाग हैं। यह प्रणाली सभी संभावित चालों का मानचित्र बनाती है। यदि खेल को अच्छी तरह से डिज़ाइन किया गया है, तो आप चाहे कहीं से भी शुरू करें, आप अंततः "अंत" (End) वर्ग (एक पूर्ण प्रमाण) तक पहुँचने की गारंटी रखते हैं। यह सुनिश्चित करता है कि ब्लूप्रइंट वास्तव में काम करता है और अनंत लूप में नहीं फंसता है।

3. खजाने की खोज: "हर्ब्रैंड सिस्टम्स" (Herbrand Systems)

इस शोध का एक मुख्य लक्ष्य प्रूफ माइनिंग (Proof Mining) है। यह विचार कि एक प्रमाण में छिपी हुई जानकारी होती है, जैसे कि एक खजाने का नक्शा।

खजाना: तर्कशास्त्र (logic) में, यह खजाना उदाहरणों की एक सूची (जिन्हें हर्ब्रैंड इंस्टेंस कहा जाता है) है जो कथन को सत्य सिद्ध करते हैं। उदाहरण के लिए, यदि आप सिद्ध करते हैं कि "सभी संख्याओं में एक गुण है," तो खजाना उन विशिष्ट संख्याओं की सूची है जो वास्तव में इसे प्रदर्शित करती हैं।
चुनौती: आमतौर पर, यदि कोई प्रमाण आगमन (induction) का उपयोग करता है, तो इस उदाहरणों की सूची को खोजना असंभव होता है क्योंकि प्रमाण बहुत अमूर्त (abstract) होता है।
महत्वपूर्ण उपलब्धि: लेखक दिखाते हैं कि उनके "ब्लूप्रिंट्स" (Proof Schemata) के लिए, वे इस खजाने के नक्शे को स्वचालित रूप से निकाल सकते हैं। वे इसके परिणामस्वरूप बनने वाले नक्शे को हर्ब्रैंड सिस्टम (Herbrand System) कहते हैं। यह उदाहरणों की एक योजनाबद्ध सूची है जो किसी भी संख्या $n$ के लिए काम करती है, जो सीधे ब्लूप्रिंट से उत्पन्न होती है।

4. संबंध: "चक्रीय प्रमाण" बनाम "ब्लूप्रिंट्स" (Cyclic Proofs vs. Blueprints)

अनंत प्रक्रियाओं को संभालने का एक अन्य तरीका जिसे चक्रीय प्रमाण (Cyclic Proofs) कहा जाता है।

उपमा: एक ऐसे प्रमाण की कल्पना करें जो एक वृत्त खींचता है। यह कहता है, "इसे सिद्ध करने के लिए, मुझे उस हिस्से को सिद्ध करने की आवश्यकता है, जो वापस शुरुआत की ओर ले जाता है, लेकिन एक छोटी संख्या के साथ।" यह एक लूप है।
शोध पत्र की उपलब्धि: लेखकों ने एक अनुवादक (translator) बनाया है। उन्होंने दिखाया कि इन "लूपिंग" प्रमाणों (Cyclical Proofs) का एक बड़ा वर्ग उनके "ब्लूप्रिंट्स" (Proof Schemata) में परिवर्तित किया जा सकता है।
यह क्यों मायने रखता है: एक बार परिवर्तित होने के बाद, "ब्लूप्रिंट" का उपयोग उस खजाने के नक्शे (Herbrand System) को निकालने के लिए किया जा सकता है जो पहले "लूपिंग" प्रमाण में ढूंढना कठिन था।

5. बड़ा परीक्षण: "टू-हाइड्रा" मॉन्स्टर (The Two-Hydra Monster)

यह सिद्ध करने के लिए कि उनका तरीका शक्तिशाली है, उन्होंने टू-हाइड्रा स्टेटमेंट (Two-Hydra Statement) नामक एक प्रसिद्ध, कठिन समस्या पर इसका परीक्षण किया।

कहानी: एक हाइड्रा (एक राक्षस) की कल्पना करें जिसके दो सिर हैं। हर बार जब आप एक सिर काटते हैं, तो वह वापस उग आता है, लेकिन एक विशिष्ट, जटिल तरीके से। प्रश्न यह है: "क्या आप अंततः इस हाइड्रा को मार सकते हैं?"
परिणाम:
- एक मानक तर्क प्रणाली (जिसे LKID कहा जाता है) यह सिद्ध नहीं कर सकती कि हाइड्रा को मारा जा सकता है। यह बहुत कमजोर है।
- "लूप्स" का उपयोग करने वाली एक प्रणाली (जिसे CLKID कहा जाता है) इसे सिद्ध कर सकती है।
- लेखकों की जीत: उन्होंने हाइड्रा के "लूपिंग" प्रमाण को अपने "ब्लूप्रिंट" में बदल दिया। उन्होंने सिद्ध किया कि उनका ब्लूप्रिंट काम करता है (यह समाप्त होता है) और सफलतापूर्वक उस "खजाने के नक्शे" (Herbrand System) को निकाला जिसने दिखाया कि हाइड्रा को ठीक कैसे हराया जाता है।
- निष्कर्ष: उनकी विधि मानक तर्क प्रणाली से अधिक शक्तिशाली है क्योंकि यह उन समस्याओं (जैसे हाइड्रा) को हल कर सकती है जिन्हें मानक प्रणाली नहीं कर सकती, जबकि साथ ही विस्तृत "खजाने के नक्शे" (उदाहरणों) को भी प्रदान करती है।

सारांश

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

तकनीकी सारांश: स्कीमाटा (Schemata), चक्रीय प्रमाण (Cyclic Proofs) और हर्ब्रैंड सिस्टम (Herbrand Systems)

समस्या विवरण
यह शोध पत्र औपचारिक तर्क (formal logic) के भीतर आगमनात्मक प्रमाणों (inductive proofs) के विश्लेषण की चुनौती को संबोधित करता है, जो विशेष रूप से गणितीय आगमन (mathematical induction) का उपयोग करने वाले प्रमाणों से गणनात्मक सामग्री (हर्ब्रैंड सूचना) निकालने पर केंद्रित है। जबकि हर्ब्रैंड का प्रमेय 'कट-फ्री' (cut-free) प्रमाणों में प्रस्तावात्मक (propositional) और क्वांटिफायर अनुमानों को अलग करने के लिए एक तंत्र प्रदान करता है, यह आगमन सिद्धांत (induction principle) की उपस्थिति में विफल रहता है। फलस्वरूप, मानक आगमनात्मक प्रमाणों से "हर्ब्रैंड सूचना" निकालना असंभव माना जाता रहा है।

आगमनात्मक तर्क के मौजूदा दृष्टिकोणों में 'प्रूफ स्कीमाटा' (प्रमाण अनुक्रमों की पुनरावर्ती परिभाषाएँ) और 'चक्रीय प्रमाण प्रणाली' (ट्रेस स्थितियों द्वारा न्यायसंगत वैश्विक प्रमाण संरचनाएँ) शामिल हैं। जबकि प्रिमिटिव रिकर्सन (primitive recursion) पर आधारित प्रूफ स्कीमाटा के लिए हर्ब्रैंड सिस्टम सफलतापूर्वक कंप्यूट किए गए हैं, और हाल के कार्यों ने दिखाया है कि हायर-ऑर्डर रिकर्सन स्कीम्स के माध्यम से चक्रीय प्रमाणों से हर्ब्रैंड संरचनाएं निकाली जा सकती हैं, चक्रीय प्रमाणों और प्रूफ स्कीमाटा के माध्यम से हर्ब्रैंड सिस्टम निकालने के बीच एक सीधा संबंध खुला रह गया था। इसके अतिरिक्त, प्रूफ स्कीमाटा की अभिव्यंजक शक्ति $CLKID_\omega$ जैसे चक्रीय प्रमाणों की तुलना में सीमित थी, जो ऐसे कथनों (जैसे, 2-हाइड्रा कथन) को सिद्ध कर सकते हैं जो मानक आगमनात्मक कैलकुलस $LKID$ में अप्राप्य हैं।

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

पॉइंट ट्रांजिशन सिस्टम (PTS): लेखक उन वस्तुओं से स्वतंत्र होकर रिकर्सिव कॉल्स का वर्णन करने के लिए एक ढांचा विकसित करते हैं जिन्हें परिभाषित किया जा रहा है। एक PTS लेबल किए गए बिंदुओं (एक लेबल और पैरामीटर्स के टुपल का जोड़ा) और शर्तों द्वारा नियंत्रित ट्रांजिशन से बना होता है। महत्वपूर्ण रूप से, वे कैनोनिक (canonic) PTS को परिभाषित करते हैं, जो सभी पैरामीटर असाइनमेंट के लिए टर्मिनेशन (समाप्ति) सुनिश्चित करने के लिए एक वेल-फाउंडेड ऑर्डरिंग को स्वीकार करते हैं। यह प्रमाण घटकों के बीच रिकर्सिव कॉल्स के माध्यम से प्रमाण अनुक्रमों का प्रतिनिधित्व करने वाले प्रूफ स्कीमाटा को परिभाषित करने की अनुमति देता है।
**स्कीमैटिक लॉजिक ($LKN $):** लेखक प्राकृतिक संख्याओं पर एक सिक्वेंट कैलकुलस$ LKN$ पेश करते हैं, जो पैरामीटर्स पर कमजोर क्वांटिफिकेशन (weak quantification) की अनुमति देता है, लेकिन पैरामीटर असाइनमेंट को प्रमाणों पर लागू करने के दौरान अर्थ संबंधी समस्याओं (semantic issues) से बचने के लिए स्ट्रॉन्ग क्वांटिफिकेशन को प्रतिबंधित करता है।
स्कीमाटा के लिए हर्ब्रैंड सिस्टम: उन प्रूफ स्कीमाटा के लिए जिनमें अधिकतम क्वांटिफायर-फ्री कट्स होते हैं, यह शोध पत्र हर्ब्रैंड सिस्टम कंप्यूट करने की विधि को परिभाषित करता है। ये क्वांटिफाइड फॉर्मूला के हर्ब्रैंड इंस्टेंस के स्कीमाटा हैं। इस पद्धति में क्वांटिफाइड फॉर्मूला के उद्भव (occurrences) को प्रमाण स्कीमा (रिकर्सिव कॉल्स सहित) के माध्यम से ट्रैक करना शामिल है ताकि प्रतिस्थापन (substitutions) एकत्र किए जा सकें, जो स्पष्ट आगमन नियमों के बिना आगमनात्मक प्रमाणों के लिए हर्ब्रैंड के प्रमेय को प्रभावी रूप से साकार करता है।
चक्रीय प्रमाणों से अनुवाद: शोध पत्र एक एल्गोरिदम, transformIntoSchema, प्रस्तुत करता है जो चक्रीय प्रमाणों ( $CLKID_\omega$ $C L K I D_{ω}$ ) के एक विशिष्ट उप-वर्ग को प्रूफ स्कीमाटा में अनुवादित करता। यह अनुवाद उन चक्रीय प्रमाणों के लिए प्रतिबंधित है जहाँ:
- आगमनात्मक परिभाषाएँ एक विशिष्ट "डेफिनेशन टाइप" की हैं (प्रिमिस नए वेरिएबल्स पेश नहीं करते हैं, और प्रोडक्शंस युग्मवार गैर-ओवरलैपिंग हैं)।
- इंडक्टिव व्यवहार को नियंत्रित करने वाले वेरिएबल्स कहीं और स्ट्रॉन्गली क्वांटिफाइड नहीं हैं।
  एल्गोरिदम पांच चरणों में आगे बढ़ता है:
- इनिशियलाइजेशन (Initialization): इंडक्टिव डेफिनिशन को फर्स्ट-ऑर्डर एक्सिओम्स ( $p_{def}$ ) के रूप में एनकोड करना।
- साइकिल डिकंपोजिशन (Cycle Decomposition): कंपैनियन नोड्स (बैक-लिंक्स के लक्ष्य) की पहचान करना और चक्रीय प्रमाण को परिमित उप-डेरिवाशन्स में विभाजित करना।
- केस पार्टीशनिंग (Case Partitioning): ब्रांचिंग को संभालने के लिए केस-स्प्लिट नियमों के आधार पर डेरिवाशन्स को विभाजित करना।
- सबडेरिवेशन ट्रांसफॉर्मेशन (Subderivation Transformation): गार्ड्स को सामान्य करने, प्रेडेसेसर फंक्शन्स के माध्यम से ऑक्जिलरी वेरिएबल्स को हटाने और कंपैनियन/बड नोड्स को प्रूफ टर्म्स से बदलने के माध्यम से उप-डेरिवाशन्स को $s$ -प्रूफ्स (स्कीमैटिक प्रमाणों) में बदलना।
- स्कीमा असेंबली (Schema Assembly): अंतिम प्रमाण स्कीमा में घटकों को एकत्रित करना।

प्रमुख योगदान और परिणाम

नया प्रूफ स्कीमा फॉर्मलिज्म: शोध पत्र पॉइंट ट्रांजिशन सिस्टम पर आधारित प्रूफ स्कीमाटा पेश करता है। प्रिमिटिव रिकर्सन पर आधारित पिछले स्कीमाटा के विपरीत, यह फॉर्मलिज्म अधिक जटिल रिकर्सिव संरचनाओं का समर्थन करता है, जिससे इसकी शक्ति बढ़ जाती है।
आगमनात्मक प्रमाणों के लिए हर्ब्रैंड सिस्टम: लेखक सिद्ध करते हैं कि अधिकतम क्वांटिफायर-फ्री कट्स वाले प्रूफ स्कीमाटा (PTS पर आधारित) के लिए, हर्ब्रैंड सिस्टम और स्कीमैटिक हर्ब्रैंड सिक्वेंट्स प्रभावी रूप से कंप्यूट किए जा सकते हैं। यह प्रिमिटिव रिकर्सन तक सीमित पिछले परिणामों का विस्तार करता है।
अनुवाद एल्गोरिदम: एक कंस्ट्रक्टिव एल्गोरिदम प्रदान किया गया है जो $CLKID_\omega$ प्रमाणों के एक महत्वपूर्ण उप-वर्ग को प्रूफ स्कीमाटा में अनुवादित करता है। यह चक्रीय प्रमाणों और स्कीमैटिक CERES विधि के बीच एक सीधा लिंक स्थापित करता है, जिससे चक्रीय प्रमाणों से हर्ब्रैंड सिस्टम का सीधा निष्कर्षण संभव होता है।
2-हाइड्रा उदाहरण: शोध पत्र 2-हाइड्रा कथन पर इस अनुवाद को लागू करता है, जो बेराडी और तात्सुटा द्वारा पेश किया गया एक प्रसिद्ध उदाहरण है।
- 2-हाइड्रा कथन $CLKID_\omega$ में सिद्ध करने योग्य है लेकिन $LKID$ में नहीं।
- लेखक 2-हाइड्रा चक्रीय प्रमाण को पॉइंट ट्रांजिशन सिस्टम पर आधारित एक प्रूफ स्कीमा में सफलतापूर्वक अनुवादित करते हैं।
- वे प्रदर्शित करते हैं कि संबंधित पॉइंट ट्रांजिशन सिस्टम टर्मिनेटिंग (कैनोनिक) है।
- वे इस स्कीमा के लिए संगत हर्ब्रैंड सिस्टम को निकालते हैं।

महत्व और दावे
इस कार्य का प्राथमिक महत्व, जैसा कि लेखकों द्वारा दावा किया गया है, दोहरा है:

अभिव्यंजक शक्ति (Expressive Power): शोध पत्र प्रदर्शित करता है कि पॉइंट ट्रांजिशन सिस्टम पर आधारित प्रूफ स्कीमाटा उन आगमनात्मक कथनों को सिद्ध करने में सक्षम हैं जो $LKID$ में सिद्ध करने योग्य नहीं हैं। विशेष रूप से, 2-हाइड्रा चक्रीय प्रमाण को अनुवादित करके, लेखक दिखाते हैं कि उनका फॉर्मलिज्म मानक आगमनात्मक कैलकुलस की पहुंच से परे आगमनात्मक तर्कों को समाहित करता है।
ढांचों का एकीकरण (Unification of Frameworks): यह कार्य चक्रीय प्रमाणों और प्रूफ स्कीमाटा के बीच के अंतर को पाटता है। एक एल्गोरिथमिक अनुवाद प्रदान करके, लेखक दिखाते हैं कि चक्रीय प्रमाणों को प्रूफ स्कीमाटा के स्रोत के रूप में देखा जा सकता है, जिससे चक्रीय प्रमाणों के एक वर्ग से हर्ब्रैंड सिस्टम के निष्कर्षण और स्कीमैटिक CERES के अनुप्रयोग की अनुमति मिलती है।

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