स्कोलेम सामान्य रूप

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

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

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

उदाहरण

स्कोलेमाइज़ेशन का सबसे सरल रूप अस्तित्वगत रूप से परिमाणित वेरिएबल के लिए है जो सार्वभौमिक परिमाणक के सीमा (तर्क) के अंदर नहीं हैं। इन्हें केवल नए स्थिरांक बनाकर प्रतिस्थापित किया जा सकता है। उदाहरण के लिए, $\exists xP(x)$ को $P(c)$ में बदला जा सकता है, जहाँ $c$ नया स्थिरांक (सूत्र में कहीं और नहीं होता है) है।

सामान्यतः, स्कोलेमाइज़ेशन प्रत्येक अस्तित्वगत रूप से परिमाणित वेरिएबल $y$ को एक शब्द $f(x_{1},\ldots ,x_{n})$ के साथ प्रतिस्थापित करके किया जाता है जिसका फ़ंक्शन प्रतीक $f$ नया है। इस पद के वेरिएबल इस प्रकार है। यदि सूत्र प्रीनेक्स सामान्य रूप में है, तो $x_{1},\ldots ,x_{n}$ वे वेरिएबल हैं जो सार्वभौमिक रूप से परिमाणित हैं और जिनके परिमाणक $y$ से पहले हैं। सामान्यतः, वे ऐसे वेरिएबल होते हैं जिन्हें सार्वभौमिक रूप से परिमाणित (हम मानते हैं कि हमें क्रम में अस्तित्वगत परिमाणकों से छुटकारा मिल गया है, इसलिए $\exists y$ से पहले के सभी अस्तित्वगत परिमाणकों को हटा दिया गया है) किया जाता है और जैसे कि $\exists y$ उनके परिमाणकों के सीमा में होता है। इस प्रक्रिया में प्रस्तुत किए गए फ़ंक्शन $f$ को स्कोलेम फ़ंक्शन (या स्कोलेम स्थिरांक यदि यह शून्य एरिटी का है) कहा जाता है और शब्द को स्कोलेम शब्द कहा जाता है।

उदाहरण के तौर पर सूत्र $\forall x\exists y\forall z.P(x,y,z)$ स्कोलेम सामान्य रूप में नहीं है क्योंकि इसमें अस्तित्वगत परिमाणक $\exists y$ सम्मिलित है। स्कोलेमाइज़ेशन $y$ को $f(x)$ से प्रतिस्थापित करता है, जहाँ $f$ एक नया फ़ंक्शन प्रतीक है, और $y$. पर परिमाणीकरण को हटा देता है। परिणामी सूत्र $\forall x\forall z.P(x,f(x),z)$ है। स्कोलेम शब्द $f(x)$ में $x$ सम्मिलित है, किन्तु $z$ नहीं, क्योंकि हटाया जाने वाला क्वांटिफायर $\exists y$ $\forall x$ के सीमा में है, किन्तु $\forall z$ के सीमा में नहीं है; चूँकि यह सूत्र प्रीनेक्स सामान्य रूप में है, यह कहने के बराबर है कि, क्वांटिफायर की सूची में, $x$, $y$ से पहले आता है जबकि $z$ नहीं। इस परिवर्तन द्वारा प्राप्त सूत्र तभी संतोषजनक है जब मूल सूत्र हो।

स्कोलेमाइज़ेशन कैसे काम करता है

स्कोलेमाइज़ेशन प्रथम-क्रम संतुष्टि की परिभाषा के साथ-साथ दूसरे-क्रम तुल्यता को लागू करके काम करता है। तुल्यता एक सार्वभौमिक परिमाणक से पहले एक अस्तित्वगत परिमाणक को "स्थानांतरित" करने का एक विधि प्रदान करती है।

$\forall x\exists yR(x,y)\iff \exists f\forall xR(x,f(x))$

जहाँ

$f(x)$ एक फ़ंक्शन है जो $x$ को $y$ पर मैप करता है।

सहज रूप से, वाक्य "प्रत्येक $x$ के लिए एक $y$ उपस्थित होता है जैसे कि $R(x,y)$" को समतुल्य रूप में परिवर्तित किया जाता है "प्रत्येक $x$ को $y$ में मैप करने वाला एक फ़ंक्शन $f$ उपस्थित होता है जैसे कि प्रत्येक $x$ के लिए यह $R(x,f(x))$ रखता है"।

यह तुल्यता उपयोगी है क्योंकि प्रथम-क्रम संतुष्टि की परिभाषा अंतर्निहित रूप से फ़ंक्शन प्रतीकों के मूल्यांकन पर परिमाण निर्धारित करती है। विशेष रूप से, प्रथम-क्रम सूत्र $\Phi$ संतोषजनक है यदि कोई मॉडल $M$ उपस्थित है और सूत्र के मुक्त वेरिएबल का मूल्यांकन $\mu$ है जो सूत्र का सही मूल्यांकन करता है। मॉडल में सभी फ़ंक्शन प्रतीकों का मूल्यांकन सम्मिलित है; इसलिए, स्कोलेम फ़ंक्शन अंतर्निहित रूप से अस्तित्वगत रूप से परिमाणित हैं। उपरोक्त उदाहरण में, $\forall x.R(x,f(x))$ यह तभी संतोषजनक है जब कोई मॉडल $M$ उपस्थित हो, जिसमें $f$ के लिए मूल्यांकन सम्मिलित हो, जैसे कि $\forall x.R(x,f(x))$ अपने मुक्त वेरिएबल (इस स्थिति में कोई नहीं) के कुछ मूल्यांकन के लिए सही है। इसे दूसरे क्रम में $\exists f\forall x.R(x,f(x))$ के रूप में व्यक्त किया जा सकता है। उपरोक्त तुल्यता के अनुसार, यह $\forall x\exists y.R(x,y)$ की संतुष्टि के समान है।

मेटा-स्तर पर, सूत्र $\Phi$ की प्रथम-क्रम संतुष्टि को $\exists M\exists \mu ~.~(M,\mu \models \Phi )$ के रूप में अंकन के थोड़े दुरुपयोग के साथ लिखा जा सकता है। जहां $M$ एक मॉडल है, $\mu$ मुक्त वेरिएबल का मूल्यांकन है, और $\models$ का अर्थ है कि $\mu$ के अनुसार $M$ में $\Phi$ सत्य है। चूँकि प्रथम-क्रम मॉडल में सभी फ़ंक्शन प्रतीकों का मूल्यांकन होता है, कोई भी स्कोलेम फ़ंक्शन जिसमें $\Phi$ सम्मिलित होता है, उसे अंतर्निहित रूप से $\exists M$ द्वारा परिमाणित किया जाता है। परिणामस्वरूप, सूत्र के सामने के कार्यों पर अस्तित्वगत परिमाणकों को वेरिएबल के स्थान पर अस्तित्वगत परिमाणकों से प्रतिस्थापित करने के बाद भी इन अस्तित्वगत परिमाणकों को हटाकर सूत्र को प्रथम-क्रम वाले परिमाणकों के रूप में माना जा सकता है। $\exists f\forall x.R(x,f(x))$ को $\forall x.R(x,f(x))$ मानने का यह अंतिम चरण पूरा किया जा सकता है क्योंकि प्रथम-क्रम संतुष्टि की परिभाषा में कार्यों को अंतर्निहित रूप से $\exists M$ द्वारा परिमाणित किया गया है।

स्कोलेमाइज़ेशन की शुद्धता को उदाहरण सूत्र $F_{1}=\forall x_{1}\dots \forall x_{n}\exists yR(x_{1},\dots ,x_{n},y)$ पर निम्नानुसार दिखाया जा सकता है। यह सूत्र मॉडल $M$ द्वारा संतुष्ट है यदि और केवल तभी, मॉडल के डोमेन में $x_{1},\dots ,x_{n}$ के लिए प्रत्येक संभावित मान के लिए, मॉडल के डोमेन में $y$ के लिए एक मान उपस्थित है जो $R(x_{1},\dots ,x_{n},y)$ को सत्य बनाता है। पसंद के सिद्धांत के अनुसार, एक फ़ंक्शन $f$ उपस्थित है जैसे कि $y=f(x_{1},\dots ,x_{n})$। परिणामस्वरूप, सूत्र $F_{2}=\forall x_{1}\dots \forall x_{n}R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))$ संतोषजनक है, क्योंकि इसमें $f$ से $M$ के मूल्यांकन को जोड़कर प्राप्त मॉडल है। इससे पता चलता है कि $F_{1}$ केवल संतोषजनक है यदि $F_{2}$ भी संतोषजनक है। इसके विपरीत, यदि $F_{2}$ संतोषजनक है, तो एक मॉडल $M'$ उपस्थित है जो इसे संतुष्ट करता है; इस मॉडल में फ़ंक्शन $f$ के लिए एक मूल्यांकन सम्मिलित है, इस प्रकार, $x_{1},\dots ,x_{n}$ के प्रत्येक मान के लिए सूत्र $R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))$ धारण करता है। परिणामस्वरूप, $F_{1}$ उसी मॉडल से संतुष्ट है क्योंकि कोई $x_{1},\ldots ,x_{n}$ के प्रत्येक मान के लिए, मान $y=f(x_{1},\dots ,x_{n})$ चुन सकता है, जहां $f$ का मूल्यांकन $M'$ के अनुसार किया जाता है।

स्कोलेमाइज़ेशन के उपयोग

स्कोलेमाइज़ेशन के उपयोगों में से स्वचालित प्रमेय सिद्ध करना है। उदाहरण के लिए, विश्लेषणात्मक टेबल्यू की विधि में, जब भी कोई सूत्र जिसका प्रमुख परिमाणक अस्तित्वगत होता है, तो स्कोलेमाइजेशन के माध्यम से उस परिमाणक को हटाकर प्राप्त सूत्र उत्पन्न किया जा सकता है। उदाहरण के लिए, यदि $\exists x.\Phi (x,y_{1},\ldots ,y_{n})$ एक टेबल्यू में होता है, जहां $x,y_{1},\ldots ,y_{n}$ $\Phi (x,y_{1},\ldots ,y_{n})$ के मुक्त वेरिएबल हैं तो $\Phi (f(y_{1},\ldots ,y_{n}),y_{1},\ldots ,y_{n})$ टेबल्यू की उसी शाखा में जोड़ा जा सकता है। यह जोड़ टेबल्यू के गुण में कोई बदलाव नहीं करता है: पुराने सूत्र के प्रत्येक मॉडल को नए सूत्र के मॉडल में $f$ का उपयुक्त मूल्यांकन जोड़कर बढ़ाया जा सकता है।

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

एक अन्य उपयोग प्रथम-क्रम तर्क के लिए रिज़ॉल्यूशन विधि में है, जहां सूत्रों को सार्वभौमिक रूप से परिमाणित समझे जाने वाले खंडों (तर्क) के सेट के रूप में दर्शाया जाता है। (उदाहरण के लिए ड्रिंकर पैराडॉक्स देखें।)

मॉडल सिद्धांत में महत्वपूर्ण परिणाम लोवेनहेम-स्कोलेम प्रमेय है, जिसे सिद्धांत को स्कोलेमाइज़ करके और परिणामी स्कोलेम कार्यों के अनुसार बंद करके सिद्ध किया जा सकता है।

स्कोलेम सिद्धांत

सामान्यतः, यदि $T$ सिद्धांत (गणितीय तर्क) है और प्रत्येक सूत्र के लिए मुक्त वेरिएबल हैं $x_{1},\dots ,x_{n},y$ फ़ंक्शन प्रतीक है $F$ यह संभवतः स्कोलेम फ़ंक्शन है $y$, तब $T$ स्कोलेम सिद्धांत कहा जाता है। प्रत्येक स्कोलेम सिद्धांत मॉडल पूर्ण सिद्धांत है, अर्थात मॉडल की प्रत्येक उपसंरचना (गणित) प्रारंभिक तुल्यता है। स्कोलेम सिद्धांत टी के मॉडल एम को देखते हुए, निश्चित सेट ए वाले सबसे छोटे उपसंरचना को ए का 'स्कोलेम हल' कहा जाता है। ए का स्कोलेम हल ए के ऊपर परमाणु मॉडल (गणितीय तर्क) प्रमुख मॉडल है।

इतिहास

स्कोलेम सामान्य रूप का नाम दिवंगत नॉर्वेजियन गणितज्ञ थोरल्फ़ स्कोलेम के नाम पर रखा गया है।

यह भी देखें

• हरब्रांडीकरण, स्कोलेमाइज़ेशन का दोहरा
• विधेय फ़ैक्टर तर्क

संदर्भ

• Hodges, Wilfrid (1997), A Shorter Model Theory, Cambridge University Press, ISBN 978-0-521-58713-6

बाहरी संबंध

• "Skolem function", Encyclopedia of Mathematics, EMS Press, 2001 [1994]
• Skolemization on PlanetMath.org
• Skolemization by Hector Zenil, The Wolfram Demonstrations Project.
• Weisstein, Eric W. "SkolemizedForm". MathWorld.