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

तार्किक सूत्र का हर्ब्रांडाइजेशन (जैक्स हेरब्रांड के नाम पर) ऐसा निर्माण है जो सूत्र के स्कोलेमाइजेशन के लिए द्वैत (गणित) है। थोरल्फ़ स्कोलेम ने लोवेनहेम-स्कोलेम प्रमेय (स्कोलेम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.