विधेय फ़ंक्टर तर्क: Difference between revisions

From Vigyanwiki
No edit summary
No edit summary
 
(6 intermediate revisions by 4 users not shown)
Line 1: Line 1:
{{Short description|Algebraization of first-order logic}}
{{Short description|Algebraization of first-order logic}}
[[गणितीय तर्क]] में, विधेय फ़ंक्टर लॉजिक (पीएफएल) [[प्रथम-क्रम तर्क]] (जिसे [[विधेय तर्क]] के रूप में भी जाना जाता है) को विशुद्ध रूप से बीजगणितीय माध्यमों से व्यक्त करने के कई तरीकों में से है, यानी, बिना [[परिमाणीकरण (तर्क)]]तर्क) के। पीएफएल कम संख्या में बीजगणितीय उपकरणों का उपयोग करता है जिन्हें विधेय फ़ैक्टर कहा जाता है (या विधेय संशोधक)<ref>Johannes Stern, ''Toward Predicate Approaches to Modality'', Springer, 2015, p. 11.</ref> जो शर्तों को प्राप्त करने के लिए शर्तों पर काम करता है। पीएफएल ज्यादातर [[तर्क]]शास्त्री और [[दार्शनिक]] [[विलार्ड क्वीन]] का आविष्कार है।
[[गणितीय तर्क]] में, '''विधेय फ़ंक्टर लॉजिक (पीएफएल)''' [[प्रथम-क्रम तर्क]] (जिसे [[विधेय तर्क]] के रूप में भी जाना जाता है) को विशुद्ध रूप से बीजगणितीय माध्यमों से व्यक्त करने के कई विधियों में से है, अर्थात, बिना [[परिमाणीकरण (तर्क)|परिमाणीकरण तर्क]] के पीएफएल कम संख्या में बीजगणितीय उपकरणों का उपयोग करता है जिन्हें विधेय फ़ैक्टर कहा जाता है (या विधेय संशोधक) <ref>Johannes Stern, ''Toward Predicate Approaches to Modality'', Springer, 2015, p. 11.</ref> जो नियमो को प्राप्त करने के लिए नियमो पर कार्य करता है। पीएफएल अधिकतर [[तर्क]]शास्त्री और [[दार्शनिक]] [[विलार्ड क्वीन]] का आविष्कार है।


==प्रेरणा==
==प्रेरणा==
इस खंड का स्रोत, साथ ही इस प्रविष्टि का अधिकांश भाग, क्वीन (1976) है। क्विन ने पीएफएल को प्रथम-क्रम तर्क को बीजगणित करने के तरीके के रूप में प्रस्तावित किया, जिस तरह से [[बूलियन बीजगणित (तर्क)]] प्रस्तावित तर्क को बीजगणित करता है। उन्होंने पीएफएल को [[पहचान (गणित)]] के साथ प्रथम-क्रम तर्क की बिल्कुल अभिव्यंजक शक्ति के लिए डिज़ाइन किया। इसलिए पीएफएल की [[मेटागणित]] बिल्कुल प्रथम-क्रम तर्क के समान हैं, जिनमें कोई व्याख्या किए गए विधेय अक्षर नहीं हैं: दोनों तर्क स्थिरता प्रमाण, [[पूर्णता (तर्क)]], और [[अनिर्णीत समस्या]] हैं। अपने जीवन के पिछले 30 वर्षों में तर्क और गणित पर क्विन द्वारा प्रकाशित अधिकांश कार्य किसी न किसी तरह से पीएफएल से संबंधित थे।
इस खंड का स्रोत, साथ ही इस प्रविष्टि का अधिकांश भाग, क्वीन (1976) है। क्विन ने पीएफएल को प्रथम-क्रम तर्क को बीजगणित करने के विधि के रूप में प्रस्तावित किया था, जिस तरह से [[बूलियन बीजगणित (तर्क)]] प्रस्तावित तर्क को बीजगणित करता है। उन्होंने पीएफएल को [[पहचान (गणित)]] के साथ प्रथम-क्रम तर्क की पूर्णतः अभिव्यंजक शक्ति के लिए डिज़ाइन किया था। इसलिए पीएफएल की [[मेटागणित]] पूर्णतः प्रथम-क्रम तर्क के समान हैं, जिनमें कोई व्याख्या किए गए विधेय अक्षर नहीं हैं: दोनों तर्क स्थिरता प्रमाण, [[पूर्णता (तर्क)]], और [[अनिर्णीत समस्या]] हैं। इस प्रकार अपने जीवन के पिछले 30 वर्षों में तर्क और गणित पर क्विन द्वारा प्रकाशित अधिकांश कार्य किसी न किसी तरह से पीएफएल से संबंधित थे।


क्विन ने अपने मित्र [[ रुडोल्फ कार्नाप |रुडोल्फ कार्नाप]] के लेखन से फ़नक्टर लिया, जो इसे [[दर्शन]] और गणितीय तर्क में नियोजित करने वाले पहले व्यक्ति थे, और इसे इस प्रकार परिभाषित किया:
क्विन ने अपने मित्र [[ रुडोल्फ कार्नाप |रुडोल्फ कार्नाप]] के लेखन से फ़नक्टर लिया था, जो इसे [[दर्शन]] और गणितीय तर्क में नियोजित करने वाले पहले व्यक्ति थे, और इसे इस प्रकार परिभाषित किया था:
फ़ंक्टर शब्द, आयात में व्याकरणिक लेकिन निवास स्थान में तार्किक... संकेत है जो किसी दिए गए व्याकरणिक प्रकार की अभिव्यक्ति उत्पन्न करने के लिए दिए गए व्याकरणिक प्रकार के या अधिक अभिव्यक्तियों से जुड़ता है। (क्वीन 1982:129)


फ़ंक्टर शब्द, आयात में व्याकरणिक किन्तु निवास समिष्ट में तार्किक... संकेत है जो किसी दिए गए व्याकरणिक प्रकार की अभिव्यक्ति उत्पन्न करने के लिए दिए गए व्याकरणिक प्रकार के या अधिक अभिव्यक्तियों से जुड़ता है। (क्वीन 1982:129)प्रथम-क्रम तर्क को बीजगणित करने के पीएफएल के अतिरिक्त अन्य विधियों में सम्मिलित हैं: 
*[[अल्फ्रेड टार्स्की]] और उनके अमेरिकी छात्रों द्वारा [[बेलनाकार बीजगणित]] बर्नेज़ (1959) में प्रस्तावित सरलीकृत बेलनाकार बीजगणित ने क्विन को विधेय फ़ंक्टर वाक्यांश के पहले उपयोग वाले पेपर को लिखने के लिए प्रेरित किया था;
*[[पॉल हेल्मोस]] का [[बहुपद बीजगणित]] अपने प्रभावकारी मौलिक और सिद्धांतों के आधार पर, यह बीजगणित पीएफएल से सबसे अधिक मिलता जुलता है;
*[[संबंध बीजगणित]] प्रथम-क्रम तर्क के टुकड़े को बीजगणित करता है जिसमें तीन से अधिक [[परिमाणक (तर्क)]] के सीमा में कोई परमाणु सूत्र नहीं होने वाले सूत्र सम्मिलित होते हैं। चूँकि, वह टुकड़ा [[पीनो अंकगणित|डोमेन अंकगणित]] और स्वयंसिद्ध समुच्चय सिद्धांत [[ZFC|जेडएफसी]] के लिए पर्याप्त है; इसलिए संबंध बीजगणित, पीएफएल के विपरीत, गोडेल की अपूर्णता प्रमेय है। इस प्रकार 1920 के बाद से संबंध बीजगणित पर अधिकांश कार्य टार्स्की और उनके अमेरिकी छात्रों द्वारा किया गया है। संबंध बीजगणित की शक्ति तब तक प्रकट नहीं हुई जब तक कि पीएफएल पर आधारित तीन महत्वपूर्ण पत्रों, अर्थात् बेकन (1985), कुह्न (1983), और क्वीन (1976) के बाद प्रकाशित मोनोग्राफ टार्स्की और गिवंत (1987) द्वारा प्रस्तुत किया गया था;
*[[ संयोजक | संयोजक]] लॉजिक कॉम्बिनेटर्स पर बनता है, उच्च क्रम के फ़ंक्शन जिनके फ़ंक्शन का डोमेन अन्य कॉम्बिनेटर या फ़ंक्शन होता है, और जिनके फ़ंक्शन की सीमा और कॉम्बिनेटर होती है। इसलिए [[संयोजनात्मक तर्क]] समुच्चय सिद्धांत की अभिव्यंजक शक्ति के कारण प्रथम-क्रम तर्क से आगे निकल जाता है, जो संयोजनात्मक तर्क को [[विरोधाभास]] के प्रति संवेदनशील बनाता है। दूसरी ओर, विधेय फ़ंक्टर, केवल विधेय (जिसे टर्म (तर्क) भी कहा जाता है) को विधेय में बदल देता है।
पीएफएल वास्तविक इन औपचारिकताओं में सबसे सरल है, फिर भी ऐसा भी है जिसके बारे में सबसे कम लिखा गया है।


प्रथम-क्रम तर्क को बीजगणित करने के पीएफएल के अलावा अन्य तरीकों में शामिल हैं:
क्विन का संयोजनात्मक तर्क के प्रति आजीवन आकर्षण था, जिसका प्रमाण रूसी तर्कशास्त्री मोसेस शॉनफिंकेल द्वारा संयोजनात्मक तर्क की स्थापना करने वाले पेपर के वान हेजेनॉर्ट (1967) में अनुवाद के उनके परिचय से मिलता है। जब क्विन ने 1959 में पीएफएल पर गंभीरता से कार्य करना प्रारंभ किया था, जिससे संयोजन तर्क को सामान्यतः निम्नलिखित कारणों से विफल माना गया था:
*[[अल्फ्रेड टार्स्की]] और उनके अमेरिकी छात्रों द्वारा [[बेलनाकार बीजगणित]]। बर्नेज़ (1959) में प्रस्तावित सरलीकृत बेलनाकार बीजगणित ने क्विन को विधेय फ़ंक्टर वाक्यांश के पहले उपयोग वाले पेपर को लिखने के लिए प्रेरित किया;
* 1960 के दशक के अंत में जब तक [[दाना स्कॉट]] ने संयोजन तर्क के [[मॉडल सिद्धांत]] पर लिखना प्रारंभ नहीं किया था, तब तक लगभग केवल [[हास्केल करी]], उनके छात्र और बेल्जियम में [[रॉबर्ट फेयस]] ने ही उस तर्क पर कार्य किया था;
*[[पॉल हेल्मोस]] का [[बहुपद बीजगणित]]। अपने किफायती आदिम और सिद्धांतों के आधार पर, यह बीजगणित पीएफएल से सबसे अधिक मिलता जुलता है;
*संयोजनात्मक तर्क के संतोषजनक स्वयंसिद्ध सूत्रीकरण आने में धीमे थे। इस प्रकार 1930 के दशक में, संयोजन तर्क के कुछ सूत्र संगतता प्रमाण पाए गए थे। करी ने [[करी विरोधाभास]] की भी खोज की थी, जो संयोजनात्मक तर्क की विशेषता है;
*[[संबंध बीजगणित]] प्रथम-क्रम तर्क के टुकड़े को बीजगणित करता है जिसमें तीन से अधिक [[परिमाणक (तर्क)]]तर्क) के दायरे में कोई परमाणु सूत्र नहीं होने वाले सूत्र शामिल होते हैं। हालाँकि, वह टुकड़ा [[पीनो अंकगणित]] और स्वयंसिद्ध सेट सिद्धांत [[ZFC]] के लिए पर्याप्त है; इसलिए संबंध बीजगणित, पीएफएल के विपरीत, गोडेल की अपूर्णता प्रमेय है। 1920 के बाद से संबंध बीजगणित पर अधिकांश कार्य टार्स्की और उनके अमेरिकी छात्रों द्वारा किया गया है। संबंध बीजगणित की शक्ति तब तक प्रकट नहीं हुई जब तक कि पीएफएल पर आधारित तीन महत्वपूर्ण पत्रों, अर्थात् बेकन (1985), कुह्न (1983), और क्वीन (1976) के बाद प्रकाशित मोनोग्राफ टार्स्की और गिवंत (1987);
*[[लैम्ब्डा कैलकुलस]], संयोजन तर्क के समान अभिव्यंजक शक्ति के साथ, उत्तम औपचारिकता के रूप में देखा गया था।
*[[ संयोजक ]]ी लॉजिक कॉम्बिनेटर्स पर बनता है, उच्च क्रम के फ़ंक्शन जिनके फ़ंक्शन का डोमेन अन्य कॉम्बिनेटर या फ़ंक्शन होता है, और जिनके फ़ंक्शन की सीमा और कॉम्बिनेटर होती है। इसलिए [[संयोजनात्मक तर्क]] सेट सिद्धांत की अभिव्यंजक शक्ति के कारण प्रथम-क्रम तर्क से आगे निकल जाता है, जो संयोजनात्मक तर्क को [[विरोधाभास]]ों के प्रति संवेदनशील बनाता है। दूसरी ओर, विधेय फ़ंक्टर, केवल विधेय (जिसे टर्म (तर्क) भी कहा जाता है) को विधेय में बदल देता है।
पीएफएल यकीनन इन औपचारिकताओं में सबसे सरल है, फिर भी ऐसा भी है जिसके बारे में सबसे कम लिखा गया है।


क्विन का संयोजनात्मक तर्क के प्रति आजीवन आकर्षण था, जिसका प्रमाण रूसी तर्कशास्त्री मोसेस शॉनफिंकेल द्वारा संयोजनात्मक तर्क की स्थापना करने वाले पेपर के वान हेजेनॉर्ट (1967) में अनुवाद के उनके परिचय से मिलता है। जब क्विन ने 1959 में पीएफएल पर गंभीरता से काम करना शुरू किया, तो संयोजन तर्क को आमतौर पर निम्नलिखित कारणों से विफल माना गया:
==कुह्न की निर्दिष्टीकरण==
* 1960 के दशक के अंत में जब तक [[दाना स्कॉट]] ने संयोजन तर्क के [[मॉडल सिद्धांत]] पर लिखना शुरू नहीं किया, तब तक लगभग केवल [[हास्केल करी]], उनके छात्र और बेल्जियम में [[रॉबर्ट फेयस]] ने ही उस तर्क पर काम किया था;
इस खंड में वर्णित पीएफएल वाक्यविन्यास, मौलिक और सिद्धांत अधिक सीमा तक [[स्टीवन कुह्न]] (1983) के हैं। इस प्रकार फ़ंक्शनलर्स के शब्दार्थ क्विन (1982) के हैं। इस प्रविष्टि के शेष भाग में बेकन (1985) की कुछ शब्दावली सम्मिलित है।
*संयोजनात्मक तर्क के संतोषजनक स्वयंसिद्ध सूत्रीकरण आने में धीमे थे। 1930 के दशक में, संयोजन तर्क के कुछ सूत्र संगतता प्रमाण पाए गए। करी ने [[करी विरोधाभास]] की भी खोज की, जो संयोजनात्मक तर्क की विशेषता है;
*[[लैम्ब्डा कैलकुलस]], संयोजन तर्क के समान अभिव्यंजक शक्ति के साथ, बेहतर औपचारिकता के रूप में देखा गया था।
 
==कुह्न की औपचारिकता==
इस खंड में वर्णित पीएफएल वाक्यविन्यास, आदिम और सिद्धांत काफी हद तक [[स्टीवन कुह्न]] (1983) के हैं। फ़ंक्शनलर्स के शब्दार्थ क्विन (1982) के हैं। इस प्रविष्टि के शेष भाग में बेकन (1985) की कुछ शब्दावली शामिल है।


===सिंटेक्स===
===सिंटेक्स===
एक परमाणु शब्द अपर केस लैटिन अक्षर है, I और S को छोड़कर, इसके बाद संख्यात्मक [[ ऊपर की ओर लिखा हुआ |ऊपर की ओर लिखा हुआ]] होती है जिसे इसकी डिग्री कहा जाता है, या संक्षिप्त लोअर केस वेरिएबल्स द्वारा, जिसे सामूहिक रूप से तर्क सूची के रूप में जाना जाता है। किसी पद की डिग्री विधेय अक्षर के बाद चरों की संख्या के समान ही जा[[नकार]]देती है। डिग्री 0 का परमाणु शब्द [[बूलियन चर]] या सत्य मान को दर्शाता है। I की डिग्री हमेशा 2 होती है और इसलिए इसे दर्शाया नहीं गया है।
एक परमाणु शब्द अपर केस लैटिन अक्षर है, I और S को छोड़कर, इसके बाद संख्यात्मक [[ ऊपर की ओर लिखा हुआ |सुपरस्क्रिप्ट]] होती है जिसे इसकी डिग्री कहा जाता है, या संक्षिप्त लोअर केस वेरिएबल्स द्वारा, जिसे सामूहिक रूप से तर्क सूची के रूप में जाना जाता है। किसी पद की डिग्री विधेय अक्षर के बाद चरों की संख्या के समान ही जा[[नकार|नकारी]] देती है। इस प्रकार डिग्री 0 का परमाणु शब्द [[बूलियन चर]] या सत्य मान को दर्शाता है। इस प्रकार I की डिग्री सदैव 2 होती है और इसलिए इसे दर्शाया नहीं गया है।


कॉम्बिनेटरी (शब्द क्वीन का है) विधेय फ़ैक्टर, पीएफएल के सभी मोनैडिक और विशिष्ट, 'इनव', 'इनव', '∃', '+' और 'पी' हैं। शब्द या तो परमाणु शब्द है, या निम्नलिखित पुनरावर्ती नियम द्वारा निर्मित है। यदि τ पद है, तो 'Inv'τ, 'inv'τ, '∃'τ, '+'τ, और 'p'τ पद हैं। सुपरस्क्रिप्ट n, n [[प्राकृतिक संख्या]] > 1 वाला फ़ैक्टर, उस फ़ैक्टर के n लगातार अनुप्रयोगों (पुनरावृत्तियों) को दर्शाता है।
कॉम्बिनेटरी (शब्द क्वीन का है) विधेय फ़ैक्टर, पीएफएल के सभी मोनैडिक और विशिष्ट, 'इनव', 'इनव', '∃', '+' और 'p' हैं। शब्द या तो परमाणु शब्द है, या निम्नलिखित पुनरावर्ती नियम द्वारा निर्मित है। यदि τ पद है, तो 'Inv'τ, 'inv'τ, '∃'τ, '+'τ, और 'p'τ पद हैं। सुपरस्क्रिप्ट n, n [[प्राकृतिक संख्या]] > 1 वाला फ़ैक्टर, उस फ़ैक्टर के n निरंतर अनुप्रयोगों (पुनरावृत्तियों) को दर्शाता है।


सूत्र या तो शब्द है या पुनरावर्ती नियम द्वारा परिभाषित है: यदि α और β सूत्र हैं, तो αβ और ~(α) भी इसी तरह सूत्र हैं। इसलिए ~ अन्य मोनैडिक फ़ंक्टर है, और कॉन्सटेनेशन एकमात्र डायडिक विधेय फ़ैक्टर है। क्विन ने इन फ़ैक्टर्स को एलेथिक कहा। ~ की स्वाभाविक व्याख्या निषेध है; संयोजन कोई भी [[तार्किक संयोजक]] है, जो निषेध के साथ संयुक्त होने पर संयोजकों का [[कार्यात्मक पूर्णता]] सेट बनाता है। क्विन का पसंदीदा कार्यात्मक पूर्ण सेट [[तार्किक संयोजन]] और निषेध था। इस प्रकार संयोजित पदों को संयुक्त माना जाता है। अंकन '+' बेकन (1985) का है; अन्य सभी संकेतन क्वीन (1976; 1982) के हैं। पीएफएल का एलेथिक भाग क्वीन (1982) के बूलियन शब्द स्कीमाटा के समान है।
सूत्र या तो शब्द है या पुनरावर्ती नियम द्वारा परिभाषित है: यदि α और β सूत्र हैं, तो αβ और ~(α) भी इसी तरह सूत्र हैं। इसलिए ~ अन्य मोनैडिक फ़ंक्टर है, और कॉन्सटेनेशन एकमात्र डायडिक विधेय फ़ैक्टर है। क्विन ने इन फ़ैक्टर्स को एलेथिक कहा ~ की स्वाभाविक व्याख्या निषेध है; संयोजन कोई भी [[तार्किक संयोजक]] है, जो निषेध के साथ संयुक्त होने पर संयोजकों का [[कार्यात्मक पूर्णता]] समुच्चय बनाता है। क्विन का रोचक कार्यात्मक पूर्ण समुच्चय [[तार्किक संयोजन]] और निषेध था। इस प्रकार संयोजित पदों को संयुक्त माना जाता है। अंकन '+' बेकन (1985) का है; अन्य सभी संकेतन क्वीन (1976; 1982) के हैं। पीएफएल का एलेथिक भाग क्वीन (1982) के बूलियन शब्द स्कीमाटा के समान है।


जैसा कि सर्वविदित है, दो एलेथिक फ़ंक्टर को निम्नलिखित सिंटैक्स और शब्दार्थ के साथ एकल डायडिक फ़ैक्टर द्वारा प्रतिस्थापित किया जा सकता है: यदि α और β सूत्र हैं, तो (αβ) ऐसा सूत्र है जिसका शब्दार्थ (α और/या β) नहीं है ( [[शेफ़र लाइन]] और लॉजिकल NOR देखें)।
जैसा कि सर्वविदित है, दो एलेथिक फ़ंक्टर को निम्नलिखित सिंटैक्स और शब्दार्थ के साथ एकल डायडिक फ़ैक्टर द्वारा प्रतिस्थापित किया जा सकता है: यदि α और β सूत्र हैं, तो (αβ) ऐसा सूत्र है जिसका शब्दार्थ (α और/या β) नहीं है ( [[शेफ़र लाइन]] और लॉजिकल NOR देखें)।


===सिद्धांत और शब्दार्थ===
===सिद्धांत और शब्दार्थ===
क्विन ने पीएफएल के लिए न तो स्वयंसिद्धीकरण और न ही प्रमाण प्रक्रिया निर्धारित की। पीएफएल का निम्नलिखित स्वयंसिद्धीकरण, कुह्न (1983) में प्रस्तावित दो में से एक, संक्षिप्त और वर्णन करने में आसान है, लेकिन [[मुक्त चर]] का व्यापक उपयोग करता है और इसलिए पीएफएल की भावना के साथ पूर्ण न्याय नहीं करता है। कुह्न मुक्त चर के साथ और स्वयंसिद्धीकरण प्रदान करता है, लेकिन इसका वर्णन करना कठिन है और यह परिभाषित फ़ंक्शनलर्स का व्यापक उपयोग करता है। कुह्न ने अपने पीएफएल स्वयंसिद्धीकरण स्थिरता प्रमाण और पूर्णता (तर्क) दोनों को सिद्ध किया।
क्विन ने पीएफएल के लिए न तो स्वयंसिद्धीकरण और न ही प्रमाण प्रक्रिया निर्धारित की थी। पीएफएल का निम्नलिखित स्वयंसिद्धीकरण, कुह्न (1983) में प्रस्तावित दो में से एक, संक्षिप्त और वर्णन करने में सरल है, किन्तु [[मुक्त चर]] का व्यापक उपयोग करता है और इसलिए पीएफएल की भावना के साथ पूर्ण न्याय नहीं करता है। कुह्न मुक्त चर के साथ और स्वयंसिद्धीकरण प्रदान करता है, किन्तु इसका वर्णन करना कठिन है और यह परिभाषित फ़ंक्शनलर्स का व्यापक उपयोग करता है। कुह्न ने अपने पीएफएल स्वयंसिद्धीकरण स्थिरता प्रमाण और पूर्णता (तर्क) दोनों को सिद्ध किया था।


यह खंड आदिम विधेय फ़ैक्टर और कुछ परिभाषित फ़ैक्टरों के आसपास बनाया गया है। एलेथिक फ़ैक्टर्स को [[भावनात्मक तर्क]] के लिए सिद्धांतों के किसी भी सेट द्वारा स्वयंसिद्ध किया जा सकता है जिनके आदिम निषेध हैं और ∧ या ∨ में से हैं। समान रूप से, भावनात्मक तर्क की सभी तनातनी (तर्क) को स्वयंसिद्धों के रूप में लिया जा सकता है।
यह खंड मौलिक विधेय फ़ैक्टर और कुछ परिभाषित फ़ैक्टरों के आसपास बनाया गया है। एलेथिक फ़ैक्टर्स को [[भावनात्मक तर्क]] के लिए सिद्धांतों के किसी भी समुच्चय द्वारा स्वयंसिद्ध किया जा सकता है जिनके मौलिक निषेध हैं और ∧ या ∨ में से हैं। समान रूप से, भावनात्मक तर्क की सभी तनातनी (तर्क) को स्वयंसिद्धों के रूप में लिया जा सकता है।


प्रत्येक विधेय फ़ैक्टर के लिए क्विन (1982) के शब्दार्थ को अमूर्तन (सेट बिल्डर नोटेशन) के संदर्भ में नीचे बताया गया है, इसके बाद या तो कुह्न (1983) से संबंधित स्वयंसिद्ध कथन, या क्विन (1976) से परिभाषा दी गई है। संकेतन <math>\{x_1\cdots x_n : Fx_1\cdots x_n\}</math> परमाणु सूत्र को संतुष्ट करने वाले n-tuple|n-tuples के समुच्चय को दर्शाता है <math>Fx_1\cdots x_n.</math>
प्रत्येक विधेय फ़ैक्टर के लिए क्विन (1982) के शब्दार्थ को अमूर्तन (सेट बिल्डर नोटेशन) के संदर्भ में नीचे बताया गया है, इसके बाद या तो कुह्न (1983) से संबंधित स्वयंसिद्ध कथन, या क्विन (1976) से परिभाषा दी गई है। संकेतन <math>\{x_1\cdots x_n : Fx_1\cdots x_n\}</math> परमाणु सूत्र को संतुष्ट करने वाले n-ट्यूपल के समुच्चय <math>Fx_1\cdots x_n.</math> को दर्शाता है
*पहचान, {{mvar|I}}, परिभाषित किया जाता है:
*पहचान, {{mvar|I}}, परिभाषित किया जाता है:
:<math> IFx_1x_2\cdots x_n \leftrightarrow (Fx_1x_1\cdots x_n \leftrightarrow Fx_2x_2\cdots x_n)\text{.}</math>
:<math> IFx_1x_2\cdots x_n \leftrightarrow (Fx_1x_1\cdots x_n \leftrightarrow Fx_2x_2\cdots x_n)\text{.}</math>
पहचान [[प्रतिवर्ती संबंध]] है ({{mvar|Ixx}}), [[सममित]] ({{math|''Ixy''→''Iyx''}}), [[सकर्मक संबंध]] ({{math|(''Ixy''∧''Iyz'') → ''Ixz''}}), और प्रतिस्थापन संपत्ति का पालन करता है:
पहचान [[प्रतिवर्ती संबंध]] है ({{mvar|Ixx}}), [[सममित]] ({{math|''Ixy''→''Iyx''}}), [[सकर्मक संबंध]] ({{math|(''Ixy''∧''Iyz'') → ''Ixz''}}), और प्रतिस्थापन गुण  का पालन करता है:
:<math>(Fx_1\cdots x_n \land Ix_1y) \rightarrow Fyx_2\cdots x_n.</math>
:<math>(Fx_1\cdots x_n \land Ix_1y) \rightarrow Fyx_2\cdots x_n.</math>
*पैडिंग, '+', किसी भी तर्क सूची के बाईं ओर वेरिएबल जोड़ता है।
*पैडिंग, '+', किसी भी तर्क सूची के बाईं ओर वेरिएबल जोड़ता है।
Line 55: Line 53:
एस 2 से अधिक किसी भी परिमित डिग्री के सभी शब्दों के प्रति संवेदनशीलता की धारणा को सामान्यीकृत करता है। एन.बी.: एस को संयोजन तर्क के संयोजन तर्क एस के साथ भ्रमित नहीं किया जाना चाहिए।
एस 2 से अधिक किसी भी परिमित डिग्री के सभी शब्दों के प्रति संवेदनशीलता की धारणा को सामान्यीकृत करता है। एन.बी.: एस को संयोजन तर्क के संयोजन तर्क एस के साथ भ्रमित नहीं किया जाना चाहिए।
*''[[कार्तीय गुणन]]'', <math>\times</math>;
*''[[कार्तीय गुणन]]'', <math>\times</math>;
:<math>F^m \times G^n \leftrightarrow F^m \exist^m G^n.</math> केवल यहीं पर, क्विन ने इन्फ़िक्स नोटेशन को अपनाया, क्योंकि कार्टेशियन उत्पाद के लिए यह इन्फ़िक्स नोटेशन गणित में बहुत अच्छी तरह से स्थापित है। कार्टेशियन उत्पाद निम्नानुसार संयोजन को पुनः स्थापित करने की अनुमति देता है:
:<math>F^m \times G^n \leftrightarrow F^m \exist^m G^n.</math>
:केवल यहीं पर, क्विन ने इन्फ़िक्स नोटेशन को अपनाया था, क्योंकि कार्टेशियन उत्पाद के लिए यह इन्फ़िक्स नोटेशन गणित में बहुत अच्छी तरह से स्थापित है। कार्टेशियन उत्पाद निम्नानुसार संयोजन को पुनः स्थापित करने की अनुमति देता है:
:<math>F^mx_1\cdots x_mG^nx_1\cdots x_n \leftrightarrow (F^m \times G^n)x_1\cdots x_mx_1\cdots x_n.</math>
:<math>F^mx_1\cdots x_mG^nx_1\cdots x_n \leftrightarrow (F^m \times G^n)x_1\cdots x_mx_1\cdots x_n.</math>
संयोजित तर्क सूची को पुन: व्यवस्थित करें ताकि डुप्लिकेट चर की जोड़ी को सबसे बाईं ओर स्थानांतरित किया जा सके, फिर डुप्लिकेशन को खत्म करने के लिए एस को आमंत्रित करें। इसे आवश्यकतानुसार कई बार दोहराने से अधिकतम लंबाई(''m'',''n'') की तर्क सूची प्राप्त होती है।
संयोजित तर्क सूची को पुन: व्यवस्थित करें जिससे डुप्लिकेट चर की जोड़ी को सबसे बाईं ओर समिष्टांतरित किया जा सकता है, फिर डुप्लिकेशन को समाप्त करने के लिए एस को आमंत्रित करें। इसे आवश्यकतानुसार कई बार दोहराने से अधिकतम लंबाई (''m'',''n'') की तर्क सूची प्राप्त होती है।


अगले तीन फ़ैक्टर इच्छानुसार तर्क सूचियों को पुन: व्यवस्थित करने में सक्षम बनाते हैं।
अगले तीन फ़ैक्टर इच्छानुसार तर्क सूचियों को पुन: व्यवस्थित करने में सक्षम बनाते हैं।
*''प्रमुख व्युत्क्रम'', इनव, तर्क सूची में चरों को दाईं ओर घुमाता है, ताकि अंतिम चर पहला बन जाए।
*''प्रमुख व्युत्क्रम'', इनव, तर्क सूची में चरों को दाईं ओर घुमाता है, जिससे अंतिम चर पहला बन जाए।
:<math>\operatorname{Inv} F^n \ \overset{\underset{\mathrm{def}}{}}{=}\ \{x_1\cdots x_n : F^nx_nx_1\cdots x_{n-1}\}.</math>
:<math>\operatorname{Inv} F^n \ \overset{\underset{\mathrm{def}}{}}{=}\ \{x_1\cdots x_n : F^nx_nx_1\cdots x_{n-1}\}.</math>
:<math>\operatorname{Inv} Fx_1\cdots x_n \leftrightarrow Fx_nx_1\cdots x_{n-1}.</math>
:<math>\operatorname{Inv} Fx_1\cdots x_n \leftrightarrow Fx_nx_1\cdots x_{n-1}.</math>
Line 66: Line 65:
:<math>\operatorname{inv} F^n \ \overset{\underset{\mathrm{def}}{}}{=}\ \{x_1\cdots x_n : F^n x_2x_1\cdots x_n\}.</math>
:<math>\operatorname{inv} F^n \ \overset{\underset{\mathrm{def}}{}}{=}\ \{x_1\cdots x_n : F^n x_2x_1\cdots x_n\}.</math>
:<math>\operatorname{inv} Fx_1\cdots x_n \leftrightarrow Fx_2x_1\cdots x_n.</math>
:<math>\operatorname{inv} Fx_1\cdots x_n \leftrightarrow Fx_2x_1\cdots x_n.</math>
*क्रमपरिवर्तन, 'पी', तर्क सूची में दूसरे से अंतिम चर को बाईं ओर घुमाता है, ताकि दूसरा चर अंतिम बन जाए।
*क्रमपरिवर्तन, 'p', तर्क सूची में दूसरे से अंतिम चर को बाईं ओर घुमाता है, जिससे दूसरा चर अंतिम बन जाता है।
:<math>\ pF^n \ \overset{\underset{\mathrm{def}}{}}{=}\ \{x_1\cdots x_n : F^n x_1x_3\cdots x_nx_2\}.</math>
:<math>\ pF^n \ \overset{\underset{\mathrm{def}}{}}{=}\ \{x_1\cdots x_n : F^n x_1x_3\cdots x_nx_2\}.</math>
:<math> pFx_1\cdots x_n \leftrightarrow \operatorname{Inv} \operatorname{inv} Fx_1x_3\cdots x_nx_2.</math>
:<math> pFx_1\cdots x_n \leftrightarrow \operatorname{Inv} \operatorname{inv} Fx_1x_3\cdots x_nx_2.</math>
n चरों से युक्त तर्क सूची को देखते हुए, 'p' स्पष्ट रूप से अंतिम n−1 चर को साइकिल श्रृंखला की तरह मानता है, जिसमें प्रत्येक चर श्रृंखला में लिंक बनाता है। 'पी' का अनुप्रयोग श्रृंखला को लिंक से आगे बढ़ाता है। k से F तक 'p' का लगातार अनुप्रयोग<sup>n</sup> k+1 वेरिएबल को F में दूसरे तर्क स्थान पर ले जाता है।
n चरों से युक्त तर्क सूची को देखते हुए, 'p' स्पष्ट रूप से अंतिम n−1 चर को साइकिल श्रृंखला की तरह मानता है, जिसमें प्रत्येक चर श्रृंखला में लिंक बनाता है। 'p' का अनुप्रयोग श्रृंखला को लिंक से आगे बढ़ाता है। k से F तक 'p<sup>n</sup>' का निरंतर अनुप्रयोग k+1 वेरिएबल को F में दूसरे तर्क समिष्ट पर ले जाता है।


जब n=2, 'Inv' और 'inv' केवल x का आदान-प्रदान करते हैं<sub>1</sub> और एक्स<sub>2</sub>. जब n=1, उनका कोई प्रभाव नहीं पड़ता। अतः n <3 होने पर 'p' का कोई प्रभाव नहीं पड़ता।
जब n=2, 'Inv' और 'inv' केवल x<sub>1</sub> और x<sub>2</sub> का आदान-प्रदान करते हैं. जब n=1, उनका कोई प्रभाव नहीं पड़ता है। अतः n <3 होने पर 'p' का कोई प्रभाव नहीं पड़ता है।


कुह्न (1983) प्रमुख व्युत्क्रम और लघु व्युत्क्रम को आदिम मानते हैं। कुह्न में अंकन 'p' 'inv' से मेल खाता है; उसके पास क्रमपरिवर्तन का कोई एनालॉग नहीं है और इसलिए उसके पास इसके लिए कोई सिद्धांत नहीं है। यदि, क्वीन (1976) के बाद, 'पी' को आदिम के रूप में लिया जाता है, तो 'इनव' और 'इनव' को '+', '∃' और पुनरावृत्त 'पी' के गैर-तुच्छ संयोजन के रूप में परिभाषित किया जा सकता है।
कुह्न (1983) प्रमुख व्युत्क्रम और लघु व्युत्क्रम को मौलिक मानते हैं। कुह्न में अंकन 'p' 'inv' से मेल खाता है; उसके पास क्रमपरिवर्तन का कोई एनालॉग नहीं है और इसलिए उसके पास इसके लिए कोई सिद्धांत नहीं है। यदि, क्वीन (1976) के बाद, 'p' को मौलिक के रूप में लिया जाता है, तो 'इनव' और 'इनव' को '+', '∃' और पुनरावृत्त 'p' के सामान्य संयोजन के रूप में परिभाषित किया जा सकता है।


निम्न तालिका सारांशित करती है कि फ़ंक्शनलर्स अपने तर्कों की डिग्री को कैसे प्रभावित करते हैं।
निम्न तालिका सारांशित करती है कि फ़ंक्शनलर्स अपने तर्कों की डिग्री को कैसे प्रभावित करते हैं।
{| class="wikitable" style="text-align: center;"
{| class="wikitable" style="text-align: center;"
!Expression
!अभिव्यक्ति
!Degree
!डिग्री
|-
|-
|<math>p;\operatorname{Inv};\operatorname{inv};\ \lnot;\ I</math>
|<math>p;\operatorname{Inv};\operatorname{inv};\ \lnot;\ I</math>
Line 91: Line 90:
वैधता को प्रभावित किए बिना, विधेय पत्र के सभी उदाहरणों को उसी डिग्री के किसी अन्य विधेय पत्र द्वारा प्रतिस्थापित किया जा सकता है। प्रथम-क्रम तर्क हैं:
वैधता को प्रभावित किए बिना, विधेय पत्र के सभी उदाहरणों को उसी डिग्री के किसी अन्य विधेय पत्र द्वारा प्रतिस्थापित किया जा सकता है। प्रथम-क्रम तर्क हैं:
* एक वैध, सरल तर्क और निष्कर्ष के नियम के रूप;
* एक वैध, सरल तर्क और निष्कर्ष के नियम के रूप;
*मान लीजिए α और β पीएफएल सूत्र हैं जिनमें <math>x_1</math> प्रकट नहीं होता है। तो अगर <math>(\alpha \land Fx_1...x_n) \rightarrow \beta </math> तो फिर, यह पीएफएल प्रमेय है <math>(\alpha \land \exist Fx_2...x_n) \rightarrow \beta </math> इसी तरह पीएफएल प्रमेय है।
*मान लीजिए α और β पीएफएल सूत्र हैं जिनमें <math>x_1</math> प्रकट नहीं होता है। तो यदि  <math>(\alpha \land Fx_1...x_n) \rightarrow \beta </math> तो फिर, यह पीएफएल प्रमेय है <math>(\alpha \land \exist Fx_2...x_n) \rightarrow \beta </math> इसी तरह पीएफएल प्रमेय है।


===कुछ उपयोगी परिणाम===
===कुछ उपयोगी परिणाम===
पीएफएल को स्वयंसिद्ध करने के बजाय, क्वीन (1976) ने निम्नलिखित अनुमानों को उम्मीदवार स्वयंसिद्ध के रूप में प्रस्तावित किया।
पीएफएल को स्वयंसिद्ध करने के अतिरिक्त, क्वीन (1976) ने निम्नलिखित अनुमानों को उम्मीदवार स्वयंसिद्ध के रूप में प्रस्तावित किया था।


: <math>\exist I</math>
: <math>\exist I</math>
'p' का n−1 लगातार पुनरावृत्ति यथास्थिति बहाल करता है:
'p' का n−1 निरंतर पुनरावृत्ति यथास्थिति बहाल करता है:
: <math>F^n \leftrightarrow p^{n-1}F^n</math>
: <math>F^n \leftrightarrow p^{n-1}F^n</math>
+ और ∃ दूसरे को नष्ट करें:
+ और ∃ दूसरे को नष्ट करें:
Line 108: Line 107:
\lnot\exist F^n \rightarrow \exist \lnot F^n\\
\lnot\exist F^n \rightarrow \exist \lnot F^n\\
p\lnot F^n \leftrightarrow \lnot pF^n\end{cases}</math>
p\lnot F^n \leftrightarrow \lnot pF^n\end{cases}</math>
+ और पी संयोजन पर वितरित करता है:
+ और p संयोजन पर वितरित करता है:


: <math>\begin{cases}+(F^nG^m) \leftrightarrow (+F^n+G^m)\\
: <math>\begin{cases}+(F^nG^m) \leftrightarrow (+F^n+G^m)\\
p(F^nG^m) \leftrightarrow (pF^npG^m)\end{cases}</math>
p(F^nG^m) \leftrightarrow (pF^npG^m)\end{cases}</math>
पहचान का दिलचस्प निहितार्थ है:
पहचान का रोचक निहितार्थ है:
: <math>IF^n \rightarrow p^{n-2} \exist p+F^n</math>
: <math>IF^n \rightarrow p^{n-2} \exist p+F^n</math>
क्विन ने नियम का भी अनुमान लगाया: यदि {{mvar|&alpha;}} पीएफएल प्रमेय है, तो ऐसा ही है {{math|''p&alpha;'', +&alpha;}}, और <math>\lnot \exist \lnot \alpha</math>.
क्विन ने नियम का भी अनुमान लगाया: यदि {{mvar|&alpha;}} पीएफएल प्रमेय है, तो ऐसा {{math|''p&alpha;'', +&alpha;}}, और <math>\lnot \exist \lnot \alpha</math> ही है.


==बेकन का कार्य==
==बेकन का कार्य==
बेकन (1985) [[सामग्री सशर्त]], नेगेशन, आइडेंटिटी, पैडिंग और मेजर और माइनर व्युत्क्रम को आदिम और क्रॉपिंग को परिभाषित मानता है। उपरोक्त से कुछ भिन्न शब्दावली और संकेतन का उपयोग करते हुए, बेकन (1985) ने पीएफएल के दो सूत्र प्रस्तुत किए:
बेकन (1985) [[सामग्री सशर्त|पदार्थ नियमबद्ध]], नेगेशन, आइडेंटिटी, पैडिंग और मेजर और माइनर व्युत्क्रम को मौलिक और क्रॉपिंग को परिभाषित मानता है। उपरोक्त से कुछ भिन्न शब्दावली और संकेतन का उपयोग करते हुए, बेकन (1985) ने पीएफएल के दो सूत्र प्रस्तुत किए:
* [[फ्रेडरिक फिच]] की शैली में [[प्राकृतिक कटौती]] सूत्रीकरण। बेकन इस सूत्रीकरण को पूर्ण विस्तार से संगति प्रमाण एवं पूर्णता (तर्क) सिद्ध करते हैं।
* [[फ्रेडरिक फिच]] की शैली में [[प्राकृतिक कटौती]] सूत्रीकरण बेकन इस सूत्रीकरण को पूर्ण विस्तार से संगति प्रमाण एवं पूर्णता (तर्क) सिद्ध करते हैं।
*एक स्वयंसिद्ध सूत्रीकरण, जिसे बेकन दावा करते हैं, लेकिन साबित नहीं करते, पिछले वाले के बराबर है। इनमें से कुछ स्वयंसिद्ध बातें केवल बेकन के संकेतन में दोहराए गए क्विन अनुमान हैं।
*एक स्वयंसिद्ध सूत्रीकरण, जिसे बेकन प्रमाणित करते हैं, किन्तु सिद्ध नहीं करते है, पिछले वाले के समान है। इनमें से कुछ स्वयंसिद्ध बातें केवल बेकन के संकेतन में दोहराए गए क्विन अनुमान हैं।


बेकन भी:
बेकन भी:
* सोमरस (1982) के [[शब्द तर्क]] के साथ पीएफएल के संबंध पर चर्चा करता है, और तर्क देता है कि लॉकवुड के सोमरस के परिशिष्ट में प्रस्तावित वाक्यविन्यास का उपयोग करके पीएफएल को पुनर्गठित करने से पीएफएल को पढ़ना, उपयोग करना और पढ़ाना आसान हो जाना चाहिए;
* सोमरस (1982) के [[शब्द तर्क]] के साथ पीएफएल के संबंध पर चर्चा करता है, और तर्क देता है कि लॉकवुड के सोमरस के परिशिष्ट में प्रस्तावित वाक्यविन्यास का उपयोग करके पीएफएल को पुनर्गठित करने से पीएफएल को पढ़ना, उपयोग करना और पढ़ाना सरल हो जाना चाहिए;
*'इन्व' और 'इन्व' की [[समूह सिद्धांत]] संरचना को छूता है;
*'इन्व' और 'इन्व' की [[समूह सिद्धांत]] संरचना स्पर्श करता है;
*उल्लेख है कि भावनात्मक तर्क, मोनैडिक विधेय तर्क, [[मोडल तर्क]] [[S5 (मोडल लॉजिक)]], और (अन)परम्यूटेड रिलेशन (गणित) के बूलियन लॉजिक, सभी पीएफएल के टुकड़े हैं।
*उल्लेख है कि भावनात्मक तर्क, मोनैडिक विधेय तर्क, [[मोडल तर्क]] [[S5 (मोडल लॉजिक)]], और परम्यूटेड सम्बन्ध (गणित) के बूलियन लॉजिक, सभी पीएफएल के टुकड़े हैं।


==प्रथम-क्रम तर्क से पीएफएल तक==
==प्रथम-क्रम तर्क से पीएफएल तक==
निम्नलिखित [[कलन विधि]] को क्वीन (1976: 300-2) से अनुकूलित किया गया है। प्रथम-क्रम तर्क के [[वाक्य (गणितीय तर्क)]] को देखते हुए, पहले निम्नलिखित कार्य करें:
निम्नलिखित [[कलन विधि]] को क्वीन (1976: 300-2) से अनुकूलित किया गया है। प्रथम-क्रम तर्क के [[वाक्य (गणितीय तर्क)]] को देखते हुए, पहले निम्नलिखित कार्य करें:
* प्रत्येक विधेय अक्षर के साथ उसकी डिग्री बताते हुए संख्यात्मक सबस्क्रिप्ट संलग्न करें;
* प्रत्येक विधेय अक्षर के साथ उसकी डिग्री बताते हुए संख्यात्मक सबस्क्रिप्ट संलग्न करें;
* सभी [[सार्वभौमिक परिमाणक]]ों का [[अस्तित्वगत परिमाणक]]ों और निषेध में अनुवाद करें;
* सभी [[सार्वभौमिक परिमाणक]] का [[अस्तित्वगत परिमाणक]] और निषेध में अनुवाद करें;
* x=y रूप के सभी [[परमाणु सूत्र]]ों को Ixy के रूप में पुनः स्थापित करें।
* x=y रूप के सभी [[परमाणु सूत्र]] को Ixy के रूप में पुनः स्थापित करें।


अब पूर्ववर्ती परिणाम पर निम्नलिखित एल्गोरिदम लागू करें:
अब पूर्ववर्ती परिणाम पर निम्नलिखित एल्गोरिदम प्रयुक्त करें:
{{ordered list
{{ordered list
|Translate the matrices of the most deeply nested quantifiers into [[disjunctive normal form]], consisting of [[logical OR|disjuncts]] of [[logical AND|conjuncts]] of terms, negating atomic terms as required. The resulting subformula contains only negation, conjunction, disjunction, and existential quantification.
|सबसे गहराई से निहित क्वांटिफायर के आव्यूहों का अनुवाद [[डिजजंक्टिव सामान्य रूप]] में करें, जिसमें [[तार्किक या|डिजंक्ट्स]] के [[तार्किक और|संयुक्त]] पद सम्मिलित हों, आवश्यकतानुसार परमाणु शब्दों को अस्वीकार। परिणामी उपसूत्र में केवल निषेध, संयोजन, विच्छेदन और अस्तित्वगत परिमाणीकरण सम्मिलित है।
 
|[[मार्ग के नियम (तर्क)|मार्ग के नियम का उपयोग करके आव्यूह में विच्छेदों पर अस्तित्व संबंधी परिमाणकों को वितरित करें]] (क्विन 1982: 119):
|Distribute the existential quantifiers over the disjuncts in the matrix using the [[rules of passage (logic)|rule of passage]] (Quine 1982: 119):
:<math>\exist x[\alpha (x) \lor \gamma (x)] \leftrightarrow (\exist x \alpha (x) \lor \exist x \gamma (x)).</math>
:<math>\exist x[\alpha (x) \lor \gamma (x)] \leftrightarrow (\exist x \alpha (x) \lor \exist x \gamma (x)).</math>


|Replace conjunction by [[Cartesian product]], by invoking the fact:
|तथ्य का उपयोग करके संयोजन को [[कार्टेशियन उत्पाद]] से बदलें:
:<math>(F^m \land G^n) \leftrightarrow (F^m \times G^n) \leftrightarrow (F^m \exist^m G^n); m<n.</math>
:<math>(F^m \land G^n) \leftrightarrow (F^m \times G^n) \leftrightarrow (F^m \exist^m G^n); m<n.</math>


|Concatenate the argument lists of all atomic terms, and move the concatenated list to the far right of the subformula.
|सभी परमाणु शब्दों की तर्क सूचियों को संयोजित करें, और संयोजित सूची को उपसूत्र के सबसे दाईं ओर ले जाएँ।
 
|परिमाणित चर के सभी उदाहरणों (इसे ''y'' कहें) को तर्क सूची के बाईं ओर ले जाने के लिए '''Inv''' और '''inv''' का उपयोग करें।
|Use '''Inv''' and '''inv''' to move all instances of the quantified variable (call it ''y'') to the left of the argument list.
|''Y'' के अंतिम उदाहरण को छोड़कर सभी को हटाने के लिए जितनी बार आवश्यक हो '''S''' का उपयोग करें। ''''' के एक उदाहरण के साथ उपसूत्र को उपसर्ग करके ''y'' को हटा दें।
 
|(1)-(6) को तब तक दोहराएँ जब तक कि सभी परिमाणित चर समाप्त न हो जाएँ। समतुल्यता का आह्वान करके परिमाणक के सीमा में आने वाले किसी भी वियोजन को हटा दें:
|Invoke '''S''' as many times as required to eliminate all but the last instance of ''y''. Eliminate ''y'' by prefixing the subformula with one instance of ''''''.
 
|Repeat (1)-(6) until all quantified variables have been eliminated. Eliminate any disjunctions falling within the scope of a quantifier by invoking the equivalence:
:<math> (\alpha \lor \beta \lor ...) \leftrightarrow \lnot(\lnot\alpha \land \lnot\beta \land ...).</math>
:<math> (\alpha \lor \beta \lor ...) \leftrightarrow \lnot(\lnot\alpha \land \lnot\beta \land ...).</math>
}}
}}
पीएफएल से प्रथम-क्रम तर्क तक रिवर्स अनुवाद पर क्विन (1976: 302-4) में चर्चा की गई है।
पीएफएल से प्रथम-क्रम तर्क तक रिवर्स अनुवाद पर क्विन (1976: 302-4) में चर्चा की गई है।


गणित का विहित आधार स्वयंसिद्ध सेट सिद्धांत है, जिसमें पृष्ठभूमि तर्क होता है जिसमें पहचान (गणित) के साथ प्रथम-क्रम तर्क शामिल होता है, जिसमें प्रवचन का ब्रह्मांड पूरी तरह से सेट होता है। डिग्री 2 का एकल प्रथम-क्रम तर्क है, जिसे सेट सदस्यता के रूप में समझा जाता है। विहित स्वयंसिद्ध सेट सिद्धांत ZFC का PFL अनुवाद कठिन नहीं है, क्योंकि किसी भी ZFC स्वयंसिद्ध के लिए 6 से अधिक परिमाणित चर की आवश्यकता नहीं होती है।<ref>[http://us.metamath.org/mpegif/mmset.html#staxioms Metamath axioms.]</ref>
गणित का विहित आधार स्वयंसिद्ध समुच्चय सिद्धांत है, जिसमें पृष्ठभूमि तर्क होता है जिसमें पहचान (गणित) के साथ प्रथम-क्रम तर्क सम्मिलित होता है, जिसमें प्रवचन का ब्रह्मांड पूरी तरह से समुच्चय होता है। डिग्री 2 का एकल प्रथम-क्रम तर्क है, जिसे समुच्चय सदस्यता के रूप में समझा जाता है। इस प्रकार निहित स्वयंसिद्ध समुच्चय सिद्धांत जेडएफसी का पीएफएल अनुवाद कठिन नहीं है, क्योंकि किसी भी जेडएफसी स्वयंसिद्ध के लिए 6 से अधिक परिमाणित चर की आवश्यकता नहीं होती है।<ref>[http://us.metamath.org/mpegif/mmset.html#staxioms Metamath axioms.]</ref>
==यह भी देखें==
==यह भी देखें                                                                                                                                                                                                                                   ==
*[[बीजगणितीय तर्क]]
*[[बीजगणितीय तर्क]]


Line 171: Line 166:
==बाहरी संबंध==
==बाहरी संबंध==
* [http://stp.ling.uu.se/~matsd/pub/pfl.ps ''An introduction to predicate-functor logic''] (one-click download, PS file) by Mats Dahllöf (Department of Linguistics, Uppsala University)
* [http://stp.ling.uu.se/~matsd/pub/pfl.ps ''An introduction to predicate-functor logic''] (one-click download, PS file) by Mats Dahllöf (Department of Linguistics, Uppsala University)
[[Category: बीजगणितीय तर्क]] [[Category: गणितीय अभिगृहीत]] [[Category: विधेय तर्क]]


[[Category: Machine Translated Page]]
[[Category:Created On 07/07/2023]]
[[Category:Created On 07/07/2023]]
[[Category:Lua-based templates]]
[[Category:Machine Translated Page]]
[[Category:Pages with script errors]]
[[Category:Templates Vigyan Ready]]
[[Category:Templates that add a tracking category]]
[[Category:Templates that generate short descriptions]]
[[Category:Templates using TemplateData]]
[[Category:गणितीय अभिगृहीत]]
[[Category:बीजगणितीय तर्क]]
[[Category:विधेय तर्क]]

Latest revision as of 15:37, 31 July 2023

गणितीय तर्क में, विधेय फ़ंक्टर लॉजिक (पीएफएल) प्रथम-क्रम तर्क (जिसे विधेय तर्क के रूप में भी जाना जाता है) को विशुद्ध रूप से बीजगणितीय माध्यमों से व्यक्त करने के कई विधियों में से है, अर्थात, बिना परिमाणीकरण तर्क के पीएफएल कम संख्या में बीजगणितीय उपकरणों का उपयोग करता है जिन्हें विधेय फ़ैक्टर कहा जाता है (या विधेय संशोधक) [1] जो नियमो को प्राप्त करने के लिए नियमो पर कार्य करता है। पीएफएल अधिकतर तर्कशास्त्री और दार्शनिक विलार्ड क्वीन का आविष्कार है।

प्रेरणा

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

क्विन ने अपने मित्र रुडोल्फ कार्नाप के लेखन से फ़नक्टर लिया था, जो इसे दर्शन और गणितीय तर्क में नियोजित करने वाले पहले व्यक्ति थे, और इसे इस प्रकार परिभाषित किया था:

फ़ंक्टर शब्द, आयात में व्याकरणिक किन्तु निवास समिष्ट में तार्किक... संकेत है जो किसी दिए गए व्याकरणिक प्रकार की अभिव्यक्ति उत्पन्न करने के लिए दिए गए व्याकरणिक प्रकार के या अधिक अभिव्यक्तियों से जुड़ता है। (क्वीन 1982:129)प्रथम-क्रम तर्क को बीजगणित करने के पीएफएल के अतिरिक्त अन्य विधियों में सम्मिलित हैं:

  • अल्फ्रेड टार्स्की और उनके अमेरिकी छात्रों द्वारा बेलनाकार बीजगणित बर्नेज़ (1959) में प्रस्तावित सरलीकृत बेलनाकार बीजगणित ने क्विन को विधेय फ़ंक्टर वाक्यांश के पहले उपयोग वाले पेपर को लिखने के लिए प्रेरित किया था;
  • पॉल हेल्मोस का बहुपद बीजगणित अपने प्रभावकारी मौलिक और सिद्धांतों के आधार पर, यह बीजगणित पीएफएल से सबसे अधिक मिलता जुलता है;
  • संबंध बीजगणित प्रथम-क्रम तर्क के टुकड़े को बीजगणित करता है जिसमें तीन से अधिक परिमाणक (तर्क) के सीमा में कोई परमाणु सूत्र नहीं होने वाले सूत्र सम्मिलित होते हैं। चूँकि, वह टुकड़ा डोमेन अंकगणित और स्वयंसिद्ध समुच्चय सिद्धांत जेडएफसी के लिए पर्याप्त है; इसलिए संबंध बीजगणित, पीएफएल के विपरीत, गोडेल की अपूर्णता प्रमेय है। इस प्रकार 1920 के बाद से संबंध बीजगणित पर अधिकांश कार्य टार्स्की और उनके अमेरिकी छात्रों द्वारा किया गया है। संबंध बीजगणित की शक्ति तब तक प्रकट नहीं हुई जब तक कि पीएफएल पर आधारित तीन महत्वपूर्ण पत्रों, अर्थात् बेकन (1985), कुह्न (1983), और क्वीन (1976) के बाद प्रकाशित मोनोग्राफ टार्स्की और गिवंत (1987) द्वारा प्रस्तुत किया गया था;
  • संयोजक लॉजिक कॉम्बिनेटर्स पर बनता है, उच्च क्रम के फ़ंक्शन जिनके फ़ंक्शन का डोमेन अन्य कॉम्बिनेटर या फ़ंक्शन होता है, और जिनके फ़ंक्शन की सीमा और कॉम्बिनेटर होती है। इसलिए संयोजनात्मक तर्क समुच्चय सिद्धांत की अभिव्यंजक शक्ति के कारण प्रथम-क्रम तर्क से आगे निकल जाता है, जो संयोजनात्मक तर्क को विरोधाभास के प्रति संवेदनशील बनाता है। दूसरी ओर, विधेय फ़ंक्टर, केवल विधेय (जिसे टर्म (तर्क) भी कहा जाता है) को विधेय में बदल देता है।

पीएफएल वास्तविक इन औपचारिकताओं में सबसे सरल है, फिर भी ऐसा भी है जिसके बारे में सबसे कम लिखा गया है।

क्विन का संयोजनात्मक तर्क के प्रति आजीवन आकर्षण था, जिसका प्रमाण रूसी तर्कशास्त्री मोसेस शॉनफिंकेल द्वारा संयोजनात्मक तर्क की स्थापना करने वाले पेपर के वान हेजेनॉर्ट (1967) में अनुवाद के उनके परिचय से मिलता है। जब क्विन ने 1959 में पीएफएल पर गंभीरता से कार्य करना प्रारंभ किया था, जिससे संयोजन तर्क को सामान्यतः निम्नलिखित कारणों से विफल माना गया था:

  • 1960 के दशक के अंत में जब तक दाना स्कॉट ने संयोजन तर्क के मॉडल सिद्धांत पर लिखना प्रारंभ नहीं किया था, तब तक लगभग केवल हास्केल करी, उनके छात्र और बेल्जियम में रॉबर्ट फेयस ने ही उस तर्क पर कार्य किया था;
  • संयोजनात्मक तर्क के संतोषजनक स्वयंसिद्ध सूत्रीकरण आने में धीमे थे। इस प्रकार 1930 के दशक में, संयोजन तर्क के कुछ सूत्र संगतता प्रमाण पाए गए थे। करी ने करी विरोधाभास की भी खोज की थी, जो संयोजनात्मक तर्क की विशेषता है;
  • लैम्ब्डा कैलकुलस, संयोजन तर्क के समान अभिव्यंजक शक्ति के साथ, उत्तम औपचारिकता के रूप में देखा गया था।

कुह्न की निर्दिष्टीकरण

इस खंड में वर्णित पीएफएल वाक्यविन्यास, मौलिक और सिद्धांत अधिक सीमा तक स्टीवन कुह्न (1983) के हैं। इस प्रकार फ़ंक्शनलर्स के शब्दार्थ क्विन (1982) के हैं। इस प्रविष्टि के शेष भाग में बेकन (1985) की कुछ शब्दावली सम्मिलित है।

सिंटेक्स

एक परमाणु शब्द अपर केस लैटिन अक्षर है, I और S को छोड़कर, इसके बाद संख्यात्मक सुपरस्क्रिप्ट होती है जिसे इसकी डिग्री कहा जाता है, या संक्षिप्त लोअर केस वेरिएबल्स द्वारा, जिसे सामूहिक रूप से तर्क सूची के रूप में जाना जाता है। किसी पद की डिग्री विधेय अक्षर के बाद चरों की संख्या के समान ही जानकारी देती है। इस प्रकार डिग्री 0 का परमाणु शब्द बूलियन चर या सत्य मान को दर्शाता है। इस प्रकार I की डिग्री सदैव 2 होती है और इसलिए इसे दर्शाया नहीं गया है।

कॉम्बिनेटरी (शब्द क्वीन का है) विधेय फ़ैक्टर, पीएफएल के सभी मोनैडिक और विशिष्ट, 'इनव', 'इनव', '∃', '+' और 'p' हैं। शब्द या तो परमाणु शब्द है, या निम्नलिखित पुनरावर्ती नियम द्वारा निर्मित है। यदि τ पद है, तो 'Inv'τ, 'inv'τ, '∃'τ, '+'τ, और 'p'τ पद हैं। सुपरस्क्रिप्ट n, n प्राकृतिक संख्या > 1 वाला फ़ैक्टर, उस फ़ैक्टर के n निरंतर अनुप्रयोगों (पुनरावृत्तियों) को दर्शाता है।

सूत्र या तो शब्द है या पुनरावर्ती नियम द्वारा परिभाषित है: यदि α और β सूत्र हैं, तो αβ और ~(α) भी इसी तरह सूत्र हैं। इसलिए ~ अन्य मोनैडिक फ़ंक्टर है, और कॉन्सटेनेशन एकमात्र डायडिक विधेय फ़ैक्टर है। क्विन ने इन फ़ैक्टर्स को एलेथिक कहा ~ की स्वाभाविक व्याख्या निषेध है; संयोजन कोई भी तार्किक संयोजक है, जो निषेध के साथ संयुक्त होने पर संयोजकों का कार्यात्मक पूर्णता समुच्चय बनाता है। क्विन का रोचक कार्यात्मक पूर्ण समुच्चय तार्किक संयोजन और निषेध था। इस प्रकार संयोजित पदों को संयुक्त माना जाता है। अंकन '+' बेकन (1985) का है; अन्य सभी संकेतन क्वीन (1976; 1982) के हैं। पीएफएल का एलेथिक भाग क्वीन (1982) के बूलियन शब्द स्कीमाटा के समान है।

जैसा कि सर्वविदित है, दो एलेथिक फ़ंक्टर को निम्नलिखित सिंटैक्स और शब्दार्थ के साथ एकल डायडिक फ़ैक्टर द्वारा प्रतिस्थापित किया जा सकता है: यदि α और β सूत्र हैं, तो (αβ) ऐसा सूत्र है जिसका शब्दार्थ (α और/या β) नहीं है ( शेफ़र लाइन और लॉजिकल NOR देखें)।

सिद्धांत और शब्दार्थ

क्विन ने पीएफएल के लिए न तो स्वयंसिद्धीकरण और न ही प्रमाण प्रक्रिया निर्धारित की थी। पीएफएल का निम्नलिखित स्वयंसिद्धीकरण, कुह्न (1983) में प्रस्तावित दो में से एक, संक्षिप्त और वर्णन करने में सरल है, किन्तु मुक्त चर का व्यापक उपयोग करता है और इसलिए पीएफएल की भावना के साथ पूर्ण न्याय नहीं करता है। कुह्न मुक्त चर के साथ और स्वयंसिद्धीकरण प्रदान करता है, किन्तु इसका वर्णन करना कठिन है और यह परिभाषित फ़ंक्शनलर्स का व्यापक उपयोग करता है। कुह्न ने अपने पीएफएल स्वयंसिद्धीकरण स्थिरता प्रमाण और पूर्णता (तर्क) दोनों को सिद्ध किया था।

यह खंड मौलिक विधेय फ़ैक्टर और कुछ परिभाषित फ़ैक्टरों के आसपास बनाया गया है। एलेथिक फ़ैक्टर्स को भावनात्मक तर्क के लिए सिद्धांतों के किसी भी समुच्चय द्वारा स्वयंसिद्ध किया जा सकता है जिनके मौलिक निषेध हैं और ∧ या ∨ में से हैं। समान रूप से, भावनात्मक तर्क की सभी तनातनी (तर्क) को स्वयंसिद्धों के रूप में लिया जा सकता है।

प्रत्येक विधेय फ़ैक्टर के लिए क्विन (1982) के शब्दार्थ को अमूर्तन (सेट बिल्डर नोटेशन) के संदर्भ में नीचे बताया गया है, इसके बाद या तो कुह्न (1983) से संबंधित स्वयंसिद्ध कथन, या क्विन (1976) से परिभाषा दी गई है। संकेतन परमाणु सूत्र को संतुष्ट करने वाले n-ट्यूपल के समुच्चय को दर्शाता है

  • पहचान, I, परिभाषित किया जाता है:

पहचान प्रतिवर्ती संबंध है (Ixx), सममित (IxyIyx), सकर्मक संबंध ((IxyIyz) → Ixz), और प्रतिस्थापन गुण का पालन करता है:

  • पैडिंग, '+', किसी भी तर्क सूची के बाईं ओर वेरिएबल जोड़ता है।
  • क्रॉपिंग, '∃', किसी भी तर्क सूची में सबसे बाएं वेरिएबल को मिटा देता है।

क्रॉपिंग दो उपयोगी परिभाषित फ़ंक्शनलर्स को सक्षम बनाता है:

  • प्रतिबिंब, 'एस':

एस 2 से अधिक किसी भी परिमित डिग्री के सभी शब्दों के प्रति संवेदनशीलता की धारणा को सामान्यीकृत करता है। एन.बी.: एस को संयोजन तर्क के संयोजन तर्क एस के साथ भ्रमित नहीं किया जाना चाहिए।

केवल यहीं पर, क्विन ने इन्फ़िक्स नोटेशन को अपनाया था, क्योंकि कार्टेशियन उत्पाद के लिए यह इन्फ़िक्स नोटेशन गणित में बहुत अच्छी तरह से स्थापित है। कार्टेशियन उत्पाद निम्नानुसार संयोजन को पुनः स्थापित करने की अनुमति देता है:

संयोजित तर्क सूची को पुन: व्यवस्थित करें जिससे डुप्लिकेट चर की जोड़ी को सबसे बाईं ओर समिष्टांतरित किया जा सकता है, फिर डुप्लिकेशन को समाप्त करने के लिए एस को आमंत्रित करें। इसे आवश्यकतानुसार कई बार दोहराने से अधिकतम लंबाई (m,n) की तर्क सूची प्राप्त होती है।

अगले तीन फ़ैक्टर इच्छानुसार तर्क सूचियों को पुन: व्यवस्थित करने में सक्षम बनाते हैं।

  • प्रमुख व्युत्क्रम, इनव, तर्क सूची में चरों को दाईं ओर घुमाता है, जिससे अंतिम चर पहला बन जाए।
  • लघु व्युत्क्रम, 'इनव', तर्क सूची में पहले दो चरों की अदला-बदली करता है।
  • क्रमपरिवर्तन, 'p', तर्क सूची में दूसरे से अंतिम चर को बाईं ओर घुमाता है, जिससे दूसरा चर अंतिम बन जाता है।

n चरों से युक्त तर्क सूची को देखते हुए, 'p' स्पष्ट रूप से अंतिम n−1 चर को साइकिल श्रृंखला की तरह मानता है, जिसमें प्रत्येक चर श्रृंखला में लिंक बनाता है। 'p' का अनुप्रयोग श्रृंखला को लिंक से आगे बढ़ाता है। k से F तक 'pn' का निरंतर अनुप्रयोग k+1 वेरिएबल को F में दूसरे तर्क समिष्ट पर ले जाता है।

जब n=2, 'Inv' और 'inv' केवल x1 और x2 का आदान-प्रदान करते हैं. जब n=1, उनका कोई प्रभाव नहीं पड़ता है। अतः n <3 होने पर 'p' का कोई प्रभाव नहीं पड़ता है।

कुह्न (1983) प्रमुख व्युत्क्रम और लघु व्युत्क्रम को मौलिक मानते हैं। कुह्न में अंकन 'p' 'inv' से मेल खाता है; उसके पास क्रमपरिवर्तन का कोई एनालॉग नहीं है और इसलिए उसके पास इसके लिए कोई सिद्धांत नहीं है। यदि, क्वीन (1976) के बाद, 'p' को मौलिक के रूप में लिया जाता है, तो 'इनव' और 'इनव' को '+', '∃' और पुनरावृत्त 'p' के सामान्य संयोजन के रूप में परिभाषित किया जा सकता है।

निम्न तालिका सारांशित करती है कि फ़ंक्शनलर्स अपने तर्कों की डिग्री को कैसे प्रभावित करते हैं।

अभिव्यक्ति डिग्री
no change
n
max(m, n)

नियम

वैधता को प्रभावित किए बिना, विधेय पत्र के सभी उदाहरणों को उसी डिग्री के किसी अन्य विधेय पत्र द्वारा प्रतिस्थापित किया जा सकता है। प्रथम-क्रम तर्क हैं:

  • एक वैध, सरल तर्क और निष्कर्ष के नियम के रूप;
  • मान लीजिए α और β पीएफएल सूत्र हैं जिनमें प्रकट नहीं होता है। तो यदि तो फिर, यह पीएफएल प्रमेय है इसी तरह पीएफएल प्रमेय है।

कुछ उपयोगी परिणाम

पीएफएल को स्वयंसिद्ध करने के अतिरिक्त, क्वीन (1976) ने निम्नलिखित अनुमानों को उम्मीदवार स्वयंसिद्ध के रूप में प्रस्तावित किया था।

'p' का n−1 निरंतर पुनरावृत्ति यथास्थिति बहाल करता है:

+ और ∃ दूसरे को नष्ट करें:

निषेध +, ∃, और p पर वितरित होता है:

+ और p संयोजन पर वितरित करता है:

पहचान का रोचक निहितार्थ है:

क्विन ने नियम का भी अनुमान लगाया: यदि α पीएफएल प्रमेय है, तो ऐसा , +α, और ही है.

बेकन का कार्य

बेकन (1985) पदार्थ नियमबद्ध, नेगेशन, आइडेंटिटी, पैडिंग और मेजर और माइनर व्युत्क्रम को मौलिक और क्रॉपिंग को परिभाषित मानता है। उपरोक्त से कुछ भिन्न शब्दावली और संकेतन का उपयोग करते हुए, बेकन (1985) ने पीएफएल के दो सूत्र प्रस्तुत किए:

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

बेकन भी:

  • सोमरस (1982) के शब्द तर्क के साथ पीएफएल के संबंध पर चर्चा करता है, और तर्क देता है कि लॉकवुड के सोमरस के परिशिष्ट में प्रस्तावित वाक्यविन्यास का उपयोग करके पीएफएल को पुनर्गठित करने से पीएफएल को पढ़ना, उपयोग करना और पढ़ाना सरल हो जाना चाहिए;
  • 'इन्व' और 'इन्व' की समूह सिद्धांत संरचना स्पर्श करता है;
  • उल्लेख है कि भावनात्मक तर्क, मोनैडिक विधेय तर्क, मोडल तर्क S5 (मोडल लॉजिक), और परम्यूटेड सम्बन्ध (गणित) के बूलियन लॉजिक, सभी पीएफएल के टुकड़े हैं।

प्रथम-क्रम तर्क से पीएफएल तक

निम्नलिखित कलन विधि को क्वीन (1976: 300-2) से अनुकूलित किया गया है। प्रथम-क्रम तर्क के वाक्य (गणितीय तर्क) को देखते हुए, पहले निम्नलिखित कार्य करें:

अब पूर्ववर्ती परिणाम पर निम्नलिखित एल्गोरिदम प्रयुक्त करें:

  1. सबसे गहराई से निहित क्वांटिफायर के आव्यूहों का अनुवाद डिजजंक्टिव सामान्य रूप में करें, जिसमें डिजंक्ट्स के संयुक्त पद सम्मिलित हों, आवश्यकतानुसार परमाणु शब्दों को अस्वीकार। परिणामी उपसूत्र में केवल निषेध, संयोजन, विच्छेदन और अस्तित्वगत परिमाणीकरण सम्मिलित है।
  2. मार्ग के नियम का उपयोग करके आव्यूह में विच्छेदों पर अस्तित्व संबंधी परिमाणकों को वितरित करें (क्विन 1982: 119):
  3. तथ्य का उपयोग करके संयोजन को कार्टेशियन उत्पाद से बदलें:
  4. सभी परमाणु शब्दों की तर्क सूचियों को संयोजित करें, और संयोजित सूची को उपसूत्र के सबसे दाईं ओर ले जाएँ।
  5. परिमाणित चर के सभी उदाहरणों (इसे y कहें) को तर्क सूची के बाईं ओर ले जाने के लिए Inv' और inv का उपयोग करें।
  6. Y के अंतिम उदाहरण को छोड़कर सभी को हटाने के लिए जितनी बार आवश्यक हो S का उपयोग करें। के एक उदाहरण के साथ उपसूत्र को उपसर्ग करके y को हटा दें।
  7. (1)-(6) को तब तक दोहराएँ जब तक कि सभी परिमाणित चर समाप्त न हो जाएँ। समतुल्यता का आह्वान करके परिमाणक के सीमा में आने वाले किसी भी वियोजन को हटा दें:

पीएफएल से प्रथम-क्रम तर्क तक रिवर्स अनुवाद पर क्विन (1976: 302-4) में चर्चा की गई है।

गणित का विहित आधार स्वयंसिद्ध समुच्चय सिद्धांत है, जिसमें पृष्ठभूमि तर्क होता है जिसमें पहचान (गणित) के साथ प्रथम-क्रम तर्क सम्मिलित होता है, जिसमें प्रवचन का ब्रह्मांड पूरी तरह से समुच्चय होता है। डिग्री 2 का एकल प्रथम-क्रम तर्क है, जिसे समुच्चय सदस्यता के रूप में समझा जाता है। इस प्रकार निहित स्वयंसिद्ध समुच्चय सिद्धांत जेडएफसी का पीएफएल अनुवाद कठिन नहीं है, क्योंकि किसी भी जेडएफसी स्वयंसिद्ध के लिए 6 से अधिक परिमाणित चर की आवश्यकता नहीं होती है।[2]

यह भी देखें

फ़ुटनोट

  1. Johannes Stern, Toward Predicate Approaches to Modality, Springer, 2015, p. 11.
  2. Metamath axioms.

संदर्भ

  • Bacon, John, 1985, "The completeness of a predicate-functor logic," Journal of Symbolic Logic 50: 903–26.
  • Paul Bernays, 1959, "Uber eine naturliche Erweiterung des Relationenkalkuls" in Heyting, A., ed., Constructivity in Mathematics. North Holland: 1–14.
  • Kuhn, Steven T., 1983, "An Axiomatization of Predicate Functor Logic," Notre Dame Journal of Formal Logic 24: 233–41.
  • Willard Quine, 1976, "Algebraic Logic and Predicate Functors" in Ways of Paradox and Other Essays, enlarged ed. Harvard Univ. Press: 283–307.
  • Willard Quine, 1982. Methods of Logic, 4th ed. Harvard Univ. Press. Chpt. 45.
  • Sommers, Fred, 1982. The Logic of Natural Language. Oxford Univ. Press.
  • Alfred Tarski and Givant, Steven, 1987. A Formalization of Set Theory Without Variables. AMS.
  • Jean Van Heijenoort, 1967. From Frege to Gödel: A Source Book on Mathematical Logic. Harvard Univ. Press.

बाहरी संबंध