अंतर्ज्ञानवादी तर्क

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

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

गणितीय रचनावाद

शास्त्रीय तर्कशास्त्र के शब्दार्थ में, प्रस्तावनात्मक सूत्रों को दो-तत्व सेट से सत्य मान दिए जाते हैं $\{\top ,\bot \}$ (क्रमशः सत्य और असत्य), भले ही हमारे पास किसी भी मामले के लिए प्रत्यक्ष साक्ष्य हों या नहीं। इसे 'बहिष्कृत मध्य का नियम' कहा जाता है, क्योंकि यह 'सत्य' या 'असत्य' के अलावा किसी भी सत्य मूल्य की संभावना को बाहर करता है। इसके विपरीत, अंतर्ज्ञानवादी तर्क में प्रस्तावनात्मक सूत्रों को एक निश्चित सत्य मान नहीं दिया जाता है और केवल तभी सत्य माना जाता है जब हमारे पास प्रत्यक्ष प्रमाण होते हैं, इसलिए प्रमाण। (हम यह भी कह सकते हैं, प्रत्यक्ष प्रमाण के कारण प्रस्तावात्मक सूत्र के सत्य होने के बजाय, यह करी-हावर्ड पत्राचार | करी-हावर्ड अर्थ में एक प्रमाण द्वारा बसा हुआ है।) अंतर्ज्ञानवादी तर्क में संचालन इसलिए औचित्य के सिद्धांत को संरक्षित करता है, साथ में सत्य-मूल्यांकन के बजाय साक्ष्य और सिद्धता के संबंध में।

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

सिंटेक्स

रिगर-निशिमुरा जाली। इसके नोड अंतर्ज्ञानवादी तार्किक निहितार्थ द्वारा आदेशित अंतर्ज्ञानवादी तार्किक समकक्षता तक एक चर में प्रस्तावात्मक सूत्र हैं।

अंतर्ज्ञानवादी तर्क के सूत्रों का वाक्य-विन्यास प्रस्तावात्मक तर्क या प्रथम-क्रम तर्क के समान है। हालाँकि, अंतर्ज्ञानवादी तार्किक संयोजक शास्त्रीय तर्कशास्त्र की तरह एक दूसरे के संदर्भ में निश्चित नहीं हैं, इसलिए उनकी पसंद मायने रखती है। इंट्यूशनिस्टिक प्रोपोज़िशनल लॉजिक (आईपीएल) में यह →, ∧, ∨, ⊥ को बुनियादी संयोजकों के रूप में उपयोग करने के लिए प्रथागत है, ¬A को एक संक्षिप्त नाम के रूप में माना जाता है। (A → ⊥). अंतर्ज्ञानवादी प्रथम-क्रम तर्क में परिमाणक (तर्क) तर्क) दोनों ∃, ∀ की आवश्यकता होती है।

शास्त्रीय तर्क से कमजोर

अंतर्ज्ञानवादी तर्क को शास्त्रीय तर्क के कमजोर होने के रूप में समझा जा सकता है, जिसका अर्थ यह है कि यह एक तर्कसंगत अनुमान लगाने की अनुमति देता है, जबकि शास्त्रीय तर्क के तहत नहीं किए जा सकने वाले किसी भी नए संदर्भ की अनुमति नहीं देता है। अंतर्ज्ञानवादी तर्क का प्रत्येक प्रमेय शास्त्रीय तर्क में एक प्रमेय है, लेकिन इसके विपरीत नहीं। क्लासिकल लॉजिक में कई टॉटोलॉजी (तर्क) इंट्यूशनिस्टिक लॉजिक में प्रमेय नहीं हैं – विशेष रूप से, जैसा कि ऊपर कहा गया है, अंतर्ज्ञानवादी तर्क के मुख्य उद्देश्यों में से एक बहिष्कृत मध्य के कानून की पुष्टि नहीं करना है, ताकि विरोधाभास द्वारा गैर-रचनात्मक प्रमाण के उपयोग को समाप्त किया जा सके, जिसका उपयोग स्पष्ट उदाहरणों के बिना अस्तित्व के दावों को प्रस्तुत करने के लिए किया जा सकता है। जिन वस्तुओं से यह साबित होता है कि वे मौजूद हैं। हम कहते हैं कि पुष्टि नहीं करते हैं क्योंकि यह जरूरी नहीं है कि कानून किसी भी संदर्भ में कायम है, कोई प्रति-उदाहरण नहीं दिया जा सकता है: इस तरह के एक प्रति-उदाहरण एक अनुमान होगा (एक निश्चित प्रस्ताव के लिए कानून की उपेक्षा) शास्त्रीय तर्क के तहत अस्वीकृत और इस प्रकार अंतर्ज्ञानवादी तर्क जैसे सख्त कमजोर पड़ने की अनुमति नहीं है। वास्तव में, कानून के दोहरे निषेध को प्रणाली के पुनरावलोकन के रूप में बरकरार रखा गया है: अर्थात, यह एक प्रमेय है जो $\neg {\big (}\neg (P\vee \neg P){\big )}$ प्रस्ताव की परवाह किए बिना $P$. तो प्रस्तावपरक कलन हमेशा शास्त्रीय तर्क के अनुकूल होता है। विधेय तर्क सूत्रों के लिए स्थिति अधिक जटिल होती है जब परिमाणित भावों को नकारा जाता है।

गणना का पालन करें

Main article: Sequent calculus

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

एलके के अन्य डेरिवेटिव अंतर्ज्ञानवादी व्युत्पन्न तक सीमित हैं लेकिन फिर भी एक अनुक्रम में कई निष्कर्ष निकालने की अनुमति देते हैं। एलजे' एक उदाहरण है।

हिल्बर्ट-शैली कलन

निम्नलिखित हिल्बर्ट-शैली की कटौती प्रणाली का उपयोग करके अंतर्ज्ञानवादी तर्क को परिभाषित किया जा सकता है। हिल्बर्ट-शैली कैलकुलस। यह प्रोपोज़िशनल कैलकुलस#ऑल्टरनेटिव कैलकुलस ऑफ़ एक्सिओमेटाइज़िंग क्लासिकल प्रोपोज़िशनल लॉजिक के समान है।

प्रस्तावपरक तर्क में, अनुमान नियम मूड सेट करना है

• एमपी : से $\phi$ और $\phi \to \psi$ तर्क करना $\psi$

और स्वयंसिद्ध हैं

• तब-1: $\phi \to (\chi \to \phi )$
• तब-2: $(\phi \to (\chi \to \psi ))\to ((\phi \to \chi )\to (\phi \to \psi ))$
• और 1: $\phi \land \chi \to \phi$
• और -2: $\phi \land \chi \to \chi$
• और-3: $\phi \to (\chi \to (\phi \land \chi ))$
• या -1: $\phi \to \phi \lor \chi$
• या -2: $\chi \to \phi \lor \chi$
• या -3: $(\phi \to \psi )\to ((\chi \to \psi )\to ((\phi \lor \chi )\to \psi ))$
• गलत: $\bot \to \phi$

इसे प्रथम-क्रम विधेय तर्क की प्रणाली बनाने के लिए, सामान्यीकरण (तर्क)

• $\forall$-जनरल: से $\psi \to \phi$ तर्क करना $\psi \to (\forall x\ \phi )$, यदि $x$ में मुक्त नहीं है $\psi$
• $\exists$-जनरल: से $\phi \to \psi$ तर्क करना $(\exists x\ \phi )\to \psi$, यदि $x$ में मुक्त नहीं है $\psi$

अभिगृहीतों के साथ जोड़े जाते हैं

• पीआरईडी-1: $(\forall x\ \phi (x))\to \phi (t)$, यदि शब्द $t$ चर के प्रतिस्थापन के लिए स्वतंत्र है $x$ में $\phi$ (यानी, यदि किसी चर की कोई घटना नहीं है $t$ में बंध जाता है $\phi (t)$)
• प्री-2: $\phi (t)\to (\exists x\ \phi (x))$, PRED-1 के समान प्रतिबंध के साथ

वैकल्पिक संयोजक

निषेध

यदि कोई संयोजक शामिल करना चाहता है $\lnot$ इसके संक्षिप्त रूप पर विचार करने के बजाय निषेध के लिए $\phi \to \bot$, यह जोड़ने के लिए पर्याप्त है:

• नहीं-1': $(\phi \to \bot )\to \lnot \phi$
• नहीं-2': $\lnot \phi \to (\phi \to \bot )$

यदि कोई संयोजक को छोड़ना चाहता है तो कई विकल्प उपलब्ध हैं $\bot$ (गलत)। उदाहरण के लिए, तीन सूक्तियों FALSE, NOT-1', और NOT-2' को दो अभिगृहीतों से प्रतिस्थापित किया जा सकता है

• नहीं-1: $(\phi \to \chi )\to ((\phi \to \lnot \chi )\to \lnot \phi )$
• नहीं-2: $\phi \to (\lnot \phi \to \chi )$

पर जैसा Propositional calculus § Axioms. NOT-1 के विकल्प हैं $(\phi \to \lnot \chi )\to (\chi \to \lnot \phi )$ या $(\phi \to \lnot \phi )\to \lnot \phi$.

समानता

संयोजक $\leftrightarrow$ तुल्यता के लिए एक संक्षिप्त नाम के साथ, के रूप में माना जा सकता है $\phi \leftrightarrow \chi$ के पक्ष में होना $(\phi \to \chi )\land (\chi \to \phi )$. वैकल्पिक रूप से, कोई अभिगृहीत जोड़ सकता है

• आईएफएफ-1: $(\phi \leftrightarrow \chi )\to (\phi \to \chi )$
• आईएफएफ-2: $(\phi \leftrightarrow \chi )\to (\chi \to \phi )$
• आईएफएफ-3: $(\phi \to \chi )\to ((\chi \to \phi )\to (\phi \leftrightarrow \chi ))$

यदि वांछित हो तो IFF-1 और IFF-2 को एक ही स्वयंसिद्ध में जोड़ा जा सकता है $(\phi \leftrightarrow \chi )\to ((\phi \to \chi )\land (\chi \to \phi ))$ संयुग्मन का उपयोग करना।

शास्त्रीय तर्कशास्त्र से संबंध

शास्त्रीय तर्क की प्रणाली निम्नलिखित में से किसी एक स्वयंसिद्ध को जोड़कर प्राप्त की जाती है:

• $\phi \lor \lnot \phi$ (बहिष्कृत मध्य का कानून। के रूप में भी तैयार किया जा सकता है।) $(\phi \to \chi )\to ((\lnot \phi \to \chi )\to \chi )$.)
• $\lnot \lnot \phi \to \phi$ (डबल निगेटिव एलिमिनेशन)
• $((\phi \to \chi )\to \phi )\to \phi$ (पियर्स का नियम)
• $(\lnot \phi \to \lnot \chi )\to (\chi \to \phi )$ (विरोधाभास का नियम)

सामान्य तौर पर, कोई भी शास्त्रीय पुनरुक्ति को अतिरिक्त स्वयंसिद्ध के रूप में ले सकता है जो दो-तत्व क्रिपके फ्रेम में मान्य नहीं है $\circ {\longrightarrow }\circ$ (दूसरे शब्दों में, वह मध्यवर्ती तर्क में शामिल नहीं है। स्मेटानिच का तर्क)।

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

1932 में, कर्ट गोडेल ने क्लासिकल और इंट्यूशनिस्टिक लॉजिक के बीच मध्यवर्ती तर्कशास्त्र की एक प्रणाली को परिभाषित किया; गोडेल लॉजिक्स को सहवर्ती रूप से मध्यवर्ती लॉजिक्स के रूप में जाना जाता है।

स्वीकार्य नियम

अंतर्ज्ञानवादी तर्क या तर्क का उपयोग कर एक निश्चित सिद्धांत में, स्थिति हो सकती है कि एक निहितार्थ हमेशा मेटाथ्योरेटिक रूप से पकड़ में आता है, लेकिन भाषा में नहीं। उदाहरण के लिए, शुद्ध प्रस्ताविक कलन में, यदि $(\neg A)\to (B\lor C)$ साध्य है, तो ऐसा है $(\neg A\to B)\lor (\neg A\to C)$. एक और उदाहरण है $(A\to B)\to (A\lor C)$ हमेशा सिद्ध होने का अर्थ यह भी है कि ऐसा है ${\big (}(A\to B)\to A{\big )}\lor {\big (}(A\to B)\to C{\big )}$. एक का कहना है कि स्वीकार्य नियम के रूप में इन निहितार्थों के तहत सिस्टम बंद है और उन्हें अपनाया जा सकता है।

ऑपरेटरों की गैर-अन्तर्निर्धारणीयता

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

अंतर्ज्ञानवादी तर्क में द्वैधता के नियम की आवश्यकता नहीं है, केवल गैर-विरोधाभास के नियम की आवश्यकता है। परिणामस्वरूप, किसी भी मूल संबंध के बिना नहीं किया जा सकता है, और उपरोक्त स्वयंसिद्ध सभी आवश्यक हैं। इसलिए संयोजकों और परिमाणकों के बीच की अधिकांश शास्त्रीय पहचान एक दिशा में अंतर्ज्ञानवादी तर्क के प्रमेय हैं। कुछ प्रमेय दोनों दिशाओं में चलते हैं, अर्थात समानताएं हैं, जैसा कि बाद में चर्चा की गई। नीचे निषेधों से जुड़े निहितार्थों की एक सूची दी गई है। उपरोक्त सिद्धांतों THEN-1 और THEN-2 को मिलाकर, $(P\to \neg Q)\leftrightarrow (Q\to \neg P)$ अनुसरण करता है, एक रूपांतरण जिसका उपयोग आगे के निहितार्थ प्राप्त करने के लिए किया जा सकता है।

अस्तित्वगत बनाम सार्वभौमिक परिमाणीकरण:

• $(\exists x\ \phi (x))\to \neg (\forall x\ \neg \phi (x))$
• $(\exists x\ \neg \phi (x))\to \neg (\forall x\ \phi (x))$

और इसके विपरीत,

• $(\forall x\ \neg \phi (x))\leftrightarrow \neg (\exists x\ \phi (x))$
• $(\forall x\ \phi (x))\to \neg (\exists x\ \neg \phi (x))$

उनमें केवल दो प्रस्तावों के साथ परिमित विविधताएँ हैं।

संयोजन बनाम संयोजन:

• $(\phi \vee \psi )\to \neg (\neg \phi \wedge \neg \psi )$
• $(\neg \phi \vee \psi )\to \neg (\phi \wedge \neg \psi )$
• $(\neg \phi \vee \neg \psi )\to \neg (\phi \wedge \psi )$

और इसके विपरीत,

• $(\neg \phi \wedge \neg \psi )\leftrightarrow \neg (\phi \vee \psi )$
• $(\phi \wedge \neg \psi )\to \neg (\neg \phi \vee \psi )$
• $(\phi \wedge \psi )\to \neg (\neg \phi \vee \neg \psi )$

इसलिए अस्वीकृत बयान कमजोर पूर्ववर्ती हैं, और बदले में शास्त्रीय डी मॉर्गन के सभी नियम लागू नहीं होते हैं।

पर जा रहा,

संयोजन बनाम निहितार्थ:

• $(\phi \wedge \psi )\to \neg (\phi \to \neg \psi )$
• $(\phi \wedge \neg \psi )\to \neg (\phi \to \psi )$

और इसके विपरीत,

• $(\phi \to \neg \psi )\leftrightarrow \neg (\phi \wedge \psi )$
• $(\phi \to \psi )\to \neg (\phi \wedge \neg \psi )$

के लिए सूत्र $\neg (\phi \wedge \psi )$ जताने के लिए इस्तेमाल किया जा सकता है $(\neg \phi \vee \neg \psi )\to (\phi \to \neg \psi )$ और एक संस्करण की स्थिति के साथ संस्करण को भी मान्य करता है $\phi$ और $\neg \phi$ स्विच किया गया। बाद वाले अस्वीकृत प्रस्तावों के लिए वियोगात्मक न्यायवाक्य के रूप हैं, $\neg \psi$. एक मजबूत रूप अभी भी अंतर्ज्ञानवादी तर्क में निम्नानुसार है।

संयोजन बनाम निहितार्थ:

• $(\phi \vee \psi )\to (\neg \phi \to \psi )$
• $(\neg \phi \vee \psi )\to (\phi \to \psi )$

तो, उदाहरण के लिए, अंतर्ज्ञानवादी रूप से या तो $P$ या $Q$यदि नहीं तो की तुलना में एक मजबूत प्रस्तावक सूत्र है $P$, तब $Q$, जबकि ये शास्त्रीय रूप से विनिमेय हैं। सामान्य के लिए ऐसा निहितार्थ $\psi$ न्यूनतम तर्क में मान्य नहीं है।

समानताएं:

उपरोक्त सूचियों में समानताएं भी हैं। सबसे पहले, एक संयोजन और एक संयोजन से जुड़ी समानता उत्पन्न होती है $(P\lor Q)\to R$ वास्तव में से अधिक मजबूत होना $P\to R$. समानता के दोनों पक्षों को स्वतंत्र निहितार्थों (बेतुकेपन) के संयोजन के रूप में समझा जा सकता है। कार्यात्मक व्याख्याओं में, यह कंडीशनल (कंप्यूटर प्रोग्रामिंग)|अगर-क्लॉज कंस्ट्रक्शन से मेल खाता है। तो उदा। नहीं ($P$ या $Q$) नहीं के बराबर है $P$, और नहीं भी $Q$. दूसरा, तुल्यता जिसमें एक निहितार्थ और एक संयुग्मन शामिल है, करी ंग से मेल खाती है। संयोजन संयोजक की समरूपता के कारण, यह फिर से निहित है

$(\phi \to \neg \psi )\leftrightarrow (\psi \to \neg \phi )$

इस रूपांतरण के विशेष मामले पिछली सूचियाँ बनाते हैं। संयोजन की समरूपता को नकारने के कारण के रूप में भी समझा जा सकता है $\phi$ उपरोक्त पहली दो सूचियों में पूर्ववर्ती और परिणामी के बीच स्थानांतरित किया जा सकता है।

सूचियों में समानता को संयुक्त रूप से समानता के लिए सामान्यीकृत किया जा सकता है

${\big (}\forall x.\phi (x)\to (\psi (x)\to \chi ){\big )}\,\,\,\leftrightarrow \,\,\,{\big (}\exists x.\phi (x)\land \psi (x){\big )}\to \chi$

जिसके लिए $\chi$ जैसा $\bot$ विसंधित समुच्चय के दो लक्षण हैं।

एक तुल्यता को आमतौर पर निहितार्थों के संयोजन के रूप में परिभाषित किया जाता है, और उसके बाद समकक्ष

• $(\phi \leftrightarrow \psi )\leftrightarrow {\big (}(\phi \to \psi )\land (\psi \to \phi ){\big )}$

इसके साथ, इस तरह के संयोजक बदले में इससे निश्चित हो जाते हैं:

• $(\phi \to \psi )\leftrightarrow ((\phi \lor \psi )\leftrightarrow \psi )$
• $(\phi \to \psi )\leftrightarrow ((\phi \land \psi )\leftrightarrow \phi )$
• $(\phi \land \psi )\leftrightarrow ((\phi \to \psi )\leftrightarrow \phi )$
• $(\phi \land \psi )\leftrightarrow (((\phi \lor \psi )\leftrightarrow \psi )\leftrightarrow \phi )$

के बदले में, $\{\lor ,\leftrightarrow ,\bot \}$ और $\{\land ,\leftrightarrow ,\neg \}$ अंतर्ज्ञानवादी संयोजकों के पूर्ण आधार हैं।

कार्यात्मक रूप से पूर्ण संयोजक:

जैसा कि अलेक्जेंडर वी। कुज़नेत्सोव द्वारा दिखाया गया है, निम्न में से कोई भी संयोजक - पहला टर्नरी, दूसरा एक क्विनरी - अपने आप में कार्यात्मक रूप से पूर्ण है: या तो कोई अंतर्ज्ञानवादी प्रस्तावपरक तर्क के लिए एकमात्र पर्याप्त ऑपरेटर की भूमिका निभा सकता है, इस प्रकार एक एनालॉग बनता है शास्त्रीय प्रस्तावपरक तर्क से शेफ़र स्ट्रोक का:

• ${\big (}(P\lor Q)\land \neg R{\big )}\lor {\big (}\neg P\land (Q\leftrightarrow R){\big )}$
• $P\to {\big (}Q\land \neg R\land (S\lor T){\big )}$

शब्दार्थ

शास्त्रीय मामले की तुलना में शब्दार्थ अधिक जटिल हैं। एक मॉडल सिद्धांत Heyting algebras द्वारा या समकक्ष रूप से Kripke semantics द्वारा दिया जा सकता है। हाल ही में, सत्य का एक सिमेंटिक सिद्धांत | टार्स्की-जैसे मॉडल सिद्धांत को रॉबर्ट ली कांस्टेबल द्वारा पूर्ण सिद्ध किया गया था, लेकिन शास्त्रीय रूप से पूर्णता की एक अलग धारणा के साथ।

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

इस दृष्टिकोण का एक परिणाम यह है कि अंतर्ज्ञानवादी तर्क की दो-मूल्यवान तर्क के रूप में कोई व्याख्या नहीं है, न ही परिमित-मूल्यवान तर्क के रूप में, परिचित अर्थों में। हालांकि अंतर्ज्ञानवादी तर्क तुच्छ प्रस्तावों को बरकरार रखता है $\{\top ,\bot \}$ शास्त्रीय तर्क से, एक प्रस्तावक सूत्र के प्रत्येक प्रमाण को एक वैध प्रस्तावक मूल्य माना जाता है, इस प्रकार ब्रौवर-हेटिंग-कोलमोगोरोव|प्रस्तावों-के-सेटों की हेटिंग की धारणा, प्रस्तावपरक सूत्र उनके प्रमाणों के (संभावित रूप से गैर-परिमित) सेट हैं।

हेटिंग बीजगणित शब्दार्थ

शास्त्रीय तर्कशास्त्र में, हम अक्सर उन सत्य मूल्यों पर चर्चा करते हैं जो एक सूत्र ग्रहण कर सकता है। मूल्यों को आमतौर पर बूलियन बीजगणित (संरचना) के सदस्यों के रूप में चुना जाता है। बूलियन बीजगणित में शामिल होने और मिलने के संचालन को ∧ और ∨ तार्किक संयोजकों के साथ पहचाना जाता है, ताकि फॉर्म ए ∧ बी के सूत्र का मान बूलियन बीजगणित में ए के मूल्य और बी के मूल्य का मिलन हो। तब हमारे पास उपयोगी प्रमेय है कि एक सूत्र शास्त्रीय तर्क का एक मान्य प्रस्ताव है यदि और केवल यदि इसका मान प्रत्येक मूल्यांकन (तर्क) के लिए 1 है - अर्थात्, इसके चर के मानों के किसी भी असाइनमेंट के लिए।

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

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

${\begin{aligned}{\text{Value}}[\bot ]&=\emptyset \\{\text{Value}}[\top ]&=\mathbf {R} \\{\text{Value}}[A\land B]&={\text{Value}}[A]\cap {\text{Value}}[B]\\{\text{Value}}[A\lor B]&={\text{Value}}[A]\cup {\text{Value}}[B]\\{\text{Value}}[A\to B]&={\text{int}}\left({\text{Value}}[A]^{\complement }\cup {\text{Value}}[B]\right)\end{aligned}}$

जहाँ int (X) X और X का आंतरिक (टोपोलॉजी) है^∁ इसका पूरक (सेट सिद्धांत) ।

A → B से संबंधित अंतिम पहचान हमें ¬A के मान की गणना करने की अनुमति देती है:

${\begin{aligned}{\text{Value}}[\neg A]&={\text{Value}}[A\to \bot ]\\&={\text{int}}\left({\text{Value}}[A]^{\complement }\cup {\text{Value}}[\bot ]\right)\\&={\text{int}}\left({\text{Value}}[A]^{\complement }\cup \emptyset \right)\\&={\text{int}}\left({\text{Value}}[A]^{\complement }\right)\end{aligned}}$

इन असाइनमेंट के साथ, अंतर्ज्ञानवादी रूप से मान्य फ़ार्मुले ठीक वही हैं जिन्हें संपूर्ण रेखा का मान निर्दिष्ट किया गया है।उदाहरण के लिए, सूत्र ¬(A ∧ ¬A) मान्य है, क्योंकि कोई भी सेट X को सूत्र A के मान के रूप में चुना गया है, ¬(A ∧ ¬A) का मान पूरी रेखा के रूप में दिखाया जा सकता है:

${\begin{aligned}{\text{Value}}[\neg (A\land \neg A)]&={\text{int}}\left({\text{Value}}[A\land \neg A]^{\complement }\right)&&{\text{Value}}[\neg B]={\text{int}}\left({\text{Value}}[B]^{\complement }\right)\\&={\text{int}}\left(\left({\text{Value}}[A]\cap {\text{Value}}[\neg A]\right)^{\complement }\right)\\&={\text{int}}\left(\left({\text{Value}}[A]\cap {\text{int}}\left({\text{Value}}[A]^{\complement }\right)\right)^{\complement }\right)\\&={\text{int}}\left(\left(X\cap {\text{int}}\left(X^{\complement }\right)\right)^{\complement }\right)\\&={\text{int}}\left(\emptyset ^{\complement }\right)&&{\text{int}}\left(X^{\complement }\right)\subseteq X^{\complement }\\&={\text{int}}(\mathbf {R} )\\&=\mathbf {R} \end{aligned}}$

तो इस सूत्र का मूल्यांकन सत्य है, और वास्तव में सूत्र मान्य है। लेकिन अपवर्जित मध्य का नियम, A ∨ ¬A, को A के लिए सकारात्मक वास्तविक संख्याओं के सेट के विशिष्ट मान का उपयोग करके अमान्य दिखाया जा सकता है:

${\begin{aligned}{\text{Value}}[A\lor \neg A]&={\text{Value}}[A]\cup {\text{Value}}[\neg A]\\&={\text{Value}}[A]\cup {\text{int}}\left({\text{Value}}[A]^{\complement }\right)&&{\text{Value}}[\neg B]={\text{int}}\left({\text{Value}}[B]^{\complement }\right)\\&=\{x>0\}\cup {\text{int}}\left(\{x>0\}^{\complement }\right)\\&=\{x>0\}\cup {\text{int}}\left(\{x\leqslant 0\}\right)\\&=\{x>0\}\cup \{x<0\}\\&=\{x\neq 0\}\\&\neq \mathbf {R} \end{aligned}}$

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

कृपके शब्दार्थ

Main article: Kripke semantics

मॉडल तर्क के शब्दार्थ पर अपने काम का निर्माण करते हुए, शाऊल क्रिपके ने अंतर्ज्ञानवादी तर्क के लिए एक और शब्दार्थ बनाया, जिसे क्रिपके शब्दार्थ या संबंधपरक शब्दार्थ के रूप में जाना जाता है।

तर्स्की-जैसे शब्दार्थ

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

अन्य लॉजिक्स से संबंध

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

बहु-मूल्यवान तर्क से संबंध

कर्ट गोडेल के काम में कई-मूल्यवान तर्क शामिल हैं, जो 1932 में दिखाया गया था कि अंतर्ज्ञानवादी तर्क एक परिमित-मूल्यवान तर्क नहीं है। (अंतर्ज्ञानवादी तर्क की एक अनंत-मूल्यवान तर्क व्याख्या के लिए उपरोक्त #Heyting बीजगणित शब्दार्थ शीर्षक वाला अनुभाग देखें।)

मध्यवर्ती लॉजिक्स से संबंध

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

मोडल लॉजिक से संबंध

इंट्यूशनिस्टिक प्रोपोज़िशनल लॉजिक (IPC) के किसी भी फॉर्मूले को सामान्य मोडल लॉजिक क्रिप्के शब्दार्थ # पत्राचार और पूर्णता में अनुवादित किया जा सकता है:

${\begin{aligned}\bot ^{*}&=\bot \\A^{*}&=\Box A&&{\text{if }}A{\text{ is prime (a positive literal)}}\\(A\wedge B)^{*}&=A^{*}\wedge B^{*}\\(A\vee B)^{*}&=A^{*}\vee B^{*}\\(A\to B)^{*}&=\Box \left(A^{*}\to B^{*}\right)\\(\neg A)^{*}&=\Box (\neg (A^{*}))&&\neg A:=A\to \bot \end{aligned}}$

और यह प्रदर्शित किया गया है कि अनुवादित सूत्र प्रस्तावात्मक मोडल लॉजिक S4 में मान्य है यदि और केवल यदि मूल सूत्र IPC में मान्य है। सूत्रों के उपरोक्त सेट को मोडल साथी | गोडेल-मैकिन्से-टार्स्की अनुवाद कहा जाता है।

मोडल लॉजिक S4 का एक इंट्यूशनिस्टिक संस्करण भी है जिसे कंस्ट्रक्टिव मोडल लॉजिक CS4 कहा जाता है।

लैम्ब्डा कैलकुस

आईपीसी और सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस के बीच एक विस्तारित करी-हावर्ड समरूपता है।

यह भी देखें

• बीएचके व्याख्या
• कम्प्यूटेबिलिटी तर्क
• रचनात्मक प्रमाण
• करी-हावर्ड पत्राचार
• खेल शब्दार्थ
• आबाद सेट
• इंटरमीडिएट लॉजिक्स
• अंतर्ज्ञानवादी प्रकार का सिद्धांत
• कृपके शब्दार्थ
• रैखिक तर्क
• परासंगत तर्क
• प्रासंगिकता सिद्धांत
• चिकना अतिसूक्ष्म विश्लेषण

संदर्भ

• van Dalen, Dirk, 2001, "Intuitionistic Logic", in Goble, Lou, ed., The Blackwell Guide to Philosophical Logic. Blackwell
• Morten H. Sørensen, Paweł Urzyczyn, 2006, Lectures on the Curry-Howard Isomorphism (chapter 2: "Intuitionistic Logic"). Studies in Logic and the Foundations of Mathematics vol. 149, Elsevier
• W. A. Carnielli (with A. B. M. Brunner)."Anti-intuitionism and paraconsistency". Journal of Applied Logic Volume 3, Issue 1, Mar 2005, pp. 161–184
• Arend Heyting, 1930, "Die formalen Regeln der intuitionistischen Logik," in three parts, Sitzungsberichte der preussischen Akademie der Wissenschaften: 42–71, 158–169.

इस पेज में लापता आंतरिक लिंक की सूची

• बहिष्कृत मध्य का कानून
• सहज-ज्ञान
• प्रमाण-सैद्धांतिक
• दोहरा निषेध उन्मूलन
• वसूली
• द्वंद्वात्मक व्याख्या
• सत्य मूल्य
• प्रस्तावक सूत्र
• औचित्य का सिद्धांत
• आबाद सेट
• निर्माणवाद (गणित)
• सबूत
• अस्तित्व संपत्ति
• Agda (प्रोग्रामिंग भाषा)
• सबूत सहायक
• तार्किक समानता
• वाक्य - विन्यास
• पहले क्रम का तर्क
• विरोधाभास द्वारा प्रमाण
• हिल्बर्ट-शैली कटौती प्रणाली
• सामग्री सशर्त
• बूलियन समारोह
• तार्किक विच्छेदन
• गैर-विरोधाभास का कानून
• द्वैधता का नियम
• वियोगी न्यायवाक्य
• सशर्त (कंप्यूटर प्रोग्रामिंग)
• अलग करना सेट
• सत्य का शब्दार्थ सिद्धांत
• जुड़ें और मिलें
• इंटीरियर (टोपोलॉजी)
• शाऊल क्रिप्के
• परासंगत तर्क
• द्वंद्व (गणित)
• सामान्य मॉडल तर्क
• सरल रूप से टाइप किया हुआ लैम्ब्डा कैलकुलस
• चिकना अत्यल्प विश्लेषण

बाहरी कड़ियाँ

• Stanford Encyclopedia of Philosophy: "Intuitionistic Logic" by Joan Moschovakis
• Intuitionistic Logic by Nick Bezhanishvili and Dick de Jongh (from the Institute for Logic, Language and Computation at the University of Amsterdam)
• Semantical Analysis of Intuitionistic Logic I by Saul A. Kripke from Harvard University, Cambridge, Mass., USA
• Intuitionistic Logic by Dirk van Dalen
• The discovery of E. W. Beth's semantics for intuitionistic logic by A. S. Troelstra and P. van Ulsen
• Expressing Database Queries with Intuitionistic Logic by Anthony J. Bonner. L. Thorne McCarty. Kumar Vadaparty. Rutgers University, Department of Computer Science
• Tableaux'method for intuitionistic logic through S4-translation tests the intuitionistic validity of propositional formulae; provided by the Laboratoire d'Informatique de Grenoble
• The Oxford Handbook of Philosophy of Mathematics and Logic: "Intuitionism in Mathematics" by David Charles McCarty