न्यूनतम तर्क: Difference between revisions
From Vigyanwiki
No edit summary |
No edit summary |
||
| Line 24: | Line 24: | ||
निषेध के साथ एक भाषा में एक प्राकृतिक कथन, जैसे कि न्यूनतम तर्क, उदाहरण के लिए, निषेध परिचय का सिद्धांत है । जिससे किसी कथन का निषेध इसे मानकर और एक विरोधाभास प्राप्त करके सिद्ध होता है। औपचारिक रूप से, इसे किन्हीं दो प्रस्तावों के रूप में व्यक्त किया जा सकता है । | निषेध के साथ एक भाषा में एक प्राकृतिक कथन, जैसे कि न्यूनतम तर्क, उदाहरण के लिए, निषेध परिचय का सिद्धांत है । जिससे किसी कथन का निषेध इसे मानकर और एक विरोधाभास प्राप्त करके सिद्ध होता है। औपचारिक रूप से, इसे किन्हीं दो प्रस्तावों के रूप में व्यक्त किया जा सकता है । | ||
:<math>(B\to (A\land \neg A))\to \neg B</math>. | :<math>(B\to (A\land \neg A))\to \neg B</math>. | ||
<math>B</math> कों विरोधाभास <math>A\land \neg A</math> के रूप में लिया | <math>B</math> कों विरोधाभास <math>A\land \neg A</math> के रूप में लिया स्वयं, यह गैर-विरोधाभास के नियम को स्थापित करता है । | ||
:<math>\neg(A\land \neg A)</math>. | :<math>\neg(A\land \neg A)</math>. | ||
| Line 36: | Line 36: | ||
=== असावधानी के माध्यम से स्वयंसिद्धीकरण === | === असावधानी के माध्यम से स्वयंसिद्धीकरण === | ||
सकारात्मक कलन को न्यूनतम तर्क तक विस्तारित करने की एक संभावित योजना उपचार करना है । <math>\neg B</math> एक निहितार्थ के रूप में, जिस स्थिति में एक तर्क के [[इम्प्लीकेशनल प्रोपोज़िशनल कैलकुलस]] से प्रमेय निषेधात्मक कथनों तक ले जाते हैं। इस कोने तक, <math>\bot</math> एक प्रस्ताव के रूप में प्रस्तुत किया जाता है । जब तक कि सिस्टम असंगत और नकारा न हो, तब तक सिद्ध नहीं किया जा सकता है । | सकारात्मक कलन को न्यूनतम तर्क तक विस्तारित करने की एक संभावित योजना उपचार करना है । <math>\neg B</math> एक निहितार्थ के रूप में, जिस स्थिति में एक तर्क के [[इम्प्लीकेशनल प्रोपोज़िशनल कैलकुलस]] से प्रमेय निषेधात्मक कथनों तक ले जाते हैं। इस कोने तक, <math>\bot</math> एक प्रस्ताव के रूप में प्रस्तुत किया जाता है । जब तक कि सिस्टम असंगत और नकारा न हो, तब तक सिद्ध नहीं किया जा सकता है । इसके बाद एक संक्षिप्त नाम <math>\neg B</math> के रूप में <math>B \to \bot</math> माना जाता है । | ||
रचनात्मक रूप से, <math>\bot</math> एक प्रस्ताव का प्रतिनिधित्व करता है । जिसके लिए विश्वास करने का कोई कारण नहीं हो सकता है। | रचनात्मक रूप से, <math>\bot</math> एक प्रस्ताव का प्रतिनिधित्व करता है । जिसके लिए विश्वास करने का कोई कारण नहीं हो सकता है। | ||
| Line 97: | Line 97: | ||
कोई भी <math>\land, \lor, \to</math> सूत्र केवल उपयोग कर रहा है । न्यूनतम तर्क में सिद्ध किया जा सकता है । यदि और केवल यदि यह अंतर्ज्ञानवादी तर्क में सिद्ध होता है। | कोई भी <math>\land, \lor, \to</math> सूत्र केवल उपयोग कर रहा है । न्यूनतम तर्क में सिद्ध किया जा सकता है । यदि और केवल यदि यह अंतर्ज्ञानवादी तर्क में सिद्ध होता है। | ||
विस्फोट का सिद्धांत अंतर्ज्ञानवादी तर्क में मान्य है और व्यक्त करता है कि किसी भी और सभी प्रस्तावों को प्राप्त करने के लिए, कोई भी | विस्फोट का सिद्धांत अंतर्ज्ञानवादी तर्क में मान्य है और व्यक्त करता है कि किसी भी और सभी प्रस्तावों को प्राप्त करने के लिए, कोई भी प्राप्त करके ऐसा कर सकता है। न्यूनतम तर्क में, यह सिद्धांत अक्षीयकरण रूप से इच्छानुसार प्रस्तावों के लिए नहीं है। जैसा कि न्यूनतम तर्क अंतर्ज्ञानवादी तर्क के केवल सकारात्मक अंश का प्रतिनिधित्व करता है । यह अंतर्ज्ञानवादी तर्क का एक उपतंत्र है और सख्ती से अशक्त है। | ||
संक्षेप में तैयार किया गया, अंतर्ज्ञानवादी तर्क में विस्फोट वास्तव में दोहरे निषेध उन्मूलन सिद्धांत के विशेष स्थितियों को अनुदान देता है । जो कि न्यूनतम तर्क के पास नहीं है। | संक्षेप में तैयार किया गया, अंतर्ज्ञानवादी तर्क में विस्फोट वास्तव में दोहरे निषेध उन्मूलन सिद्धांत के विशेष स्थितियों को अनुदान देता है । जो कि न्यूनतम तर्क के पास नहीं है। | ||
| Line 104: | Line 104: | ||
व्यावहारिक रूप से, अंतर्ज्ञानवादी संदर्भ में, विस्फोट का सिद्धांत वियोगात्मक न्यायवाक्य को सक्षम बनाता है । | व्यावहारिक रूप से, अंतर्ज्ञानवादी संदर्भ में, विस्फोट का सिद्धांत वियोगात्मक न्यायवाक्य को सक्षम बनाता है । | ||
:<math>((A \lor B)\land \neg A) \to B.</math> | :<math>((A \lor B)\land \neg A) \to B.</math> | ||
इसे इस प्रकार पढ़ा जा सकता है । जिसके रचनात्मक प्रमाण को देखते हुए <math>A \lor B</math> और रचनात्मक अस्वीकृति <math>A</math>, एक बिना शर्त के सकारात्मक स्थिति के विकल्प के लिए अनुमति देता है । <math>B</math>इस प्रकार, न्यायवाक्य वियोजन के लिए एक अनपैकिंग सिद्धांत है। इसे विस्फोट के औपचारिक परिणाम के रूप में देखा जा सकता है और इसका तात्पर्य भी है। ऐसा इसलिए है क्योंकि यदि <math>A \lor B</math> सिद्ध करके सिद्ध किया था । | इसे इस प्रकार पढ़ा जा सकता है । जिसके रचनात्मक प्रमाण को देखते हुए <math>A \lor B</math> और रचनात्मक अस्वीकृति <math>A</math>, एक बिना शर्त के सकारात्मक स्थिति के विकल्प के लिए अनुमति देता है । <math>B</math>इस प्रकार, न्यायवाक्य वियोजन के लिए एक अनपैकिंग सिद्धांत है। इसे विस्फोट के औपचारिक परिणाम के रूप में देखा जा सकता है और इसका तात्पर्य भी है। ऐसा इसलिए है क्योंकि यदि <math>A \lor B</math> सिद्ध करके सिद्ध किया था । तब <math>B</math> पहले से ही सिद्ध है, जबकि यदि <math>A \lor B</math> सिद्ध करके सिद्ध किया था । <math>A</math>, तब <math>B</math> यह भी अनुसरण करता है । क्योंकि अंतर्ज्ञानवादी सिस्टम विस्फोट की अनुमति देती है। | ||
उदाहरण के लिए, एक रचनात्मक तर्क दिया गया है कि एक सिक्के के पलटने का परिणाम या तो हेड या टेल होता है । (<math>A</math> या <math>B</math>), एक रचनात्मक तर्क के साथ कि परिणाम वास्तव में हेड्स नहीं था । न्यायवाक्य अभिव्यक्त करता है कि तब यह पहले से ही एक तर्क का गठन करता है । | उदाहरण के लिए, एक रचनात्मक तर्क दिया गया है कि एक सिक्के के पलटने का परिणाम या तो हेड या टेल होता है । (<math>A</math> या <math>B</math>), एक रचनात्मक तर्क के साथ कि परिणाम वास्तव में हेड्स नहीं था । न्यायवाक्य अभिव्यक्त करता है कि तब यह पहले से ही एक तर्क का गठन करता है । | ||
| Line 144: | Line 144: | ||
=== निषेध का प्रयोग === | === निषेध का प्रयोग === | ||
<math>\bot</math> न केवल [[प्राकृतिक कटौती|प्राकृतिक छय]] में प्रयोग किया जाता है । किन्तु करी-हावर्ड | <math>\bot</math> न केवल [[प्राकृतिक कटौती|प्राकृतिक छय]] में प्रयोग किया जाता है । किन्तु करी-हावर्ड के अनुसार सैद्धांतिक सूत्र में भी प्रयोग किया जाता है। | ||
टाइप सिस्टम में, <math>\bot</math> अधिकांशतः खाली प्रकार के रूप में भी प्रस्तुत किया जाता है। | टाइप सिस्टम में, <math>\bot</math> अधिकांशतः खाली प्रकार के रूप में भी प्रस्तुत किया जाता है। | ||
| Line 150: | Line 150: | ||
कई संदर्भों में, <math>\bot</math> तर्क में एक अलग स्थिरांक होने की आवश्यकता नहीं है । किन्तु इसकी भूमिका को किसी भी अस्वीकृत प्रस्ताव से बदला जा सकता है। उदाहरण के लिए, इसे परिभाषित किया जा सकता है । <math>a=b</math> जहाँ <math>a, b</math> विशिष्ट होना चाहिए। उस प्रस्ताव के लिए प्रमाण के अस्तित्व में न होने का प्रमाणित तब स्थिरता का प्रमाणित है। | कई संदर्भों में, <math>\bot</math> तर्क में एक अलग स्थिरांक होने की आवश्यकता नहीं है । किन्तु इसकी भूमिका को किसी भी अस्वीकृत प्रस्ताव से बदला जा सकता है। उदाहरण के लिए, इसे परिभाषित किया जा सकता है । <math>a=b</math> जहाँ <math>a, b</math> विशिष्ट होना चाहिए। उस प्रस्ताव के लिए प्रमाण के अस्तित्व में न होने का प्रमाणित तब स्थिरता का प्रमाणित है। | ||
एक उदाहरण लक्षण वर्णन <math>\bot</math> है । | एक उदाहरण लक्षण वर्णन <math>\bot</math> है । <math>0=1</math> एक सिद्धांत में प्राकृतिक संख्या सम्मिलित है। इसे सादे रचनात्मक तर्क के लिए भी अपनाया जा सकता है। | ||
इससे <math>3^4=8</math> सिद्ध होता है । अर्थात् <math>\neg(3^4=8)</math>, बस सिद्ध करने का कारण है । <math>(3^4=8)\to(0=1)</math>. हम नोटेशन प्रस्तुत कर सकते हैं । <math>3^4 \neq 8</math> प्रमाण पर कब्जा करने के लिए भी और वास्तव में, अंकगणित का प्रयोग करके, <math>\tfrac{3^4-8}{73}=1</math> रखता है, किन्तु <math>(3^4=8)</math> भी तात्पर्य है । <math>\tfrac{3^4-8}{73}=0</math>. तो इसका कारण होगा <math>1=0</math> और इसलिए <math>\neg(3^4=8)</math> हम प्राप्त करते हैं । | इससे <math>3^4=8</math> सिद्ध होता है । अर्थात् <math>\neg(3^4=8)</math>, बस सिद्ध करने का कारण है । <math>(3^4=8)\to(0=1)</math>. हम नोटेशन प्रस्तुत कर सकते हैं । <math>3^4 \neq 8</math> प्रमाण पर कब्जा करने के लिए भी और वास्तव में, अंकगणित का प्रयोग करके, <math>\tfrac{3^4-8}{73}=1</math> रखता है, किन्तु <math>(3^4=8)</math> भी तात्पर्य है । <math>\tfrac{3^4-8}{73}=0</math>. तो इसका कारण होगा <math>1=0</math> और इसलिए <math>\neg(3^4=8)</math> हम प्राप्त करते हैं । | ||
| Line 161: | Line 161: | ||
इसे निम्नलिखित अनुक्रमिक कलन नियमों द्वारा परिभाषित किया जा सकता है । | इसे निम्नलिखित अनुक्रमिक कलन नियमों द्वारा परिभाषित किया जा सकता है । | ||
:<math>\dfrac{}{\Gamma \cup \{A\} \vdash A} \mbox{ axiom}</math> | :<math>\dfrac{}{\Gamma \cup \{A\} \vdash A} \mbox{ axiom}</math> <math>\dfrac{\Gamma \cup \{A\} \vdash B}{\Gamma \vdash A \to B} \mbox{ intro}</math> <math>\dfrac{\Gamma \vdash A \to B ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ \Delta \vdash A}{\Gamma \cup \Delta \vdash B} \mbox{ elim.}</math><ref>{{cite book | author=M. Weber and M. Simons and C. Lafontaine | publisher=Springer | series=LNCS | title=The Generic Development Language DEVA: Presentation and Case Studies | volume=738 | pages=246 | year=1993 }} Here: p.36-40.</ref><ref>{{cite book | url=http://yquem.inria.fr/~huet/PUBLIC/Formal_Structures.ps.gz | archive-url=https://web.archive.org/web/20140714171331/http://yquem.inria.fr/~huet/PUBLIC/Formal_Structures.ps.gz | url-status=dead | archive-date=2014-07-14 | author=Gérard Huet | title=संगणना और कटौती के लिए औपचारिक संरचनाएं| location=Marktoberdorf | series=International Summer School on Logic of Programming and Calculi of Discrete Design | date=May 1986 }} Here: p.125, p.132</ref> | ||
इस प्रतिबंधित न्यूनतम तर्क का प्रत्येक सूत्र सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस में एक प्रकार से मेल खाता है । देखें करी-हावर्ड | इस प्रतिबंधित न्यूनतम तर्क का प्रत्येक सूत्र सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस में एक प्रकार से मेल खाता है । देखें करी-हावर्ड प्राकृतिक छय और लैम्ब्डा कैलकुलस करी-हावर्ड उस संदर्भ में, न्यूनतम तर्क वाक्यांश का उपयोग कभी-कभी न्यूनतम तर्क के इस प्रतिबंध के अर्थ में किया जाता है।<ref>{{Cite web |last=Sørensen |first=Morten Heine B. |last2=Urzyczyn |first2=Pawel |date=May 1998 |title=करी-हावर्ड समरूपतावाद पर व्याख्यान|url=https://disi.unitn.it/%7Ebernardi/RSISE11/Papers/curry-howard.pdf}}</ref> मिनिमल लॉजिक का यह इम्प्लीकेशनल फ्रैगमेंट हिल्बर्ट सिस्टम्स की सूची के समान है । पॉजिटिव, इंप्लीकेशनल फ्रैगमेंट ऑफ इंट्यूशनिस्टिक लॉजिक चूंकि न्यूनतम लॉजिक पहले से ही इंट्यूशनिस्टिक लॉजिक का पॉजिटिव फ्रैगमेंट है। | ||
== शब्दार्थ == | == शब्दार्थ == | ||
Revision as of 17:22, 24 May 2023
न्यूनतम तर्क, या न्यूनतम कलन, एक गणितीय तर्क सिस्टम है । जिसे मूल रूप से इंजीब्रिट जोहानसन द्वारा विकसित किया गया था।[1] यह एक अंतर्ज्ञानवादी तर्क और परासंगत तर्क है । जो बहिष्कृत मध्य के नियम के साथ-साथ विस्फोट के सिद्धांत (पूर्व मिथ्या क्वाडलिबेट) दोनों को अस्वीकार करता है, और इसलिए निम्नलिखित दो व्युत्पत्तियों में से कोई भी मान्य नहीं है ।
जहाँ और कोई प्रस्ताव हैं। अधिकांश रचनात्मक तर्क केवल पूर्व को अस्वीकार करते हैं । अपवर्जित मध्य का नियम मौलिक तर्कशास्त्र में, भूतपूर्व नियम भी गलत होते हैं ।
- साथ ही साथ उनके वेरिएंट और स्विच्ड, एक दूसरे के समतुल्य और मान्य हैं। मिनिमल लॉजिक भी उन सिद्धांतों को खारिज करता है।
अक्षीयकरण
मिनिमल लॉजिक को अंतर्ज्ञानवादी तर्क के हिल्बर्ट प्रणालियों की सूची सकारात्मक प्रस्तावपरक कलन पर अक्षीयकरण किया गया है। इन दोनों लॉजिक्स को समान अक्षीयकरण उपयोग करके भाषा में तैयार किया जा सकता है ।
तार्किक निहितार्थ तार्किक संयोजन और तार्किक विच्छेदन मूलभूत तार्किक संयोजक के रूप में, किन्तु न्यूनतम तर्क जोड़ता है ।
असत्य भाषा के भाग के रूप में वैकल्पिक रूप से, निषेध के प्रत्यक्ष अभिगृहीतों की चर्चा नीचे की गई है।
प्रमेय
यहां केवल ऐसे प्रमेय सम्मिलित हैं । जो धनात्मक कलन में पहले से ही सिद्ध नहीं किए जा सकते हैं।
निषेध परिचय
निहितार्थ और निषेध नियमो का एक त्वरित विश्लेषण इस बात का एक अच्छा संकेत देता है कि यह तर्क, जिसमें पूर्ण विस्फोट की कमी है । क्या सिद्ध कर सकता है ।
निषेध के साथ एक भाषा में एक प्राकृतिक कथन, जैसे कि न्यूनतम तर्क, उदाहरण के लिए, निषेध परिचय का सिद्धांत है । जिससे किसी कथन का निषेध इसे मानकर और एक विरोधाभास प्राप्त करके सिद्ध होता है। औपचारिक रूप से, इसे किन्हीं दो प्रस्तावों के रूप में व्यक्त किया जा सकता है ।
- .
कों विरोधाभास के रूप में लिया स्वयं, यह गैर-विरोधाभास के नियम को स्थापित करता है ।
- .
किसी भी को मानते हुए, मटेरियल कंडिशनल का परिचय नियम देता है, वह भी तब जब और प्रासंगिकता तर्क रूप से संबंधित नहीं हैं। इसके साथ और निहितार्थ उन्मूलन, उपरोक्त परिचय सिद्धांत का तात्पर्य है ।
- ,
अर्थात किसी भी विरोधाभास को मानते हुए, प्रत्येक प्रस्ताव को नकारा जा सकता है। न्यूनतम तर्क में निषेध का परिचय संभव है । इसलिए यहाँ एक विरोधाभास भी प्रत्येक दोहरे निषेध को सिद्ध करता है । विस्फोट बाद के दोहरे निषेध को दूर करने की अनुमति देगा, किन्तु यह सिद्धांत नहीं अपनाया गया है।
इसके अलावा, उपरोक्त का उपयोग करना