प्रीनेक्स सामान्य रूप: Difference between revisions

From Vigyanwiki
No edit summary
No edit summary
Line 1: Line 1:
{{Short description|Formalism of first-order logic}}
{{Short description|Formalism of first-order logic}}
[[विधेय कलन]] का [[सूत्र (गणितीय तर्क)]] प्रीनेक्स में है<ref>The term 'prenex' comes from the [[Latin]] ''praenexus'' "tied or bound up in front", past participle of ''praenectere'' [http://cs.nyu.edu/pipermail/fom/2007-November/012328.html] (archived as of May 27, 2011 at [https://web.archive.org/web/20110527102347/http://cs.nyu.edu/pipermail/fom/2007-November/012328.html])</ref> [[सामान्य रूप (सार पुनर्लेखन)]] (पीएनएफ) यदि यह [[ परिमाणक (तर्क) |परिमाणक (तर्क)]] और [[ बाध्य चर |बाध्य चर]] की स्ट्रिंग के रूप में रीराइटिंग # लॉजिक है, जिसे उपसर्ग कहा जाता है, इसके पश्चात् क्वांटिफायर-मुक्त भाग होता है, जिसे मैट्रिक्स कहा जाता है।<ref>Hinman, P. (2005), p. 110</ref> [[प्रस्तावात्मक कलन]] (उदाहरण के लिए [[विच्छेदात्मक सामान्य रूप]] या [[ संयोजक सामान्य रूप |संयोजक सामान्य रूप]] ) में सामान्य रूपों के साथ, यह स्वचालित प्रमेय साबित करने में उपयोगी [[विहित सामान्य रूप]] प्रदान करता है।
[[विधेय कलन]] का [[सूत्र (गणितीय तर्क)]] प्रीनेक्स में है<ref>The term 'prenex' comes from the [[Latin]] ''praenexus'' "tied or bound up in front", past participle of ''praenectere'' [http://cs.nyu.edu/pipermail/fom/2007-November/012328.html] (archived as of May 27, 2011 at [https://web.archive.org/web/20110527102347/http://cs.nyu.edu/pipermail/fom/2007-November/012328.html])</ref> [[सामान्य रूप (सार पुनर्लेखन)]] (पीएनएफ) यदि यह [[ परिमाणक (तर्क) |परिमाणक (तर्क)]] और [[ बाध्य चर |बाध्य चर]] की स्ट्रिंग के रूप में रीराइटिंग # लॉजिक है, जिसे उपसर्ग कहा जाता है, इसके पश्चात् क्वांटिफायर-मुक्त भाग होता है, जिसे मैट्रिक्स कहा जाता है।<ref>Hinman, P. (2005), p. 110</ref> [[प्रस्तावात्मक कलन]] (उदाहरण के लिए [[विच्छेदात्मक सामान्य रूप]] या [[ संयोजक सामान्य रूप |संयोजक सामान्य रूप]] ) में सामान्य रूपों के साथ, यह स्वचालित प्रमेय सिद्ध करना  करने में उपयोगी [[विहित सामान्य रूप]] प्रदान करता है।


[[शास्त्रीय तर्क]] में प्रत्येक सूत्र तार्किक रूप से प्रीनेक्स सामान्य रूप में सूत्र के सामान्तर है। उदाहरण के लिए, यदि <math>\phi(y)</math>, <math>\psi(z)</math>, और <math>\rho(x)</math> तब दिखाए गए मुक्त चर के साथ क्वांटिफायर-मुक्त सूत्र हैं
[[शास्त्रीय तर्क|मौलिक  तर्क]] में प्रत्येक सूत्र तार्किक रूप से प्रीनेक्स सामान्य रूप में सूत्र के सामान्तर है। उदाहरण के लिए, यदि <math>\phi(y)</math>, <math>\psi(z)</math>, और <math>\rho(x)</math> तब दिखाए गए मुक्त चर के साथ क्वांटिफायर-मुक्त सूत्र हैं
:<math>\forall x \exists y \forall z (\phi(y) \lor (\psi(z) \rightarrow \rho(x)))</math>
:<math>\forall x \exists y \forall z (\phi(y) \lor (\psi(z) \rightarrow \rho(x)))</math>
मैट्रिक्स के साथ प्रीनेक्स सामान्य रूप में है <math>\phi(y) \lor (\psi(z) \rightarrow \rho(x))</math>, जबकि
मैट्रिक्स के साथ प्रीनेक्स सामान्य रूप में है <math>\phi(y) \lor (\psi(z) \rightarrow \rho(x))</math>, जबकि
:<math>\forall x ((\exists y \phi(y)) \lor ((\exists z \psi(z) ) \rightarrow \rho(x)))</math>
:<math>\forall x ((\exists y \phi(y)) \lor ((\exists z \psi(z) ) \rightarrow \rho(x)))</math>
तार्किक रूप से समतुल्य है लेकिन प्रीनेक्स सामान्य रूप में नहीं।
तार्किक रूप से समतुल्य है किन्तु प्रीनेक्स सामान्य रूप में नहीं।


== प्रीनेक्स फॉर्म में रूपांतरण ==
== प्रीनेक्स फॉर्म में रूपांतरण ==
प्रत्येक [[प्रथम-क्रम विधेय कलन]]|प्रथम-क्रम सूत्र तार्किक रूप से (शास्त्रीय तर्क में) प्रीनेक्स सामान्य रूप में कुछ सूत्र के सामान्तर है।<ref>Hinman, P. (2005), p. 111</ref> ऐसे अनेक रूपांतरण नियम हैं जिन्हें किसी सूत्र को प्रीनेक्स सामान्य रूप में परिवर्तित करने के लिए पुनरावर्ती रूप से क्रियान्वित किया जा सकता है। नियम इस पर निर्भर करते हैं कि सूत्र में कौन से [[तार्किक संयोजक]] दिखाई देते हैं।
प्रत्येक [[प्रथम-क्रम विधेय कलन]]|प्रथम-क्रम सूत्र तार्किक रूप से (मौलिक  तर्क में) प्रीनेक्स सामान्य रूप में कुछ सूत्र के सामान्तर है।<ref>Hinman, P. (2005), p. 111</ref> ऐसे अनेक रूपांतरण नियम हैं जिन्हें किसी सूत्र को प्रीनेक्स सामान्य रूप में परिवर्तित करने के लिए पुनरावर्ती रूप से क्रियान्वित किया जा सकता है। नियम इस पर निर्भर करते हैं कि सूत्र में कौन से [[तार्किक संयोजक]] दिखाई देते हैं।


=== संधि और विच्छेद ===
=== संधि और विच्छेद ===


[[तार्किक संयोजन]] और तार्किक वियोजन के नियम यही कहते हैं
[[तार्किक संयोजन]] और तार्किक वियोजन के नियम यही कहते हैं
:<math>(\forall x \phi) \land \psi</math> के सामान्तर है <math>\forall x ( \phi \land \psi)</math> (हल्के) अतिरिक्त शर्त के तहत <math>\exists x \top</math>, या, समकक्ष, <math>\lnot\forall x \bot</math> (मतलब कि कम से कम व्यक्ति मौजूद है),
:<math>(\forall x \phi) \land \psi</math> के सामान्तर है <math>\forall x ( \phi \land \psi)</math> (हल्के) अतिरिक्त शर्त के अनुसार  <math>\exists x \top</math>, या, समकक्ष, <math>\lnot\forall x \bot</math> (कारणकि कम से कम व्यक्ति उपस्तिथ है),
:<math>(\forall x \phi) \lor \psi</math> के सामान्तर है <math>\forall x ( \phi \lor \psi)</math>;
:<math>(\forall x \phi) \lor \psi</math> के सामान्तर है <math>\forall x ( \phi \lor \psi)</math>;
और
और
:<math>(\exists x \phi) \land \psi</math> के सामान्तर है <math>\exists x (\phi \land \psi)</math>,
:<math>(\exists x \phi) \land \psi</math> के सामान्तर है <math>\exists x (\phi \land \psi)</math>,
:<math>(\exists x \phi) \lor \psi</math> के सामान्तर है <math>\exists x (\phi \lor \psi)</math> अतिरिक्त शर्त के तहत <math>\exists x \top</math>.
:<math>(\exists x \phi) \lor \psi</math> के सामान्तर है <math>\exists x (\phi \lor \psi)</math> अतिरिक्त शर्त के अनुसार  <math>\exists x \top</math>.
समतुल्यताएँ तब मान्य होती हैं जब <math>x</math> के [[मुक्त चर]] के रूप में प्रकट नहीं होता है <math>\psi</math>; अगर <math>x</math> में मुक्त दिखाई देता है <math>\psi</math>, कोई बाउंड का नाम बदल सकता है <math>x</math> में <math>(\exists x \phi)</math> और समतुल्य प्राप्त करें <math>(\exists x' \phi[x/x'])</math>.
समतुल्यताएँ तब मान्य होती हैं जब <math>x</math> के [[मुक्त चर]] के रूप में प्रकट नहीं होता है <math>\psi</math>; अगर <math>x</math> में मुक्त दिखाई देता है <math>\psi</math>, कोई बाउंड का नाम बदल सकता है <math>x</math> में <math>(\exists x \phi)</math> और समतुल्य प्राप्त करें <math>(\exists x' \phi[x/x'])</math>.


उदाहरण के लिए, रिंग (गणित) की भाषा में,
उदाहरण के लिए, रिंग (गणित) की भाषा में,
:<math>(\exists x (x^2 = 1)) \land (0 = y)</math> के सामान्तर है <math>\exists x ( x^2 = 1 \land 0 = y)</math>,
:<math>(\exists x (x^2 = 1)) \land (0 = y)</math> के सामान्तर है <math>\exists x ( x^2 = 1 \land 0 = y)</math>,
लेकिन
किन्तु
:<math>(\exists x (x^2 = 1)) \land (0 = x)</math> के सामान्तर नहीं है <math>\exists x ( x^2 = 1 \land 0 = x)</math>
:<math>(\exists x (x^2 = 1)) \land (0 = x)</math> के सामान्तर नहीं है <math>\exists x ( x^2 = 1 \land 0 = x)</math>
क्योंकि बाईं ओर का सूत्र किसी भी रिंग में सत्य है जब मुक्त चर x 0 के सामान्तर है, जबकि दाईं ओर के सूत्र में कोई मुक्त चर नहीं है और किसी भी गैर-तुच्छ रिंग में गलत है। इसलिए <math>(\exists x (x^2 = 1)) \land (0 = x)</math> पहले के रूप में पुनः लिखा जाएगा <math>(\exists x' (x'^2 = 1)) \land (0 = x)</math> और फिर प्रीनेक्स को सामान्य रूप में डाल दें <math>\exists x' ( x'^2 = 1 \land 0 = x)</math>.
क्योंकि बाईं ओर का सूत्र किसी भी रिंग में सत्य है जब मुक्त चर x 0 के सामान्तर है, जबकि दाईं ओर के सूत्र में कोई मुक्त चर नहीं है और किसी भी गैर-तुच्छ रिंग में गलत है। इसलिए <math>(\exists x (x^2 = 1)) \land (0 = x)</math> पहले के रूप में पुनः लिखा जाएगा <math>(\exists x' (x'^2 = 1)) \land (0 = x)</math> और फिर प्रीनेक्स को सामान्य रूप में डाल दें <math>\exists x' ( x'^2 = 1 \land 0 = x)</math>.
Line 39: Line 39:


पूर्ववर्ती से परिमाणकों को हटाने के नियम हैं (परिमाणकों के परिवर्तन पर ध्यान दें):
पूर्ववर्ती से परिमाणकों को हटाने के नियम हैं (परिमाणकों के परिवर्तन पर ध्यान दें):
:<math>(\forall x \phi ) \rightarrow \psi</math> के सामान्तर है <math>\exists x (\phi \rightarrow \psi)</math> (इस धारणा के तहत <math>\exists x \top</math>),
:<math>(\forall x \phi ) \rightarrow \psi</math> के सामान्तर है <math>\exists x (\phi \rightarrow \psi)</math> (इस धारणा के अनुसार  <math>\exists x \top</math>),
:<math>(\exists x \phi ) \rightarrow \psi</math> के सामान्तर है <math>\forall x (\phi \rightarrow \psi)</math>.
:<math>(\exists x \phi ) \rightarrow \psi</math> के सामान्तर है <math>\forall x (\phi \rightarrow \psi)</math>.
परिणामी से परिमाणक हटाने के नियम हैं:
परिणामी से परिमाणक हटाने के नियम हैं:
:<math>\phi \rightarrow (\exists x \psi)</math> के सामान्तर है <math>\exists x (\phi \rightarrow \psi)</math> (इस धारणा के तहत <math>\exists x \top</math>),
:<math>\phi \rightarrow (\exists x \psi)</math> के सामान्तर है <math>\exists x (\phi \rightarrow \psi)</math> (इस धारणा के अनुसार  <math>\exists x \top</math>),
:<math>\phi \rightarrow (\forall x \psi)</math> के सामान्तर है <math>\forall x (\phi \rightarrow \psi)</math>.
:<math>\phi \rightarrow (\forall x \psi)</math> के सामान्तर है <math>\forall x (\phi \rightarrow \psi)</math>.
उदाहरण के लिए, जब [[परिमाणीकरण की सीमा]] गैर-ऋणात्मक [[प्राकृतिक संख्या]] है (अर्थात। <math>n\in \mathbb{N}</math>), कथन
उदाहरण के लिए, जब [[परिमाणीकरण की सीमा]] गैर-ऋणात्मक [[प्राकृतिक संख्या]] है (अर्थात। <math>n\in \mathbb{N}</math>), कथन
Line 48: Line 48:
तार्किक रूप से कथन के समतुल्य है
तार्किक रूप से कथन के समतुल्य है
:<math>\exists n\in \mathbb{N}[ (x< n)  \rightarrow (x< 0)]</math>
:<math>\exists n\in \mathbb{N}[ (x< n)  \rightarrow (x< 0)]</math>
पहला कथन कहता है कि यदि x किसी प्राकृत संख्या से कम है, तब x शून्य से भी कम है। पश्चात् वाला कथन कहता है कि कुछ प्राकृतिक संख्या n मौजूद है जैसे कि यदि x, n से कम है, तब x शून्य से भी कम है। दोनों कथन सत्य हैं। पहला कथन सत्य है क्योंकि यदि x किसी प्राकृत संख्या से कम है, तब उसे सबसे छोटी प्राकृत संख्या (शून्य) से भी कम होना चाहिए। पश्चात् वाला कथन सत्य है क्योंकि n=0 निहितार्थ को [[टॉटोलॉजी (तर्क)]] बनाता है।
पहला कथन कहता है कि यदि x किसी प्राकृत संख्या से कम है, तब x शून्य से भी कम है। पश्चात् वाला कथन कहता है कि कुछ प्राकृतिक संख्या n उपस्तिथ है जैसे कि यदि x, n से कम है, तब x शून्य से भी कम है। दोनों कथन सत्य हैं। पहला कथन सत्य है क्योंकि यदि x किसी प्राकृत संख्या से कम है, तब उसे सबसे छोटी प्राकृत संख्या (शून्य) से भी कम होना चाहिए। पश्चात् वाला कथन सत्य है क्योंकि n=0 निहितार्थ को [[टॉटोलॉजी (तर्क)]] बनाता है।


ध्यान दें कि कोष्ठक का स्थान स्कोप (तर्क) को दर्शाता है, जो सूत्र के अर्थ के लिए बहुत महत्वपूर्ण है। निम्नलिखित दो कथनों पर विचार करें:
ध्यान दें कि कोष्ठक का स्थान स्कोप (तर्क) को दर्शाता है, जो सूत्र के अर्थ के लिए बहुत महत्वपूर्ण है। निम्नलिखित दो कथनों पर विचार करें:
Line 54: Line 54:
और इसका तार्किक रूप से समतुल्य कथन
और इसका तार्किक रूप से समतुल्य कथन
:<math>[\exists n\in \mathbb{N} (x< n) ] \rightarrow (x< 0)</math>
:<math>[\exists n\in \mathbb{N} (x< n) ] \rightarrow (x< 0)</math>
पहला कथन कहता है कि किसी भी प्राकृतिक संख्या n के लिए, यदि x, n से कम है तब x शून्य से कम है। पश्चात् वाला कथन कहता है कि यदि कोई प्राकृतिक संख्या n मौजूद है जैसे कि x, n से कम है, तब x शून्य से कम है। दोनों कथन झूठे हैं. पहला कथन n=2 के लिए मान्य नहीं है, क्योंकि x=1 n से कम है, लेकिन शून्य से कम नहीं है। पश्चात् वाला कथन x=1 के लिए मान्य नहीं है, क्योंकि प्राकृतिक संख्या n=2 x<n को संतुष्ट करती है, लेकिन x=1 शून्य से कम नहीं है।
पहला कथन कहता है कि किसी भी प्राकृतिक संख्या n के लिए, यदि x, n से कम है तब x शून्य से कम है। पश्चात् वाला कथन कहता है कि यदि कोई प्राकृतिक संख्या n उपस्तिथ है जैसे कि x, n से कम है, तब x शून्य से कम है। दोनों कथन झूठे हैं. पहला कथन n=2 के लिए मान्य नहीं है, क्योंकि x=1 n से कम है, किन्तु शून्य से कम नहीं है। पश्चात् वाला कथन x=1 के लिए मान्य नहीं है, क्योंकि प्राकृतिक संख्या n=2 x<n को संतुष्ट करती है, किन्तु x=1 शून्य से कम नहीं है।


=== उदाहरण ===
=== उदाहरण ===
Line 60: Line 60:
लगता है कि <math>\phi</math>, <math>\psi</math>, और <math>\rho</math> क्वांटिफायर-मुक्त सूत्र हैं और इनमें से कोई भी दो सूत्र किसी भी मुक्त चर को साझा नहीं करते हैं। सूत्र पर विचार करें
लगता है कि <math>\phi</math>, <math>\psi</math>, और <math>\rho</math> क्वांटिफायर-मुक्त सूत्र हैं और इनमें से कोई भी दो सूत्र किसी भी मुक्त चर को साझा नहीं करते हैं। सूत्र पर विचार करें
:<math> (\phi \lor \exists x \psi) \rightarrow \forall z \rho</math>.
:<math> (\phi \lor \exists x \psi) \rightarrow \forall z \rho</math>.
अंतरतम उपसूत्रों से शुरू होने वाले नियमों को पुनरावर्ती रूप से क्रियान्वित करके, तार्किक रूप से समकक्ष सूत्रों का निम्नलिखित अनुक्रम प्राप्त किया जा सकता है:
अंतरतम उपसूत्रों से प्रारंभ होने वाले नियमों को पुनरावर्ती रूप से क्रियान्वित करके, तार्किक रूप से समकक्ष सूत्रों का निम्नलिखित अनुक्रम प्राप्त किया जा सकता है:
:<math> (\phi \lor \exists x \psi) \rightarrow \forall z \rho</math>.
:<math> (\phi \lor \exists x \psi) \rightarrow \forall z \rho</math>.
:<math> ( \exists x (\phi \lor \psi) ) \rightarrow \forall z \rho</math>,
:<math> ( \exists x (\phi \lor \psi) ) \rightarrow \forall z \rho</math>,
Line 80: Line 80:
=== [[अंतर्ज्ञानवादी तर्क]] ===
=== [[अंतर्ज्ञानवादी तर्क]] ===


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


[[बीएचके व्याख्या]] दर्शाती है कि क्यों कुछ सूत्रों में कोई अंतर्ज्ञान-समतुल्य प्रीनेक्स फॉर्म नहीं है। इस व्याख्या में, का प्रमाण
[[बीएचके व्याख्या]] दर्शाती है कि क्यों कुछ सूत्रों में कोई अंतर्ज्ञान-समतुल्य प्रीनेक्स फॉर्म नहीं है। इस व्याख्या में, का प्रमाण
:<math>(\exists x \phi) \rightarrow \exists y \psi \qquad (1)</math>
:<math>(\exists x \phi) \rightarrow \exists y \psi \qquad (1)</math>
एक फलन है, जिसे ठोस x और प्रमाण दिया गया है <math>\phi (x)</math>, ठोस y और प्रमाण उत्पन्न करता है <math>\psi (y)</math>. इस मामले में x के दिए गए मान से y के मान की गणना करना स्वीकार्य है। का प्रमाण
एक फलन है, जिसे ठोस x और प्रमाण दिया गया है <math>\phi (x)</math>, ठोस y और प्रमाण उत्पन्न करता है <math>\psi (y)</math>. इस स्थितियोंमें x के दिए गए मान से y के मान की गणना करना स्वीकार्य है। का प्रमाण
:<math>\exists y ( \exists x \phi \rightarrow \psi), \qquad  (2)</math>
:<math>\exists y ( \exists x \phi \rightarrow \psi), \qquad  (2)</math>
दूसरी ओर, y का एकल ठोस मान और फलन उत्पन्न करता है जो किसी भी प्रमाण को परिवर्तित करता है <math>\exists x \phi</math> के प्रमाण में <math>\psi (y)</math>. यदि प्रत्येक x संतोषजनक है <math>\phi</math> y संतोषजनक बनाने के लिए उपयोग किया जा सकता है <math>\psi</math> लेकिन ऐसे किसी भी y का निर्माण ऐसे x के ज्ञान के बिना नहीं किया जा सकता है तब सूत्र (1) सूत्र (2) के सामान्तर नहीं होगा।
दूसरी ओर, y का एकल ठोस मान और फलन उत्पन्न करता है जो किसी भी प्रमाण को परिवर्तित करता है <math>\exists x \phi</math> के प्रमाण में <math>\psi (y)</math>. यदि प्रत्येक x संतोषजनक है <math>\phi</math> y संतोषजनक बनाने के लिए उपयोग किया जा सकता है <math>\psi</math> किन्तु ऐसे किसी भी y का निर्माण ऐसे x के ज्ञान के बिना नहीं किया जा सकता है तब सूत्र (1) सूत्र (2) के सामान्तर नहीं होगा।


किसी सूत्र को प्रीनेक्स फॉर्म में परिवर्तित करने के नियम जो अंतर्ज्ञानवादी तर्क में विफल होते हैं:
किसी सूत्र को प्रीनेक्स फॉर्म में परिवर्तित करने के नियम जो अंतर्ज्ञानवादी तर्क में विफल होते हैं:
Line 102: Line 102:
[[प्रथम-क्रम तर्क]] के लिए गोडेल की पूर्णता प्रमेय का प्रमाण यह मानता है कि सभी सूत्रों को प्रीनेक्स सामान्य रूप में पुनर्गठित किया गया है।
[[प्रथम-क्रम तर्क]] के लिए गोडेल की पूर्णता प्रमेय का प्रमाण यह मानता है कि सभी सूत्रों को प्रीनेक्स सामान्य रूप में पुनर्गठित किया गया है।


ज्यामिति के लिए टार्स्की के स्वयंसिद्ध तार्किक प्रणाली है जिसके सभी वाक्य 'सार्वभौमिक-अस्तित्ववादी रूप' में लिखे जा सकते हैं, प्रीनेक्स सामान्य रूप का विशेष मामला जिसमें किसी भी [[अस्तित्वगत परिमाणीकरण]] से पहले प्रत्येक [[सार्वभौमिक परिमाणीकरण]] होता है, ताकि सभी वाक्यों को इस रूप में फिर से लिखा जा सके <math>\forall u</math> <math>\forall v</math> <math>\ldots</math> <math>\exists a</math> <math>\exists b</math> <math>\phi</math>, कहाँ <math>\phi</math> वाक्य है जिसमें कोई परिमाणक नहीं है। इस तथ्य ने [[अल्फ्रेड टार्स्की]] को यह साबित करने की अनुमति दी कि यूक्लिडियन ज्यामिति निर्णायकता (तर्क) है।
ज्यामिति के लिए टार्स्की के स्वयंसिद्ध तार्किक प्रणाली है जिसके सभी वाक्य 'सार्वभौमिक-अस्तित्ववादी रूप' में लिखे जा सकते हैं, प्रीनेक्स सामान्य रूप का विशेष मामला जिसमें किसी भी [[अस्तित्वगत परिमाणीकरण]] से पहले प्रत्येक [[सार्वभौमिक परिमाणीकरण]] होता है, जिससे कि सभी वाक्यों को इस रूप में फिर से लिखा जा सके <math>\forall u</math> <math>\forall v</math> <math>\ldots</math> <math>\exists a</math> <math>\exists b</math> <math>\phi</math>, कहाँ <math>\phi</math> वाक्य है जिसमें कोई परिमाणक नहीं है। इस तथ्य ने [[अल्फ्रेड टार्स्की]] को यह सिद्ध करना  करने की अनुमति दी कि यूक्लिडियन ज्यामिति निर्णायकता (तर्क) है।


==यह भी देखें==
==यह भी देखें==

Revision as of 22:19, 19 July 2023

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

मौलिक तर्क में प्रत्येक सूत्र तार्किक रूप से प्रीनेक्स सामान्य रूप में सूत्र के सामान्तर है। उदाहरण के लिए, यदि , , और तब दिखाए गए मुक्त चर के साथ क्वांटिफायर-मुक्त सूत्र हैं

मैट्रिक्स के साथ प्रीनेक्स सामान्य रूप में है , जबकि

तार्किक रूप से समतुल्य है किन्तु प्रीनेक्स सामान्य रूप में नहीं।

प्रीनेक्स फॉर्म में रूपांतरण

प्रत्येक प्रथम-क्रम विधेय कलन|प्रथम-क्रम सूत्र तार्किक रूप से (मौलिक तर्क में) प्रीनेक्स सामान्य रूप में कुछ सूत्र के सामान्तर है।[3] ऐसे अनेक रूपांतरण नियम हैं जिन्हें किसी सूत्र को प्रीनेक्स सामान्य रूप में परिवर्तित करने के लिए पुनरावर्ती रूप से क्रियान्वित किया जा सकता है। नियम इस पर निर्भर करते हैं कि सूत्र में कौन से तार्किक संयोजक दिखाई देते हैं।

संधि और विच्छेद

तार्किक संयोजन और तार्किक वियोजन के नियम यही कहते हैं

के सामान्तर है (हल्के) अतिरिक्त शर्त के अनुसार , या, समकक्ष, (कारणकि कम से कम व्यक्ति उपस्तिथ है),
के सामान्तर है ;

और

के सामान्तर है ,
के सामान्तर है अतिरिक्त शर्त के अनुसार .

समतुल्यताएँ तब मान्य होती हैं जब के मुक्त चर के रूप में प्रकट नहीं होता है ; अगर में मुक्त दिखाई देता है , कोई बाउंड का नाम बदल सकता है में और समतुल्य प्राप्त करें .

उदाहरण के लिए, रिंग (गणित) की भाषा में,

के सामान्तर है ,

किन्तु

के सामान्तर नहीं है

क्योंकि बाईं ओर का सूत्र किसी भी रिंग में सत्य है जब मुक्त चर x 0 के सामान्तर है, जबकि दाईं ओर के सूत्र में कोई मुक्त चर नहीं है और किसी भी गैर-तुच्छ रिंग में गलत है। इसलिए पहले के रूप में पुनः लिखा जाएगा और फिर प्रीनेक्स को सामान्य रूप में डाल दें .

निषेध

निषेध के नियम यही कहते हैं

के सामान्तर है और
के सामान्तर है .

निहितार्थ

भौतिक सशर्त के लिए चार नियम हैं: दो जो पूर्ववर्ती से परिमाणक हटाते हैं और दो जो परिणामी से परिमाणवाचक हटाते हैं। इन नियमों को निहितार्थ #तर्क को पुनः लिखकर प्राप्त किया जा सकता है जैसा और उपरोक्त विच्छेद और निषेध के नियमों को क्रियान्वित करना। विच्छेदन के नियमों की तरह, इन नियमों के लिए आवश्यक है कि उपसूत्र में परिमाणित चर दूसरे उपसूत्र में मुक्त दिखाई न दे।

पूर्ववर्ती से परिमाणकों को हटाने के नियम हैं (परिमाणकों के परिवर्तन पर ध्यान दें):

के सामान्तर है (इस धारणा के अनुसार ),
के सामान्तर है .

परिणामी से परिमाणक हटाने के नियम हैं:

के सामान्तर है (इस धारणा के अनुसार ),
के सामान्तर है .

उदाहरण के लिए, जब परिमाणीकरण की सीमा गैर-ऋणात्मक प्राकृतिक संख्या है (अर्थात। ), कथन

तार्किक रूप से कथन के समतुल्य है

पहला कथन कहता है कि यदि x किसी प्राकृत संख्या से कम है, तब x शून्य से भी कम है। पश्चात् वाला कथन कहता है कि कुछ प्राकृतिक संख्या n उपस्तिथ है जैसे कि यदि x, n से कम है, तब x शून्य से भी कम है। दोनों कथन सत्य हैं। पहला कथन सत्य है क्योंकि यदि x किसी प्राकृत संख्या से कम है, तब उसे सबसे छोटी प्राकृत संख्या (शून्य) से भी कम होना चाहिए। पश्चात् वाला कथन सत्य है क्योंकि n=0 निहितार्थ को टॉटोलॉजी (तर्क) बनाता है।

ध्यान दें कि कोष्ठक का स्थान स्कोप (तर्क) को दर्शाता है, जो सूत्र के अर्थ के लिए बहुत महत्वपूर्ण है। निम्नलिखित दो कथनों पर विचार करें:

और इसका तार्किक रूप से समतुल्य कथन

पहला कथन कहता है कि किसी भी प्राकृतिक संख्या n के लिए, यदि x, n से कम है तब x शून्य से कम है। पश्चात् वाला कथन कहता है कि यदि कोई प्राकृतिक संख्या n उपस्तिथ है जैसे कि x, n से कम है, तब x शून्य से कम है। दोनों कथन झूठे हैं. पहला कथन n=2 के लिए मान्य नहीं है, क्योंकि x=1 n से कम है, किन्तु शून्य से कम नहीं है। पश्चात् वाला कथन x=1 के लिए मान्य नहीं है, क्योंकि प्राकृतिक संख्या n=2 x<n को संतुष्ट करती है, किन्तु x=1 शून्य से कम नहीं है।

उदाहरण

लगता है कि , , और क्वांटिफायर-मुक्त सूत्र हैं और इनमें से कोई भी दो सूत्र किसी भी मुक्त चर को साझा नहीं करते हैं। सूत्र पर विचार करें

.

अंतरतम उपसूत्रों से प्रारंभ होने वाले नियमों को पुनरावर्ती रूप से क्रियान्वित करके, तार्किक रूप से समकक्ष सूत्रों का निम्नलिखित अनुक्रम प्राप्त किया जा सकता है:

.
,
,
,
,
,
,
.

यह मूल सूत्र के समतुल्य एकमात्र प्रीनेक्स फॉर्म नहीं है। उदाहरण के लिए, उपरोक्त उदाहरण में पूर्ववर्ती से पहले परिणामी से निपटकर, प्रीनेक्स फॉर्म

प्राप्त किया जा सकता है:

,
,
.

क्वांटिफायर (तर्क)#समान सीमा वाले दो सार्वभौमिक क्वांटिफायर के क्वांटिफायर (नेस्टिंग) का क्रम कथन के अर्थ/सत्य मूल्य को नहीं बदलता है।

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

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

बीएचके व्याख्या दर्शाती है कि क्यों कुछ सूत्रों में कोई अंतर्ज्ञान-समतुल्य प्रीनेक्स फॉर्म नहीं है। इस व्याख्या में, का प्रमाण

एक फलन है, जिसे ठोस x और प्रमाण दिया गया है , ठोस y और प्रमाण उत्पन्न करता है . इस स्थितियोंमें x के दिए गए मान से y के मान की गणना करना स्वीकार्य है। का प्रमाण

दूसरी ओर, y का एकल ठोस मान और फलन उत्पन्न करता है जो किसी भी प्रमाण को परिवर्तित करता है के प्रमाण में . यदि प्रत्येक x संतोषजनक है y संतोषजनक बनाने के लिए उपयोग किया जा सकता है किन्तु ऐसे किसी भी y का निर्माण ऐसे x के ज्ञान के बिना नहीं किया जा सकता है तब सूत्र (1) सूत्र (2) के सामान्तर नहीं होगा।

किसी सूत्र को प्रीनेक्स फॉर्म में परिवर्तित करने के नियम जो अंतर्ज्ञानवादी तर्क में विफल होते हैं:

(1) तात्पर्य ,
(2) तात्पर्य ,
(3) तात्पर्य ,
(4) तात्पर्य ,
(5) तात्पर्य ,

(x मुक्त चर के रूप में प्रकट नहीं होता है (1) और (3) में; x मुक्त चर के रूप में प्रकट नहीं होता है (2) और (4) में)।

प्रीनेक्स फॉर्म का उपयोग

कुछ प्रमाण गणना केवल उस सिद्धांत से निपटेंगे जिसके सूत्र प्रीनेक्स सामान्य रूप में लिखे गए हैं। अंकगणितीय पदानुक्रम और विश्लेषणात्मक पदानुक्रम विकसित करने के लिए यह अवधारणा आवश्यक है।

प्रथम-क्रम तर्क के लिए गोडेल की पूर्णता प्रमेय का प्रमाण यह मानता है कि सभी सूत्रों को प्रीनेक्स सामान्य रूप में पुनर्गठित किया गया है।

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

यह भी देखें

टिप्पणियाँ

  1. The term 'prenex' comes from the Latin praenexus "tied or bound up in front", past participle of praenectere [1] (archived as of May 27, 2011 at [2])
  2. Hinman, P. (2005), p. 110
  3. Hinman, P. (2005), p. 111

संदर्भ

  • रिचर्ड एल एप्सटीन (18 December 2011). Classical Mathematical Logic: The Semantic Foundations of Logic. Princeton University Press. pp. 108–. ISBN 978-1-4008-4155-4.
  • पीटर बी. एंड्रयूज (17 April 2013). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Springer Science & Business Media. pp. 111–. ISBN 978-94-015-9934-4.
  • इलियट मेंडेलसन (1 June 1997). Introduction to Mathematical Logic, Fourth Edition. CRC Press. pp. 109–. ISBN 978-0-412-80830-2.
  • हिनमन, पीटर (2005), गणितीय तर्क के मूल सिद्धांत, ए के पीटर्स, ISBN 978-1-56881-262-5