हरब्रांडीकरण

एक तार्किक सूत्र का हेरब्रांडाइजेशन (जैक्स हेरब्रांड के नाम पर) एक निर्माण है जो एक सूत्र के शोलेमाइजेशन के लिए द्वैत (गणित) है। थोरल्फ़ स्कोलेम ने लोवेनहेम-स्कोलेम प्रमेय (स्कोलेम 1920) के अपने प्रमाण के हिस्से के रूप में प्रीनेक्स फॉर्म में सूत्रों के स्कोलेमाइजेशन पर विचार किया था। हेरब्रांड ने हेरब्रांडाइजेशन की इस दोहरी धारणा के साथ काम किया, जिसे हेरब्रांड के प्रमेय (प्रमाण सिद्धांत) को साबित करने के लिए गैर-प्रीनेक्स फ़ार्मुलों पर भी लागू करने के लिए सामान्यीकृत किया गया।

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

परिभाषा एवं उदाहरण

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

का हरब्रांडीकरण $F$ फिर इस प्रकार प्राप्त किया जाता है:

• सबसे पहले, किसी भी फ्री वेरिएबल को बदलें $F$ निरंतर प्रतीकों द्वारा.
• दूसरा, वेरिएबल्स पर सभी क्वांटिफायर को हटा दें जो या तो (1) सार्वभौमिक रूप से परिमाणित हैं और निषेध चिह्नों की एक सम संख्या के भीतर हैं, या (2) अस्तित्वगत रूप से परिमाणित हैं और विषम संख्या में निषेध चिह्नों के भीतर हैं।
• अंत में, ऐसे प्रत्येक वेरिएबल को बदलें $v$ एक फ़ंक्शन प्रतीक के साथ $f_{v}(x_{1},\dots ,x_{k})$, कहाँ $x_{1},\dots ,x_{k}$ वे चर हैं जो अभी भी परिमाणित हैं, और जिनके परिमाणक नियंत्रित होते हैं $v$.

उदाहरण के लिए, सूत्र पर विचार करें $F:=\forall y\exists x[R(y,x)\wedge \neg \exists zS(x,z)]$. प्रतिस्थापित करने के लिए कोई निःशुल्क चर नहीं हैं। चर $y,z$ दूसरे चरण के लिए हम इस प्रकार पर विचार करते हैं, इसलिए हम क्वांटिफायर हटा देते हैं $\forall y$ और $\exists z$. अंत में, हम फिर प्रतिस्थापित करते हैं $y$ एक स्थिरांक के साथ $c_{y}$ (चूँकि शासन करने वाला कोई अन्य परिमाणक नहीं था $y$), और हम प्रतिस्थापित करते हैं $z$ एक फ़ंक्शन प्रतीक के साथ $f_{z}(x)$:

$F^{H}=\exists x[R(c_{y},x)\wedge \neg S(x,f_{z}(x))].$

किसी सूत्र का स्कोलेमाइज़ेशन समान रूप से प्राप्त किया जाता है, सिवाय इसके कि ऊपर के दूसरे चरण में, हम उन चरों पर क्वांटिफायर हटा देंगे जो या तो (1) अस्तित्वगत रूप से परिमाणित हैं और निषेधों की एक सम संख्या के भीतर हैं, या (2) सार्वभौमिक रूप से परिमाणित हैं और एक विषम संख्या के भीतर हैं नकारों का. इस प्रकार, उसी पर विचार किया जा रहा है $F$ ऊपर से, इसका स्कोलेमाइज़ेशन होगा:

$F^{S}=\forall y[R(y,f_{x}(y))\wedge \neg \exists zS(f_{x}(y),z)].$

इन निर्माणों के महत्व को समझने के लिए, हेरब्रांड का प्रमेय (प्रमाण सिद्धांत)|हेरब्रांड का प्रमेय या लोवेनहेम-स्कोलेम प्रमेय देखें।

यह भी देखें

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

संदर्भ

• Skolem, T. "Logico-combinatorial investigations in the satisfiability or provability of mathematical propositions: A simplified proof of a theorem by L. Löwenheim and generalizations of the theorem". (In van Heijenoort 1967, 252-63.)
• Herbrand, J. "Investigations in proof theory: The properties of true propositions". (In van Heijenoort 1967, 525-81.)
• van Heijenoort, J. From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931. Harvard University Press, 1967.