कट-उन्मूलन प्रमेय: Difference between revisions

Latest revision as of 09:55, 4 August 2023

कट-उन्मूलन प्रमेय (या जेंटज़ेन का हौप्त्सत्ज़) अनुक्रमिक कलन के महत्व को स्थापित करने वाला केंद्रीय परिणाम है। इसे मूल रूप से गेरहार्ड जेंटज़न ने अपने ऐतिहासिक 1934 के पेपर इन्वेस्टिगेशंस इन लॉजिकल डिडक्शन में प्रणाली प्रणाली एल.जे और प्रणाली एलके के लिए क्रमशः अंतर्ज्ञानवादी तर्क और मौलिक तर्क को औपचारिक रूप से सिद्ध किया था। कट-उन्मूलन प्रमेय में कहा गया है कि कोई भी निर्णय जिसमें कट नियम का उपयोग करते हुए अनुक्रमिक कलन में प्रमाण होता है, उसके समीप कट-मुक्त प्रमाण भी होता है, अर्थात ऐसा प्रमाण जो कट नियम का उपयोग नहीं करता है।^[1]^[2]

कट नियम

अनुक्रम अनेक सूत्रों से संबंधित एक तार्किक अभिव्यक्ति है, "" $A_{1},A_{2},A_{3},\ldots \vdash B_{1},B_{2},B_{3},\ldots$ "" के रूप में, जिसे "" $A_{1},A_{2},A_{3},\ldots$ सिद्ध होता है $B_{1},B_{2},B_{3},\ldots$ ", और (जैसा कि जेंटज़ेन द्वारा स्पष्ट किया गया है) को सत्य-फ़ंक्शन के समतुल्य समझा जाना चाहिए "यदि ( $A_{1}$ और $A_{2}$ और $A_{3}$ …) तो ( $B_{1}$ या $B_{2}$ या $B_{3}$ …)।"^[3] ध्यान दें कि बाएं हाथ की ओर (एलएचएस) एक संयोजन (और) है और दाईं ओर (आरएचएस) एक विच्छेदन (या) है।

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

अनुक्रमिक कैलकुलस के सामान्य कथन में कट एक नियम है, और अन्य प्रमाण सिद्धांत में विभिन्न नियमों के समान है, जो दिया गया है

$\Gamma \vdash A,\Delta$

और

$\Pi ,A\vdash \Lambda$

किसी को अनुमान लगाने की अनुमति देता है

$\Gamma ,\Pi \vdash \Delta ,\Lambda$

अर्थात्, यह सूत्र A की घटनाओं को अनुमानात्मक संबंध से "कट " कर देता है।

कट उन्मूलन

कट-उन्मूलन प्रमेय में कहा गया है कि (किसी दिए गए प्रणाली के लिए) कट नियम का उपयोग करके सिद्ध किए जाने वाले किसी भी अनुक्रम को इस नियम के उपयोग के बिना सिद्ध किया जा सकता है।

अनुक्रमिक गणनाओं के लिए जिनका आरएचएस में केवल एक सूत्र है, कट नियम दिया गया है

$\Gamma \vdash A$

और

$\Pi ,A\vdash B$

किसी को अनुमान लगाने की अनुमति देता है

$\Gamma ,\Pi \vdash B$

यदि हम $B$ को एक प्रमेय के रूप में विचार करते हैं, तो इस स्थिति में कट-एलिमिनेशन बस यह कहता है कि इस प्रमेय को सिद्ध करने के लिए उपयोग किया गया एक लेम्मा $A$ इनलाइन किया जा सकता है। जब भी प्रमेय के प्रमाण में लेम्मा $A$ का उल्लेख होता है, हम $A$ के प्रमाण के लिए घटनाओं को प्रतिस्थापित कर सकते हैं। परिणाम स्वरुप, कट नियम स्वीकार्य है।

प्रमेय के परिणाम

अनुक्रमिक कलन में तैयार की गई प्रणालियों के लिए, विश्लेषणात्मक प्रमाण वे प्रमाण हैं जो कट का उपयोग नहीं करते हैं। समान्यत: ऐसा प्रमाण निश्चित रूप से लंबा होगा, जिसमे और आवश्यक नहीं कि यह तुच्छ हो। अपने निबंध डोंट एलिमिनेट कट में!^[4] जॉर्ज बूलोस ने प्रदर्शित किया कि एक व्युत्पत्ति थी जिसे कट का उपयोग करके एक पृष्ठ में पूर्ण किया जा सकता था, किंतु जिसका विश्लेषणात्मक प्रमाण ब्रह्मांड के जीवनकाल में पूर्ण नहीं किया जा सकता था।

इस प्रमेय के अनेक , समृद्ध परिणाम हैं:

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

क्रेग प्रक्षेप को सिद्ध करने के लिए कट एलिमिनेशन अधिक शक्तिशाली उपकरणों में से एक है। प्रथम-क्रम रिज़ॉल्यूशन के आधार पर प्रमाण खोज करने की संभावना, प्रोलॉग प्रोग्रामिंग भाषा के लिए आवश्यक अंतर्दृष्टि, उपयुक्त प्रणाली में कट की स्वीकार्यता पर निर्भर करती है।

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

यह भी देखें

कट प्रमेय
पीनो के सिद्धांतों के लिए जेंटज़ेन की स्थिरता का प्रमाण

↑ Curry 1977, pp. 208–213, gives a 5-page proof of the elimination theorem. See also pages 188, 250.
↑ Kleene 2009, pp. 453, gives a very brief proof of the cut-elimination theorem.
↑ Wilfried Buchholz, Beweistheorie (university lecture notes about cut-elimination, German, 2002-2003)
↑ Boolos 1984, pp. 373–378

संदर्भ

Gentzen, Gerhard (1935). "Untersuchungen über das logische Schließen. I.". Mathematische Zeitschrift. 39: 176–210. doi:10.1007/BF01201353.
- Untersuchungen über das logische Schließen I (Archive.org)
- Gentzen, Gerhard (1964). "Investigations into logical deduction". American Philosophical Quarterly. 1 (4): 249–287.
Gentzen, Gerhard (1935). "Untersuchungen über das logische Schließen. II". Mathematische Zeitschrift. 39: 405–431. doi:10.1007/BF01201363.
- Untersuchungen über das logische Schließen II (Archive.org)
- Gentzen, Gerhard (1965). "Investigations into logical deduction". American Philosophical Quarterly. 2 (3): 204–218.
Curry, Haskell Brooks (1977) [1963]. Foundations of mathematical logic. New York: Dover Publications Inc. ISBN 978-0-486-63462-3.
Kleene, Stephen Cole (2009) [1952]. Introduction to metamathematics. Ishi Press International. ISBN 978-0-923891-57-2.
Boolos, George (1984). "Don't eliminate cut". Journal of Philosophical Logic. 13 (4): 373–378.

बाहरी संबंध

Alex Sakharov. "Cut Elimination Theorem". MathWorld.
Dragalin, A.G. (2001) [1994], "Sequent calculus", Encyclopedia of Mathematics, EMS Press

[1] Curry 1977, pp. 208–213, gives a 5-page proof of the elimination theorem. See also pages 188, 250.

[2] Kleene 2009, pp. 453, gives a very brief proof of the cut-elimination theorem.

[3] Wilfried Buchholz, Beweistheorie (university lecture notes about cut-elimination, German, 2002-2003)

[4] Boolos 1984, pp. 373–378

[1]

[2]

[3]

[4]

@@ Line 1: / Line 1: @@
 {{Short description|Theorem in formal logic}}
-कट-उन्मूलन प्रमेय (या जेंटज़ेन का ''हौप्त्सत्ज़'') अनुक्रमिक कलन के महत्व को स्थापित करने वाला केंद्रीय परिणाम है। इसे मूल रूप से [[गेरहार्ड जेंटज़न]] ने अपने ऐतिहासिक 1934 के पेपर इन्वेस्टिगेशंस इन लॉजिकल डिडक्शन में सिस्टम [[ सिस्टम एल.जे ]] और [[सिस्टम एलके]] के लिए क्रमशः [[अंतर्ज्ञानवादी तर्क]] और [[शास्त्रीय तर्क]] को औपचारिक रूप से साबित किया था। कट-उन्मूलन प्रमेय में कहा गया है कि कोई भी निर्णय जिसमें कट नियम का उपयोग करते हुए अनुक्रमिक कलन में प्रमाण होता है, उसके पास कट-मुक्त प्रमाण भी होता है, अर्थात ऐसा प्रमाण जो कट नियम का उपयोग नहीं करता है।<ref>{{harvnb|Curry|1977|pp=208–213}}, gives a 5-page proof of the elimination theorem. See also pages 188, 250.</ref><ref>{{harvnb|Kleene|2009|pp=453}}, gives a very brief proof of the cut-elimination theorem.</ref>
+'''कट-उन्मूलन प्रमेय''' (या जेंटज़ेन का ''हौप्त्सत्ज़'') अनुक्रमिक कलन के महत्व को स्थापित करने वाला केंद्रीय परिणाम है। इसे मूल रूप से [[गेरहार्ड जेंटज़न]] ने अपने ऐतिहासिक 1934 के पेपर इन्वेस्टिगेशंस इन लॉजिकल डिडक्शन में प्रणाली [[ सिस्टम एल.जे |प्रणाली एल.जे]] और [[सिस्टम एलके|प्रणाली एलके]] के लिए क्रमशः [[अंतर्ज्ञानवादी तर्क]] और [[शास्त्रीय तर्क|मौलिक तर्क]] को औपचारिक रूप से सिद्ध किया था। कट-उन्मूलन प्रमेय में कहा गया है कि कोई भी निर्णय जिसमें कट नियम का उपयोग करते हुए अनुक्रमिक कलन में प्रमाण होता है, उसके समीप कट-मुक्त प्रमाण भी होता है, अर्थात ऐसा प्रमाण जो कट नियम का उपयोग नहीं करता है।<ref>{{harvnb|Curry|1977|pp=208–213}}, gives a 5-page proof of the elimination theorem. See also pages 188, 250.</ref><ref>{{harvnb|Kleene|2009|pp=453}}, gives a very brief proof of the cut-elimination theorem.</ref>
+==कट नियम                                                                                                                                                   ==
+अनुक्रम अनेक सूत्रों से संबंधित एक तार्किक अभिव्यक्ति है, "{{nowrap|"<math>A_1, A_2, A_3, \ldots \vdash B_1, B_2, B_3, \ldots</math>"}}" के रूप में, जिसे "{{nowrap|"<math>A_1, A_2, A_3, \ldots</math>}} सिद्ध होता है {{nowrap|<math>B_1, B_2, B_3, \ldots</math>"}}, और (जैसा कि जेंटज़ेन द्वारा स्पष्ट किया गया है) को सत्य-फ़ंक्शन के समतुल्य समझा जाना चाहिए "यदि (<math>A_1</math> और <math>A_2</math> और <math>A_3</math> …) तो (<math>B_1</math> या <math>B_2</math> या <math>B_3</math> …)।"<ref>Wilfried Buchholz, [http://www.mathematik.uni-muenchen.de/~buchholz/articles/beweisth.ps Beweistheorie] (university lecture notes about cut-elimination, German, 2002-2003)</ref> ध्यान दें कि बाएं हाथ की ओर (एलएचएस) एक संयोजन (और) है और दाईं ओर (आरएचएस) एक विच्छेदन (या) है।
+एलएचएस में इच्छित रूप से अनेक या कुछ सूत्र हो सकते हैं; जब एलएचएस रिक्त होता है, तो आरएचएस एक [[टॉटोलॉजी (तर्क)]] है। एलके में, आरएचएस में किसी भी संख्या में सूत्र हो सकते हैं - यदि इसमें कोई भी नहीं है, तो एलएचएस एक [[विरोधाभास]] है, जबकि एलजे में आरएचएस में केवल एक सूत्र हो सकता है या कोई भी नहीं: यहां हम देखते हैं कि आरएचएस में एक से अधिक सूत्र की अनुमति देना है समतुल्य, सही संकुचन नियम की उपस्थिति में, बहिष्कृत मध्य के नियम की स्वीकार्यता के लिए चूँकि अनुक्रमिक कैलकुलस एक अधिक अभिव्यंजक रूपरेखा है, और प्रस्तावित अंतर्ज्ञानवादी तर्क के लिए अनुक्रमिक कैलकुली हैं जो आरएचएस में अनेक सूत्रों की अनुमति देते हैं। [[जीन-यवेस गिरार्ड]] के तर्क एलसी से मौलिक तर्क की एक प्राकृतिक औपचारिकता प्राप्त करना सरल है जहां आरएचएस में अधिकतम एक सूत्र होता है; यह तार्किक और संरचनात्मक नियमों की परस्पर क्रिया है जो यहां की कुंजी है।
-==कटौती नियम==
+ अनुक्रमिक कैलकुलस के सामान्य कथन में कट एक नियम है, और अन्य [[प्रमाण सिद्धांत]] में विभिन्न नियमों के समान है, जो दिया गया है
-अनुक्रम एक तार्किक अभिव्यक्ति है जो कई सूत्रों से संबंधित होती है {{nowrap|"<math>A_1, A_2, A_3, \ldots \vdash B_1, B_2, B_3, \ldots</math>"}}, जिसे इस प्रकार पढ़ा जाना चाहिए {{nowrap|"<math>A_1, A_2, A_3, \ldots</math>}} सिद्ध होता है {{nowrap|<math>B_1, B_2, B_3, \ldots</math>"}}, और (जैसा कि जेंटज़ेन द्वारा स्पष्ट किया गया है) को सत्य-कार्य के समतुल्य समझा जाना चाहिए यदि (<math>A_1</math> और <math>A_2</math> और <math>A_3</math> …) तब (<math>B_1</math> या <math>B_2</math> या <math>B_3</math> …).<ref>Wilfried Buchholz, [http://www.mathematik.uni-muenchen.de/~buchholz/articles/beweisth.ps Beweistheorie] (university lecture notes about cut-elimination, German, 2002-2003)</ref> ध्यान दें कि बाईं ओर (LHS) एक संयोजन (और) है और दाईं ओर (RHS) एक वियोजन (या) है।
-एलएचएस में मनमाने ढंग से कई या कुछ सूत्र हो सकते हैं; जब एलएचएस खाली होता है, तो आरएचएस एक [[टॉटोलॉजी (तर्क)]] है। एलके में, आरएचएस में किसी भी संख्या में सूत्र हो सकते हैं - यदि इसमें कोई भी नहीं है, तो एलएचएस एक [[विरोधाभास]] है, जबकि एलजे में आरएचएस में केवल एक सूत्र हो सकता है या कोई भी नहीं: यहां हम देखते हैं कि आरएचएस में एक से अधिक सूत्र की अनुमति देना है समतुल्य, सही संकुचन नियम की उपस्थिति में, बहिष्कृत मध्य के कानून की स्वीकार्यता के लिए। हालाँकि, अनुक्रमिक कैलकुलस एक काफी अभिव्यंजक रूपरेखा है, और प्रस्तावित अंतर्ज्ञानवादी तर्क के लिए अनुक्रमिक कैलकुली हैं जो आरएचएस में कई सूत्रों की अनुमति देते हैं। [[जीन-यवेस गिरार्ड]] के तर्क एलसी से शास्त्रीय तर्क की एक प्राकृतिक औपचारिकता प्राप्त करना आसान है जहां आरएचएस में अधिकतम एक सूत्र होता है; यह तार्किक और संरचनात्मक नियमों की परस्पर क्रिया है जो यहां की कुंजी है।
+<ol><li><math> \Gamma \vdash A,\Delta
- अनुक्रमिक कैलकुलस के सामान्य कथन में कट एक नियम है, और अन्य [[प्रमाण सिद्धांत]] में विभिन्न नियमों के बराबर है, जो दिया गया है
+                              </math></li></ol>
-<ol><li><math> \Gamma \vdash A,\Delta</math></li></ol>
 और
-<ol प्रारंभ= 2 ><li><math> \Pi, A \vdash \Lambda</math></li></ol>
+<ol प्रारंभ= 2 ><li><math> \Pi, A \vdash \Lambda
+                                                                                </math></li></ol>
 किसी को अनुमान लगाने की अनुमति देता है
@@ Line 20: / Line 22: @@
 <ol प्रारंभ=3><li><math>\Gamma, \Pi \vdash \Delta,\Lambda</math></li></ol>
-अर्थात् यह सूत्र की घटनाओं को काट देता है <math>A</math> अनुमानित संबंध से बाहर.
+अर्थात्, यह सूत्र A की घटनाओं को अनुमानात्मक संबंध से "कट " कर देता है।
-==कटौती उन्मूलन==
+==कट उन्मूलन                                                                          ==
-कट-उन्मूलन प्रमेय में कहा गया है कि (किसी दिए गए सिस्टम के लिए) कट नियम का उपयोग करके सिद्ध किए जाने वाले किसी भी अनुक्रम को इस नियम के उपयोग के बिना सिद्ध किया जा सकता है।
+कट-उन्मूलन प्रमेय में कहा गया है कि (किसी दिए गए प्रणाली के लिए) कट नियम का उपयोग करके सिद्ध किए जाने वाले किसी भी अनुक्रम को इस नियम के उपयोग के बिना सिद्ध किया जा सकता है।
 अनुक्रमिक गणनाओं के लिए जिनका आरएचएस में केवल एक सूत्र है, कट नियम दिया गया है
@@ Line 37: / Line 39: @@
 <ol प्रारंभ=3><li><math>\Gamma, \Pi \vdash B</math></li></ol>
-अगर हम सोचें <math>B</math> एक प्रमेय के रूप में, तो इस मामले में कट-उन्मूलन केवल एक लेम्मा कहता है <math>A</math> इस प्रमेय को सिद्ध करने के लिए इनलाइन किया जा सकता है। जब भी प्रमेय के प्रमाण में [[लेम्मा (गणित)]] का उल्लेख होता है <math>A</math>, हम प्रमाण के स्थान पर घटनाओं को प्रतिस्थापित कर सकते हैं <math>A</math>. फलस्वरूप, कटौती नियम [[स्वीकार्य नियम]] है।
+यदि हम <math>B</math> को एक प्रमेय के रूप में विचार करते हैं, तो इस स्थिति में कट-एलिमिनेशन बस यह कहता है कि इस प्रमेय को सिद्ध करने के लिए उपयोग किया गया एक लेम्मा <math>A</math> इनलाइन किया जा सकता है। जब भी प्रमेय के प्रमाण में लेम्मा <math>A</math> का उल्लेख होता है, हम <math>A</math> के प्रमाण के लिए घटनाओं को प्रतिस्थापित कर सकते हैं। परिणाम स्वरुप, कट नियम स्वीकार्य है।
 ==प्रमेय के परिणाम==
-अनुक्रमिक कलन में तैयार की गई प्रणालियों के लिए, [[विश्लेषणात्मक प्रमाण]] वे प्रमाण हैं जो कट का उपयोग नहीं करते हैं। आमतौर पर ऐसा प्रमाण निश्चित रूप से लंबा होगा, और जरूरी नहीं कि यह तुच्छ हो। अपने निबंध डोंट एलिमिनेट कट में!<ref>{{harvnb|Boolos|1984|pp=373-378}}</ref> [[जॉर्ज बूलोस]] ने प्रदर्शित किया कि एक व्युत्पत्ति थी जिसे कट का उपयोग करके एक पृष्ठ में पूरा किया जा सकता था, लेकिन जिसका विश्लेषणात्मक प्रमाण ब्रह्मांड के जीवनकाल में पूरा नहीं किया जा सकता था।
+अनुक्रमिक कलन में तैयार की गई प्रणालियों के लिए, [[विश्लेषणात्मक प्रमाण]] वे प्रमाण हैं जो कट का उपयोग नहीं करते हैं। समान्यत: ऐसा प्रमाण निश्चित रूप से लंबा होगा, जिसमे और आवश्यक नहीं कि यह तुच्छ हो। अपने निबंध डोंट एलिमिनेट कट में!<ref>{{harvnb|Boolos|1984|pp=373-378}}</ref> [[जॉर्ज बूलोस]] ने प्रदर्शित किया कि एक व्युत्पत्ति थी जिसे कट का उपयोग करके एक पृष्ठ में पूर्ण किया जा सकता था, किंतु जिसका विश्लेषणात्मक प्रमाण ब्रह्मांड के जीवनकाल में पूर्ण नहीं किया जा सकता था।
-इस प्रमेय के कई, समृद्ध परिणाम हैं:
+इस प्रमेय के अनेक , समृद्ध परिणाम हैं:
-* एक प्रणाली निरंतरता प्रमाण है यदि वह बेतुके प्रमाण को स्वीकार करती है। यदि सिस्टम में कट उन्मूलन प्रमेय है, तो यदि उसके पास बेतुके, या खाली अनुक्रम का प्रमाण है, तो उसके पास बिना कटौती के, बेतुके (या खाली अनुक्रम) का प्रमाण भी होना चाहिए। आमतौर पर यह जांचना बहुत आसान है कि ऐसा कोई सबूत तो नहीं है। इस प्रकार, एक बार जब किसी सिस्टम में कट एलिमिनेशन प्रमेय दिखाया जाता है, तो यह आमतौर पर तत्काल होता है कि सिस्टम सुसंगत है।
+* एक प्रणाली निरंतरता प्रमाण है यदि वह निरर्थक प्रमाण को स्वीकार करती है। यदि प्रणाली में कट उन्मूलन प्रमेय है, तो यदि उसके समीप निरर्थक, या रिक्त अनुक्रम का प्रमाण है, तो उसके समीप बिना कट के, निरर्थक (या रिक्त अनुक्रम) का प्रमाण भी होना चाहिए। समान्यत यह जांचना अधिक सरल है कि ऐसा कोई प्रमाण तो नहीं है। इस प्रकार, पुनः जब किसी प्रणाली में कट एलिमिनेशन प्रमेय दिखाया जाता है, तो यह समान्यत तत्काल होता है कि प्रणाली सुसंगत है।
-* आम तौर पर सिस्टम में, कम से कम प्रथम क्रम तर्क में, उप-सूत्र संपत्ति, [[प्रमाण-सैद्धांतिक शब्दार्थ]] के कई दृष्टिकोणों में एक महत्वपूर्ण संपत्ति होती है।
+* सामान्यतः प्रणाली में, कम से कम प्रथम क्रम तर्क में, उप-सूत्र गुण, [[प्रमाण-सैद्धांतिक शब्दार्थ]] के अनेक दृष्टिकोणों में एक महत्वपूर्ण गुण होती है।
-[[ क्रेग प्रक्षेप ]] को साबित करने के लिए कट एलिमिनेशन सबसे शक्तिशाली उपकरणों में से एक है। प्रथम-क्रम रिज़ॉल्यूशन के आधार पर प्रमाण खोज करने की संभावना, [[प्रोलॉग]] प्रोग्रामिंग भाषा के लिए आवश्यक अंतर्दृष्टि, उपयुक्त प्रणाली में कट की स्वीकार्यता पर निर्भर करती है।
+[[ क्रेग प्रक्षेप | क्रेग प्रक्षेप]] को सिद्ध करने के लिए कट एलिमिनेशन अधिक शक्तिशाली उपकरणों में से एक है। प्रथम-क्रम रिज़ॉल्यूशन के आधार पर प्रमाण खोज करने की संभावना, [[प्रोलॉग]] प्रोग्रामिंग भाषा के लिए आवश्यक अंतर्दृष्टि, उपयुक्त प्रणाली में कट की स्वीकार्यता पर निर्भर करती है।
-करी-हावर्ड समरूपता के माध्यम से उच्च-क्रम टाइप किए गए लैम्ब्डा कैलकुलस पर आधारित प्रूफ सिस्टम के लिए, कट एलिमिनेशन एल्गोरिदम [[सामान्यीकरण संपत्ति (सार पुनर्लेखन)]] के अनुरूप होते हैं (प्रत्येक प्रूफ शब्द चरणों की एक सीमित संख्या में एक [[सामान्य रूप (शब्द पुनर्लेखन)]] में कम हो जाता है)।
+करी-हावर्ड समरूपता के माध्यम से उच्च-क्रम टाइप किए गए लैम्ब्डा कैलकुलस पर आधारित प्रूफ प्रणाली के लिए, कट एलिमिनेशन एल्गोरिदम [[सामान्यीकरण संपत्ति (सार पुनर्लेखन)|सामान्यीकरण गुण (सार पुनर्लेखन)]] के अनुरूप होते हैं (प्रत्येक प्रूफ शब्द चरणों की एक सीमित संख्या में एक [[सामान्य रूप (शब्द पुनर्लेखन)]] में कम हो जाता है)।
 == यह भी देखें ==
-* [[कटौती प्रमेय]]
+* [[कटौती प्रमेय|कट प्रमेय]]
-* पीनो के सिद्धांतों के लिए जेंटज़ेन की संगति प्रमाण
+* पीनो के सिद्धांतों के लिए जेंटज़ेन की स्थिरता का प्रमाण
 ==टिप्पणियाँ==
@@ Line 61: / Line 63: @@
 == संदर्भ ==
 * {{cite journal |first=Gerhard |last=Gentzen |author-link=Gerhard Gentzen |title=Untersuchungen über das logische Schließen. I. |journal=Mathematische Zeitschrift |volume=39 |pages=176–210 |year=1935 |doi=10.1007/BF01201353}}
-** [https://web.archive.org/web/20151224194624/http://gdz.sub.uni-goettingen.de/dms/load/img/?IDDOC=17178 Untersuchungen über das logische Schließen I]  (Archive.org)
+** [https://web.archive.org/web/20151224194624/http://gdz.sub.uni-goettingen.de/dms/load/img/?IDDOC=17178 Untersuchungen über das logische Schließen I] (Archive.org)
 ** {{cite journal | first=Gerhard | last=Gentzen | title=Investigations into logical deduction | journal=American Philosophical Quarterly | volume=1 | number=4 | pages=249–287 | year=1964}}
 * {{cite journal |first=Gerhard |last=Gentzen |author-link=Gerhard Gentzen |title=Untersuchungen über das logische Schließen. II. |journal=Mathematische Zeitschrift |volume=39 |pages=405–431 |year=1935 |doi=10.1007/BF01201363}}
@@ Line 79: / Line 81: @@
   |author-first1=A.G.
 }}
-[[Category: गणित की नींव में प्रमेय]] [[Category: प्रमाण सिद्धांत]]
-[[Category: Machine Translated Page]]
 [[Category:Created On 20/07/2023]]
+[[Category:Lua-based templates]]
+[[Category:Machine Translated Page]]
+[[Category:Pages with script errors]]
+[[Category:Short description with empty Wikidata description]]
+[[Category:Templates Vigyan Ready]]
+[[Category:Templates that add a tracking category]]
+[[Category:Templates that generate short descriptions]]
+[[Category:Templates using TemplateData]]
+[[Category:गणित की नींव में प्रमेय]]
+[[Category:प्रमाण सिद्धांत]]

Anonymous

Search

कट-उन्मूलन प्रमेय: Difference between revisions

Namespaces

More

Page actions

Latest revision as of 09:55, 4 August 2023

Contents

कट नियम

कट उन्मूलन

प्रमेय के परिणाम

यह भी देखें

टिप्पणियाँ

संदर्भ

बाहरी संबंध

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

कट-उन्मूलन प्रमेय: Difference between revisions

Latest revision as of 09:55, 4 August 2023

कट नियम

कट उन्मूलन

प्रमेय के परिणाम

यह भी देखें

टिप्पणियाँ

संदर्भ

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories