न्यूनतम तर्क: 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>B \to \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>B</math> पहले से ही सिद्ध है, जबकि यदि <math>A \lor B</math> सिद्ध करके सिद्ध किया था । <math>A</math>, तब <math>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>0=1</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 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>
:<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> मिनिमल लॉजिक का यह इम्प्लीकेशनल फ्रैगमेंट हिल्बर्ट सिस्टम्स की सूची के समान है । पॉजिटिव, इंप्लीकेशनल फ्रैगमेंट ऑफ इंट्यूशनिस्टिक लॉजिक चूंकि न्यूनतम लॉजिक पहले से ही इंट्यूशनिस्टिक लॉजिक का पॉजिटिव फ्रैगमेंट है।
इस प्रतिबंधित न्यूनतम तर्क का प्रत्येक सूत्र सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस में एक प्रकार से मेल खाता है । देखें करी-हावर्ड प्राकृतिक छय और लैम्ब्डा कैलकुलस करी-हावर्ड उस संदर्भ में, न्यूनतम तर्क वाक्यांश का उपयोग कभी-कभी न्यूनतम तर्क के इस प्रतिबंध के अर्थ में किया जाता है।<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] यह एक अंतर्ज्ञानवादी तर्क और परासंगत तर्क है । जो बहिष्कृत मध्य के नियम के साथ-साथ विस्फोट के सिद्धांत (पूर्व मिथ्या क्वाडलिबेट) दोनों को अस्वीकार करता है, और इसलिए निम्नलिखित दो व्युत्पत्तियों में से कोई भी मान्य नहीं है ।

जहाँ और कोई प्रस्ताव हैं। अधिकांश रचनात्मक तर्क केवल पूर्व को अस्वीकार करते हैं । अपवर्जित मध्य का नियम मौलिक तर्कशास्त्र में, भूतपूर्व नियम भी गलत होते हैं ।

साथ ही साथ उनके वेरिएंट और स्विच्ड, एक दूसरे के समतुल्य और मान्य हैं। मिनिमल लॉजिक भी उन सिद्धांतों को खारिज करता है।

अक्षीयकरण

मिनिमल लॉजिक को अंतर्ज्ञानवादी तर्क के हिल्बर्ट प्रणालियों की सूची सकारात्मक प्रस्तावपरक कलन पर अक्षीयकरण किया गया है। इन दोनों लॉजिक्स को समान अक्षीयकरण उपयोग करके भाषा में तैयार किया जा सकता है ।

तार्किक निहितार्थ तार्किक संयोजन और तार्किक विच्छेदन मूलभूत तार्किक संयोजक के रूप में, किन्तु न्यूनतम तर्क जोड़ता है ।

असत्य भाषा के भाग के रूप में वैकल्पिक रूप से, निषेध के प्रत्यक्ष अभिगृहीतों की चर्चा नीचे की गई है।

प्रमेय

यहां केवल ऐसे प्रमेय सम्मिलित हैं । जो धनात्मक कलन में पहले से ही सिद्ध नहीं किए जा सकते हैं।

निषेध परिचय

निहितार्थ और निषेध नियमो का एक त्वरित विश्लेषण इस बात का एक अच्छा संकेत देता है कि यह तर्क, जिसमें पूर्ण विस्फोट की कमी है । क्या सिद्ध कर सकता है ।

निषेध के साथ एक भाषा में एक प्राकृतिक कथन, जैसे कि न्यूनतम तर्क, उदाहरण के लिए, निषेध परिचय का सिद्धांत है । जिससे किसी कथन का निषेध इसे मानकर और एक विरोधाभास प्राप्त करके सिद्ध होता है। औपचारिक रूप से, इसे किन्हीं दो प्रस्तावों के रूप में व्यक्त किया जा सकता है ।

.

कों विरोधाभास के रूप में लिया स्वयं, यह गैर-विरोधाभास के नियम को स्थापित करता है ।

.

किसी भी को मानते हुए, मटेरियल कंडिशनल का परिचय नियम देता है, वह भी तब जब और प्रासंगिकता तर्क रूप से संबंधित नहीं हैं। इसके साथ और निहितार्थ उन्मूलन, उपरोक्त परिचय सिद्धांत का तात्पर्य है ।

,

अर्थात किसी भी विरोधाभास को मानते हुए, प्रत्येक प्रस्ताव को नकारा जा सकता है। न्यूनतम तर्क में निषेध का परिचय संभव है । इसलिए यहाँ एक विरोधाभास भी प्रत्येक दोहरे निषेध को सिद्ध करता है । विस्फोट बाद के दोहरे निषेध को दूर करने की अनुमति देगा, किन्तु यह सिद्धांत नहीं अपनाया गया है।

इसके अलावा, उपरोक्त का उपयोग करना

.

इसकी तुलना पूर्ण वियोजन न्यायवाक्य से की जानी है।

असावधानी के माध्यम से स्वयंसिद्धीकरण

सकारात्मक कलन को न्यूनतम तर्क तक विस्तारित करने की एक संभावित योजना उपचार करना है । एक निहितार्थ के रूप में, जिस स्थिति में एक तर्क के इम्प्लीकेशनल प्रोपोज़िशनल कैलकुलस से प्रमेय निषेधात्मक कथनों तक ले जाते हैं। इस कोने तक, एक प्रस्ताव के रूप में प्रस्तुत किया जाता है । जब तक कि सिस्टम असंगत और नकारा न हो, तब तक सिद्ध नहीं किया जा सकता है । इसके बाद एक संक्षिप्त नाम के रूप में माना जाता है ।

रचनात्मक रूप से, एक प्रस्ताव का प्रतिनिधित्व करता है । जिसके लिए विश्वास करने का कोई कारण नहीं हो सकता है।

पहले से ही चर्चा किए गए सिद्धांत सकारात्मक खंड पर प्रमेय से हो सकते हैं।

निषेध परिचय, पिछले अनुभाग में लिखा गया है । केवल एक विशेष स्थिति के रूप में निहित है ।

कब . इस तरह, न्यूनतम तर्क को नकारात्मक उन्मूलन (उर्फ विस्फोट) के बिना एक रचनात्मक तर्क के रूप में वर्णित किया जा सकता है।

उपरोक्त कैन को निष्कर्ष के नियम के रूप के माध्यम से सिद्ध किया जा सकता है । जिसे एक प्रस्ताव के रूप में पढ़ा जाता है ।

और वास्तव में उपरोक्त का एक विशेष स्थिति है । जब क्या सच है। जिसके माध्यम से निषेध की परिभाषा के साथ , मोडस पोनेन्स कथन स्वयं उसी तरह से फिर से विशिष्ट हो सकता है, और फिर गैर-विरोधाभास सिद्धांत स्थापित करता है । जो पहले से ही ऊपर वर्णित है। कढ़ी तुल्यता सहित सभी सामान्य अंतर्ज्ञानात्मक तर्क ऑपरेटरों की गैर-अंतर-परिभाषा योग्यता प्राप्त की जा सकती है। एक उदाहरण के लिए, यह महत्वपूर्ण तुल्यता पर बल देने योग्य है ।

,

यह व्यक्त करते हुए कि दोनों कहने के दो समान विधि और , हैं । सबसे पहले, डी मॉर्गन के दो परिचित नियम प्राप्त होते हैं ।

.

तीसरा मान्य डी मॉर्गन नियम भी व्युत्पन्न किया जा सकता है।

दूसरे, साथ जैसा ऊपर, यह इस प्रकार है ।

और यह बहिष्कृत मध्य के दोहरे निषेध को कम करता है ।

निहितार्थ परिचय द्वारा,

इसका तात्पर्य भी है । सीधे दिखा रहा है कि कैसे मानते हैं । न्यूनतम तर्क में सभी निषेधों को सिद्ध करता है। यह ऊपर भी बताया गया है । किन्तु यहाँ इसे छोटा किया जा सकता है ।

यदि असावधानी प्राचीन है तो पूर्ण विस्फोट को भी कहा जा सकता है ।

अधिक सिद्धांतों के माध्यम से स्वयंसिद्धीकरण

इस प्रकार

इसलिए

और

निषेध परिचय सिद्धांत से संबंधित, से

.

न्यूनतम तर्क विरोधाभास सिद्ध करता है ।

उपरोक्त सिद्धांतों को संयोजन में सकारात्मक कलन से प्रमेयों का उपयोग करके भी प्राप्त किया गया है ।

उपरोक्त दोहरे निषेध सिद्धांत को अपनाने के साथ-साथ गर्भनिरोधक सिद्धांत के साथ अंतर्ज्ञानवादी तर्क के सकारात्मक अंश पर न्यूनतम तर्क का एक वैकल्पिक स्वयंसिद्धता प्रदान करता है।

अप्रमाणिक वाक्य

सामान्यीकरण की युक्ति को दोहरे निषेधों से जुड़े सभी मौलिक रूप से मान्य कथनों को सिद्ध करने के लिए काम नहीं करता है। ध्यान दें कि वाक्य रचनात्मक आकार का कोई भी स्कीमा सिद्ध करने के लिए बहुत शक्तिशाली है । यदि यह सिद्ध करने योग्य था, तो कोई सच्चा प्रस्ताव कोई अन्य प्रस्ताव सिद्ध करेगा । अब यहाँ रुचि का एक प्रकार है जहाँ द्वारा प्रतिस्थापित किया जाए . यह दिखाता है, संभवतः आश्चर्यजनक रूप से, कि दोहरे निषेध का भोला सामान्यीकरण इस प्रकार सिद्ध नहीं किया जा सकता है।

न्यूनतम तर्क का प्रमेय है, जैसा है . इसलिए, पूर्ण दोहरे निषेध सिद्धांत को अपनाना न्यूनतम तर्क में कलन को मौलिक तर्क में वापस लाता है । साथ ही सभी मध्यवर्ती तर्क को छोड़ देता है।

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

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

अंतर्ज्ञानवादी रूप से भी मान्य नहीं है और न ही है ।
.

दोहरे-निषेध अनुवाद परिणामों से परे, यह गैर-मौलिक सिद्धांतों की अनुमति देता है।

अंतर्ज्ञानवादी तर्क से संबंध

कोई भी सूत्र केवल उपयोग कर रहा है । न्यूनतम तर्क में सिद्ध किया जा सकता है । यदि और केवल यदि यह अंतर्ज्ञानवादी तर्क में सिद्ध होता है।

विस्फोट का सिद्धांत अंतर्ज्ञानवादी तर्क में मान्य है और व्यक्त करता है कि किसी भी और सभी प्रस्तावों को प्राप्त करने के लिए, कोई भी प्राप्त करके ऐसा कर सकता है। न्यूनतम तर्क में, यह सिद्धांत अक्षीयकरण रूप से इच्छानुसार प्रस्तावों के लिए नहीं है। जैसा कि न्यूनतम तर्क अंतर्ज्ञानवादी तर्क के केवल सकारात्मक अंश का प्रतिनिधित्व करता है । यह अंतर्ज्ञानवादी तर्क का एक उपतंत्र है और सख्ती से अशक्त है।

संक्षेप में तैयार किया गया, अंतर्ज्ञानवादी तर्क में विस्फोट वास्तव में दोहरे निषेध उन्मूलन सिद्धांत के विशेष स्थितियों को अनुदान देता है । जो कि न्यूनतम तर्क के पास नहीं है।

वियोगात्मक न्यायवाक्य

व्यावहारिक रूप से, अंतर्ज्ञानवादी संदर्भ में, विस्फोट का सिद्धांत वियोगात्मक न्यायवाक्य को सक्षम बनाता है ।

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

उदाहरण के लिए, एक रचनात्मक तर्क दिया गया है कि एक सिक्के के पलटने का परिणाम या तो हेड या टेल होता है । ( या ), एक रचनात्मक तर्क के साथ कि परिणाम वास्तव में हेड्स नहीं था । न्यायवाक्य अभिव्यक्त करता है कि तब यह पहले से ही एक तर्क का गठन करता है ।

यदि अंतर्ज्ञानवादी तर्क सिस्टम को मेटालॉजिकल रूप से सुसंगत माना जाता है, तो न्यायवाक्य को यह कहते हुए पढ़ा जा सकता है कि एक रचनात्मक प्रदर्शन और , प्रदर्शन करने वाले अन्य गैर-तार्किक अक्षीयकरण के अभाव में , वास्तव में का एक प्रदर्शन सम्मिलित है ।

न्यूनतम तर्क में, कोई इसका प्रमाण प्राप्त नहीं कर सकता है । इस प्रकार से चूँकि, एक ही आधार का तात्पर्य दोहरे-नकारात्मक से है । , अर्थात . यदि न्यूनतम तर्क सिस्टम को मेटालॉजिकल रूप से सुसंगत माना जाता है, तो उस निहितार्थ सूत्र को यह कहकर व्यक्त किया जा सकता है । केवल अस्वीकार नहीं किया जा सकता है।

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

.

चूंकि पदार्थ सशर्त अनुदान सिद्ध प्रस्तावों के लिए डबल-निषेध उन्मूलन प्रदान करता है । यह फिर से अस्वीकृत प्रस्तावों के लिए डबल-निषेध उन्मूलन के समान है।

सिद्धांत में उपयोग का अंतर्ज्ञानवादी उदाहरण

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

माना कोई भी परिमाणक-मुक्त विधेय हो, और इस प्रकार सभी संख्याओं के लिए निर्णायक हो , जिससे बहिष्कृत मध्य धारण करे ।

.

फिर इंडक्शन द्वारा ,

शब्दों में: संख्याओं के लिए तक सीमित दायरे में , यदि इस बात से इंकार किया जा सकता है कि कोई स्थिति मान्य नहीं है, अर्थात यदि यह खारिज किया जा सकता है कि प्रत्येक संख्या के लिए, मान लीजिए , संगत प्रस्ताव सदैव अस्वीकार्य रहेगा, तो इसका तात्पर्य है कि कुछ है उनके बीच जिसके लिए है साध्य है।

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

यदि प्रस्ताव को प्रारंभ के रूप में तैयार किया गया है , तो यह प्रारंभिक स्थिति पहले से ही एक रिक्त खंड से विस्फोट का रूप देता है ।

.

अगला स्थिति एक निर्णायक विधेय के लिए दोहरा निषेध उन्मूलन बताता है ।

. h> स्थिति पढ़ता है
,

जो, जैसा कि पहले ही उल्लेख किया गया है, जिसके समान है ।

.

दोनों और एक निर्णायक विधेय के लिए फिर से दोहरे निषेध उन्मूलन के स्थिति हैं।

एक कथन निश्चित के लिए और न्यूनतम तर्क के सिद्धांतों का उपयोग करके, अन्य माध्यमों से सिद्ध किया जा सकता है।

एक तरफ के रूप में, सामान्य निर्णायक पूर्वानुमानो के लिए असीमित स्कीमा भी अंतर्ज्ञानवादी रूप से सिद्ध नहीं है । मार्कोव के सिद्धांत को देखें।

टाइप सिद्धांत से संबंध

निषेध का प्रयोग

न केवल प्राकृतिक छय में प्रयोग किया जाता है । किन्तु करी-हावर्ड के अनुसार सैद्धांतिक सूत्र में भी प्रयोग किया जाता है।

टाइप सिस्टम में, अधिकांशतः खाली प्रकार के रूप में भी प्रस्तुत किया जाता है।

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

एक उदाहरण लक्षण वर्णन है । एक सिद्धांत में प्राकृतिक संख्या सम्मिलित है। इसे सादे रचनात्मक तर्क के लिए भी अपनाया जा सकता है।

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

सरल प्रकार

कार्यात्मक प्रोग्रामिंग गणना पहले से ही मुख्य रूप से निहितार्थ संयोजी पर निर्भर करती है । उदाहरण के लिए देखें एक विधेय तर्क रुपरेखा के लिए निर्माण की गणना होती है ।

इस खंड में हम न्यूनतम तर्क को केवल निहितार्थ तक सीमित करके प्राप्त सिस्टम का उल्लेख करते हैं, और औपचारिक रूप से इसका वर्णन करते हैं।

इसे निम्नलिखित अनुक्रमिक कलन नियमों द्वारा परिभाषित किया जा सकता है ।

[2][3]

इस प्रतिबंधित न्यूनतम तर्क का प्रत्येक सूत्र सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस में एक प्रकार से मेल खाता है । देखें करी-हावर्ड प्राकृतिक छय और लैम्ब्डा कैलकुलस करी-हावर्ड उस संदर्भ में, न्यूनतम तर्क वाक्यांश का उपयोग कभी-कभी न्यूनतम तर्क के इस प्रतिबंध के अर्थ में किया जाता है।[4] मिनिमल लॉजिक का यह इम्प्लीकेशनल फ्रैगमेंट हिल्बर्ट सिस्टम्स की सूची के समान है । पॉजिटिव, इंप्लीकेशनल फ्रैगमेंट ऑफ इंट्यूशनिस्टिक लॉजिक चूंकि न्यूनतम लॉजिक पहले से ही इंट्यूशनिस्टिक लॉजिक का पॉजिटिव फ्रैगमेंट है।

शब्दार्थ

न्यूनतम तर्क के शब्दार्थ हैं । जो अंतर्ज्ञानवादी तर्क के फ्रेम-अर्थशास्त्र को प्रतिबिंबित करते हैं । पैराकंसिस्टेंट तर्क में शब्दार्थ की चर्चा देखें। यहां प्रस्तावों के लिए सत्यता और असत्यता निर्दिष्ट करने वाले मूल्यांकन कार्य कम बाधाओं के अधीन हो सकते हैं।

यह भी देखें

संदर्भ

  1. Ingebrigt Johansson (1937). "Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus". Compositio Mathematica (in Deutsch). 4: 119–136.
  2. M. Weber and M. Simons and C. Lafontaine (1993). The Generic Development Language DEVA: Presentation and Case Studies. LNCS. Vol. 738. Springer. p. 246. Here: p.36-40.
  3. Gérard Huet (May 1986). संगणना और कटौती के लिए औपचारिक संरचनाएं. International Summer School on Logic of Programming and Calculi of Discrete Design. Marktoberdorf. Archived from the original on 2014-07-14.{{cite book}}: CS1 maint: location missing publisher (link) Here: p.125, p.132
  4. Sørensen, Morten Heine B.; Urzyczyn, Pawel (May 1998). "करी-हावर्ड समरूपतावाद पर व्याख्यान" (PDF).
  • A.S. Troelstra and H. Schwichtenberg, 2000, Basic Proof Theory, Cambridge University Press, ISBN 0521779111