2025-11-23T13:43:17.173951

Admissibility of Substitution Rule in Cyclic-Proof Systems

Saotome, Nakazawa

This paper investigates the admissibility of the substitution rule in cyclic-proof systems. The substitution rule complicates theoretical case analysis and increases computational cost in proof search since every sequent can be a conclusion of an instance of the substitution rule; hence, admissibility is desirable on both fronts. While admissibility is often shown by local proof transformations in non-cyclic systems, such transformations may disrupt cyclic structure and do not readily apply. Prior remarks suggested that the substitution rule is likely nonadmissible in the cyclic-proof system CLKID^omega for first-order logic with inductive predicates. In this paper, we prove admissibility in CLKID^omega, assuming the presence of the cut rule. Our approach unfolds a cyclic proof into an infinitary form, lifts the substitution rules, and places back edges to construct a cyclic proof without the substitution rule. If we restrict substitutions to exclude function symbols, the result extends to a broader class of systems, including cut-free CLKID^omega and cyclic-proof systems for the separation logic.

academic

चक्रीय-प्रमाण प्रणालियों में प्रतिस्थापन नियम की स्वीकार्यता

मूल जानकारी

पेपर ID: 2510.14749
शीर्षक: चक्रीय-प्रमाण प्रणालियों में प्रतिस्थापन नियम की स्वीकार्यता
लेखक: केंजी साओटोमे, कोजी नाकाज़ावा (नागोया विश्वविद्यालय)
वर्गीकरण: cs.LO (तर्कशास्त्र)
प्रकाशन समय: 16 अक्टूबर 2025
पेपर लिंक: https://arxiv.org/abs/2510.14749

सारांश

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

अनुसंधान पृष्ठभूमि और प्रेरणा

समस्या परिभाषा

चक्रीय प्रमाण पारंपरिक प्रमाण वृक्षों का विस्तार हैं, जो आगमनात्मक रूप से परिभाषित विधेयों के बारे में तर्क करने के लिए चक्रीय संरचनाओं को प्रस्तुत करते हैं। प्रतिस्थापन नियम $\frac{\Gamma \vdash \Delta}{\Gamma[\theta] \vdash \Delta[\theta]}$ (Subst) कई चक्रीय प्रमाण प्रणालियों में चक्रीय संरचना के निर्माण में सहायता के लिए प्रस्तुत किया गया है।

समस्या की महत्ता

सैद्धांतिक दृष्टिकोण: प्रतिस्थापन नियम हमेशा लागू होता है, जिससे प्रमाण विश्लेषण जटिल हो जाता है
व्यावहारिक दृष्टिकोण: प्रतिस्थापन नियम का असीमित अनुप्रयोग कम्प्यूटेशनल लागत को बढ़ाता है, क्योंकि प्रत्येक चरण में कई प्रतिस्थापन लागू हो सकते हैं

मौजूदा विधियों की सीमाएं

गैर-चक्रीय प्रमाण प्रणालियों में, प्रतिस्थापन नियम की स्वीकार्यता आमतौर पर दो चरणों में प्राप्त की जाती है:

उन्नयन चरण: प्रतिस्थापन नियम को ऊपर की ओर स्थानांतरित करना
उन्मूलन चरण: स्वयंसिद्धों पर प्रतिस्थापन नियम को समाप्त करना

लेकिन चक्रीय प्रमाण प्रणालियों में, यह विधि मौलिक कठिनाइयों का सामना करती है:

उन्नयन चरण कली-साथी संबंध (bud-companion relationship) को नष्ट कर सकता है
उन्मूलन चरण कली पर प्रतिस्थापन को समाप्त नहीं कर सकता

अनुसंधान प्रेरणा

ब्रदरस्टन 1 ने CLKIDω में प्रतिस्थापन नियम की स्वीकार्यता का प्रश्न उठाया, जिससे संकेत मिलता है कि सामान्य स्थिति में, कम से कम कट-मुक्त सेटिंग में, यह संभवतः स्वीकार्य नहीं है। यह पेपर इस खुली समस्या को हल करने का लक्ष्य रखता है।

मुख्य योगदान

प्रमुख सैद्धांतिक परिणाम: कट नियम की उपस्थिति में, CLKIDω में प्रतिस्थापन नियम स्वीकार्य है, यह सिद्ध किया गया है
विस्तारित परिणाम: जब प्रतिस्थापन को परमाणु प्रतिस्थापन तक सीमित किया जाता है (सकारात्मक अरिटी कार्य प्रतीकों को प्रस्तुत न करने वाला), तो परिणाम कट-मुक्त CLKIDω तक विस्तारित होता है
अनुप्रयोग सामान्यीकरण: यह परिणाम अन्य प्रमाण प्रणालियों पर लागू होता है, जैसे पृथक्करण तर्क की चक्रीय प्रमाण प्रणाली
नवीन विधि: अनंत विस्तार, प्रतिस्थापन उन्नयन और चक्रीय पुनर्निर्माण के माध्यम से तीन-चरणीय उन्मूलन रणनीति प्रस्तावित की गई है

विधि विवरण

कार्य परिभाषा

CLKIDω में प्रतिस्थापन नियम युक्त प्रमाण Pr+ दिया गया है, एक ऐसा प्रमाण Pr- बनाएं जिसमें प्रतिस्थापन नियम न हो, ताकि दोनों एक ही अनुक्रम को सिद्ध करें।

मुख्य विधि आर्किटेक्चर

इस पेपर की उन्मूलन प्रक्रिया दो मुख्य चरणों में विभाजित है:

1. समग्र प्रतिस्थापन का उन्मूलन

परिभाषा:

परमाणु प्रतिस्थापन: केवल चर और स्थिरांक युक्त प्रतिस्थापन
समग्र प्रतिस्थापन: सकारात्मक अरिटी कार्य प्रतीकों युक्त पद वाले प्रतिस्थापन

विधि: निम्नलिखित परिवर्तन के माध्यम से समग्र प्रतिस्थापन को समाप्त करना:

Γ ⊢ Δ
────────────────────────── (Subst)
Γ[x₁:=t₁,...,xₙ:=tₙ] ⊢ Δ[x₁:=t₁,...,xₙ:=tₙ]

कट नियम, समानता नियम और अस्तित्वगत परिमाणक नियम के संयोजन का उपयोग करके परिवर्तित करना, अंततः केवल परमाणु प्रतिस्थापन को संरक्षित करना।

2. परमाणु प्रतिस्थापन का उन्मूलन

यह मुख्य नवाचार है, जिसमें तीन चरण शामिल हैं:

चरण 1: चक्रीय विस्तार

चक्रीय प्रमाण Pr_var+ को अनंत प्रमाण Pr^ω में विस्तारित करना
मानचित्र f^ω: Seq(Pr^ω) → Seq(Pr_var+) को परिभाषित करना जो अनुक्रम घटनाओं को जोड़ता है

चरण 2: प्रतिस्थापन उन्नयन

गहराई d के भीतर प्रतिस्थापन नियम के बिना LKIDω प्रमाण Pr^ω_d को पुनरावर्ती रूप से बनाना
प्रतिस्थापन-अनुप्रयोग गुण का उपयोग करना

चरण 3: चक्रीय पुनर्निर्माण

Pr^ω_d से CLKIDω पूर्व-प्रमाण Pr- बनाना
कली और साथी का चयन करना, वैश्विक ट्रेस स्थिति को सुनिश्चित करना

तकनीकी नवाचार बिंदु

1. आंशिक प्रतिस्थापन संवरण (Partial-substitution Closure)

परिभाषा 10: प्रतिस्थापन समुच्चय Θ और चर समुच्चय X दिए गए हैं, आंशिक प्रतिस्थापन संवरण Cps(Θ,X) निम्नलिखित शर्तों को संतुष्ट करने वाला न्यूनतम समुच्चय है:

Θ ⊆ Cps(Θ,X)
θ∈Cps(Θ,X) और x,y∈X के लिए: θx→y ∈ Cps(Θ,X)
θ₁,θ₂∈Cps(Θ,X) के लिए: θ₁θ₂ ∈ Cps(Θ,X)

मुख्य गुण: जब परमाणु प्रतिस्थापन तक सीमित किया जाता है, तो आंशिक प्रतिस्थापन संवरण परिमित होता है।

2. प्रतिस्थापन-अनुप्रयोग गुण (Substitution-application Property)

परिभाषा 11: नियम (R) प्रतिस्थापन-अनुप्रयोग गुण को संतुष्ट करता है, यदि किसी भी नियम उदाहरण और परमाणु प्रतिस्थापन θ के लिए, संबंधित प्रतिस्थापन-अनुप्रयोग उदाहरण मौजूद है, और ट्रेस को संरक्षित करता है।

लेम्मा 4: CLKIDω और LKIDω प्रतिस्थापन-अनुप्रयोग गुण को संतुष्ट करते हैं।

3. वैश्विक ट्रेस स्थिति का संरक्षण

संबंधित पथ की अवधारणा के माध्यम से पुनर्निर्मित प्रमाण की वैश्विक ट्रेस स्थिति को सुनिश्चित करना:

परिभाषा 12: Pr- में पथ (eᵢ) के लिए, Pr_var+ में संबंधित पथ (e'ⱼ) को परिभाषित करना, ताकि प्रत्येक अनंत प्रगति ट्रेस को संरक्षित किया जाए।

प्रायोगिक सेटअप

यह पेपर शुद्ध सैद्धांतिक कार्य है, जिसमें पारंपरिक अर्थ में कोई प्रयोग नहीं है। सत्यापन निम्नलिखित तरीकों से किया जाता है:

सैद्धांतिक सत्यापन

रचनात्मक प्रमाण: स्पष्ट निर्माण एल्गोरिदम के माध्यम से स्वीकार्यता सिद्ध करना
प्रतिउदाहरण विश्लेषण: सीमित शर्तों के तहत स्वीकार्यता को संतुष्ट न करने वाले मामलों का विश्लेषण
प्रणाली विस्तार: अन्य प्रणालियों में परिणामों की प्रयोज्यता का सत्यापन

उदाहरण विश्लेषण

पेपर ठोस प्रमाण परिवर्तन उदाहरण प्रदान करता है:

चित्र 1: प्रतिस्थापन नियम युक्त चक्रीय प्रमाण
चित्र 3: विस्तारित अनंत प्रमाण
N(x) ⊢ E(x)∨O(x) के चक्रीय प्रमाण से प्रतिस्थापन नियम को कैसे समाप्त किया जाए, यह दिखाता है

प्रायोगिक परिणाम

मुख्य सैद्धांतिक परिणाम

प्रमेय 2 (CLKIDω में प्रतिस्थापन नियम की स्वीकार्यता): यदि Γ ⊢ Δ CLKIDω में सिद्ध है, तो यह (Subst) के बिना CLKIDω में भी सिद्ध है।

प्रमेय 3 (परमाणु प्रतिस्थापन का मजबूत परिणाम): यदि Pr CLKIDω में Γ ⊢ Δ का प्रमाण है और Θ(Pr) केवल परमाणु प्रतिस्थापन युक्त है, तो (Subst) के बिना प्रमाण मौजूद है, और केवल Pr में दिखाई देने वाले नियमों को शामिल करता है।

विस्तारित परिणाम

प्रमेय 4 (कट-मुक्त प्रणाली में स्वीकार्यता): CLKIDω^- (कट-मुक्त CLKIDω) में, परमाणु प्रतिस्थापन नियम स्वीकार्य है।

प्रमेय 5 (पृथक्करण तर्क में अनुप्रयोग): प्रतिस्थापन नियम CSLω और CSLω^- दोनों में स्वीकार्य है।

सैद्धांतिक निष्कर्ष

कट नियम की महत्वपूर्ण भूमिका: समग्र प्रतिस्थापन के उन्मूलन के लिए कट नियम आवश्यक है
परमाणु प्रतिस्थापन की सार्वभौमिकता: परमाणु प्रतिस्थापन का उन्मूलन व्यापक प्रणालियों पर लागू होता है
कार्य प्रतीकों की सीमितता: कार्य प्रतीकों की उपस्थिति स्वीकार्यता की मुख्य बाधा है

निष्कर्ष और चर्चा

मुख्य निष्कर्ष

कट नियम की उपस्थिति में CLKIDω में, प्रतिस्थापन नियम स्वीकार्य है
जब परमाणु प्रतिस्थापन तक सीमित किया जाता है, तो परिणाम कट-मुक्त प्रणालियों तक विस्तारित होता है
यह परिणाम पृथक्करण तर्क जैसी अन्य महत्वपूर्ण प्रणालियों पर लागू होता है

सीमाएं

कट नियम पर निर्भरता: समग्र प्रतिस्थापन के उन्मूलन के लिए कट नियम आवश्यक है
कार्य प्रतीक प्रतिबंध: पूर्ण सामान्य परिणाम के लिए कार्य प्रतीकों को बाहर करने की आवश्यकता है
निर्माण जटिलता: प्रमाण परिवर्तन प्रक्रिया अपेक्षाकृत जटिल है

भविष्य की दिशाएं

न्यूनतम नियम समुच्चय: कार्य प्रतीकों की उपस्थिति में भी प्रतिस्थापन नियम उन्मूलन की अनुमति देने वाले न्यूनतम नियम समुच्चय का अनुसंधान
कट उन्मूलन: अतिरिक्त नियमों को प्रस्तुत करके चक्रीय प्रमाण प्रणालियों के कट उन्मूलन गुण का अनुसंधान
कम्प्यूटेशनल जटिलता: प्रतिस्थापन नियम उन्मूलन की कम्प्यूटेशनल जटिलता का विश्लेषण

गहन मूल्यांकन

लाभ

सैद्धांतिक महत्व: इस क्षेत्र की एक महत्वपूर्ण खुली समस्या को हल करता है
विधि नवाचार: चक्रीय संरचना के लिए लागू नई तकनीकें प्रस्तावित करता है
कठोरता: प्रमाण कठोर और रचनात्मक है
व्यापक प्रयोज्यता: परिणाम कई संबंधित प्रणालियों पर लागू होते हैं
स्पष्ट अभिव्यक्ति: तकनीकी विवरण स्पष्ट रूप से व्यक्त किए गए हैं, समझने में आसान

कमियां

व्यावहारिक प्रयोज्यता सीमा: कट नियम पर निर्भरता व्यावहारिक अनुप्रयोग को सीमित करती है
जटिलता: प्रमाण परिवर्तन प्रक्रिया अपेक्षाकृत जटिल है
पूर्णता: कट-मुक्त सेटिंग में अभी भी प्रतिबंध हैं

प्रभाव

सैद्धांतिक योगदान: चक्रीय प्रमाण सिद्धांत के लिए महत्वपूर्ण सैद्धांतिक आधार प्रदान करता है
व्यावहारिक मूल्य: प्रमाण खोज कार्यान्वयन के लिए अधिक लचीलापन प्रदान करता है
विस्तारणीयता: विधि अन्य संबंधित प्रणालियों पर लागू हो सकती है

प्रयोज्य परिदृश्य

स्वचालित प्रमेय प्रमाण: चक्रीय प्रमाण खोज की दक्षता में सुधार
कार्यक्रम सत्यापन: पृथक्करण तर्क जैसे सत्यापन ढांचे में अनुप्रयोग
सैद्धांतिक अनुसंधान: चक्रीय प्रमाण सिद्धांत के आगे के अनुसंधान के लिए आधार

संदर्भ

पेपर 19 संबंधित संदर्भों का हवाला देता है, मुख्य रूप से:

ब्रदरस्टन का चक्रीय प्रमाण अग्रणी कार्य
पृथक्करण तर्क में चक्रीय प्रमाण के अनुप्रयोग अनुसंधान
स्वचालित प्रमाण खोज का संबंधित कार्य
कट उन्मूलन और प्रमाण सिद्धांत का मूलभूत अनुसंधान

यह पेपर चक्रीय प्रमाण सिद्धांत में महत्वपूर्ण योगदान देता है, नवीन तकनीकी साधनों के माध्यम से एक महत्वपूर्ण खुली समस्या को हल करता है, और इस क्षेत्र के आगे के विकास के लिए आधार तैयार करता है।