विधेय फ़ंक्टर तर्क

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

प्रेरणा

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

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

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

प्रथम-क्रम तर्क को बीजगणित करने के पीएफएल के अलावा अन्य तरीकों में शामिल हैं:

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

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

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

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

कुह्न की औपचारिकता

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

सिंटेक्स

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

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

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

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

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

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

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

प्रत्येक विधेय फ़ैक्टर के लिए क्विन (1982) के शब्दार्थ को अमूर्तन (सेट बिल्डर नोटेशन) के संदर्भ में नीचे बताया गया है, इसके बाद या तो कुह्न (1983) से संबंधित स्वयंसिद्ध कथन, या क्विन (1976) से परिभाषा दी गई है। संकेतन $\{x_{1}\cdots x_{n}:Fx_{1}\cdots x_{n}\}$ परमाणु सूत्र को संतुष्ट करने वाले n-tuple|n-tuples के समुच्चय को दर्शाता है $Fx_{1}\cdots x_{n}.$

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

$IFx_{1}x_{2}\cdots x_{n}\leftrightarrow (Fx_{1}x_{1}\cdots x_{n}\leftrightarrow Fx_{2}x_{2}\cdots x_{n}){\text{.}}$

पहचान प्रतिवर्ती संबंध है (Ixx), सममित (Ixy→Iyx), सकर्मक संबंध ((Ixy∧Iyz) → Ixz), और प्रतिस्थापन संपत्ति का पालन करता है:

$(Fx_{1}\cdots x_{n}\land Ix_{1}y)\rightarrow Fyx_{2}\cdots x_{n}.$

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

$\ +F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{0}x_{1}\cdots x_{n}:F^{n}x_{1}\cdots x_{n}\}.$

$+Fx_{1}\cdots x_{n}\leftrightarrow Fx_{2}\cdots x_{n}.$

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

$\exists F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{2}\cdots x_{n}:\exists x_{1}F^{n}x_{1}\cdots x_{n}\}.$

$Fx_{1}\cdots x_{n}\rightarrow \exists Fx_{2}\cdots x_{n}.$

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

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

$SF^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{2}\cdots x_{n}:F^{n}x_{2}x_{2}\cdots x_{n}\}.$

$SF^{n}\leftrightarrow \exists IF^{n}.$

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

• कार्तीय गुणन, $\times$;

$F^{m}\times G^{n}\leftrightarrow F^{m}\exists ^{m}G^{n}.$ केवल यहीं पर, क्विन ने इन्फ़िक्स नोटेशन को अपनाया, क्योंकि कार्टेशियन उत्पाद के लिए यह इन्फ़िक्स नोटेशन गणित में बहुत अच्छी तरह से स्थापित है। कार्टेशियन उत्पाद निम्नानुसार संयोजन को पुनः स्थापित करने की अनुमति देता है:

$F^{m}x_{1}\cdots x_{m}G^{n}x_{1}\cdots x_{n}\leftrightarrow (F^{m}\times G^{n})x_{1}\cdots x_{m}x_{1}\cdots x_{n}.$

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

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

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

$\operatorname {Inv} F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{n}x_{1}\cdots x_{n-1}\}.$

$\operatorname {Inv} Fx_{1}\cdots x_{n}\leftrightarrow Fx_{n}x_{1}\cdots x_{n-1}.$

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

$\operatorname {inv} F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{2}x_{1}\cdots x_{n}\}.$

$\operatorname {inv} Fx_{1}\cdots x_{n}\leftrightarrow Fx_{2}x_{1}\cdots x_{n}.$

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

$\ pF^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{1}x_{3}\cdots x_{n}x_{2}\}.$

$pFx_{1}\cdots x_{n}\leftrightarrow \operatorname {Inv} \operatorname {inv} Fx_{1}x_{3}\cdots x_{n}x_{2}.$

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

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

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

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

Expression	Degree
$p;\operatorname {Inv} ;\operatorname {inv} ;\ \lnot ;\ I$	no change
$+F^{n-1};\ \exists F^{n+1};\ SF^{n+1}$	n
$\alpha ^{m}\beta ^{n};\ F^{m}\times G^{n}$	max(m, n)

नियम

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

• एक वैध, सरल तर्क और निष्कर्ष के नियम के रूप;
• मान लीजिए α और β पीएफएल सूत्र हैं जिनमें $x_{1}$ प्रकट नहीं होता है। तो अगर $(\alpha \land Fx_{1}...x_{n})\rightarrow \beta$ तो फिर, यह पीएफएल प्रमेय है $(\alpha \land \exists Fx_{2}...x_{n})\rightarrow \beta$ इसी तरह पीएफएल प्रमेय है।

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

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

$\exists I$

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

$F^{n}\leftrightarrow p^{n-1}F^{n}$

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

${\begin{cases}F^{n}\rightarrow +\exists F^{n}\\F^{n}\leftrightarrow \exists +F^{n}\end{cases}}$

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

${\begin{cases}+\lnot F^{n}\leftrightarrow \lnot +F^{n}\\\lnot \exists F^{n}\rightarrow \exists \lnot F^{n}\\p\lnot F^{n}\leftrightarrow \lnot pF^{n}\end{cases}}$

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

${\begin{cases}+(F^{n}G^{m})\leftrightarrow (+F^{n}+G^{m})\\p(F^{n}G^{m})\leftrightarrow (pF^{n}pG^{m})\end{cases}}$

पहचान का दिलचस्प निहितार्थ है:

$IF^{n}\rightarrow p^{n-2}\exists p+F^{n}$

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

बेकन का कार्य

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

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

बेकन भी:

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

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

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

• प्रत्येक विधेय अक्षर के साथ उसकी डिग्री बताते हुए संख्यात्मक सबस्क्रिप्ट संलग्न करें;
• सभी सार्वभौमिक परिमाणकों का अस्तित्वगत परिमाणकों और निषेध में अनुवाद करें;
• x=y रूप के सभी परमाणु सूत्रों को Ixy के रूप में पुनः स्थापित करें।

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

1. Translate the matrices of the most deeply nested quantifiers into disjunctive normal form, consisting of disjuncts of conjuncts of terms, negating atomic terms as required. The resulting subformula contains only negation, conjunction, disjunction, and existential quantification.
2. Distribute the existential quantifiers over the disjuncts in the matrix using the rule of passage (Quine 1982: 119):

   $\exists x[\alpha (x)\lor \gamma (x)]\leftrightarrow (\exists x\alpha (x)\lor \exists x\gamma (x)).$

3. Replace conjunction by Cartesian product, by invoking the fact:
   $(F^{m}\land G^{n})\leftrightarrow (F^{m}\times G^{n})\leftrightarrow (F^{m}\exists ^{m}G^{n});m<n.$
4. Concatenate the argument lists of all atomic terms, and move the concatenated list to the far right of the subformula.
5. Use Inv and inv to move all instances of the quantified variable (call it y) to the left of the argument list.
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 ∃.
7. Repeat (1)-(6) until all quantified variables have been eliminated. Eliminate any disjunctions falling within the scope of a quantifier by invoking the equivalence:
   $(\alpha \lor \beta \lor ...)\leftrightarrow \lnot (\lnot \alpha \land \lnot \beta \land ...).$

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

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

यह भी देखें

• बीजगणितीय तर्क

संदर्भ

• 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.

बाहरी संबंध

• An introduction to predicate-functor logic (one-click download, PS file) by Mats Dahllöf (Department of Linguistics, Uppsala University)