विच्छेद और अस्तित्व गुण

गणितीय तर्क में, विच्छेदन और अस्तित्व गुण रचनात्मक गणित सिद्धांतों जैसे हेयटिंग अंकगणित और रचनात्मक सेट सिद्धांत (रथजेन 2005) की पहचान हैं।

परिभाषाएँ

• विच्छेदन गुण एक सिद्धांत से संतुष्ट होता है यदि, जब भी एक वाक्य (गणितीय तर्क) A ∨ B एक प्रमेय है, तो या तो A एक प्रमेय है, या B एक प्रमेय है
• अस्तित्व गुण या गवाह गुण एक सिद्धांत से संतुष्ट है, जब भी एक वाक्य (∃x)A(x) एक प्रमेय है, जहां A(x) में कोई अन्य मुक्त वेरिएबल नहीं है, तो कुछ शब्द t है जैसे कि सिद्धांत A(t) सिद्ध करता है)।

संबंधित गुण

राथजेन (2005) ने पांच गुणों की सूची दी है जो एक सिद्धांत में हो सकते हैं। इनमें विच्छेदन गुण (डीपी), अस्तित्व गुण (ईपी), और तीन अतिरिक्त गुण सम्मिलित हैं:

• संख्यात्मक अस्तित्व गुण (एनईपी) बताती है कि यदि सिद्धांत सिद्ध होता है $(\exists x\in \mathbb {N} )\varphi (x)$, जहां φ का कोई अन्य मुक्त वेरिएबल नहीं है, तो सिद्धांत सिद्ध होता है $\varphi ({\bar {n}})$ कुछ के लिए $n\in \mathbb {N} {\text{.}}$ यहाँ ${\bar {n}}$ में एक शब्द है $T$ संख्या n का प्रतिनिधित्व करने वाला एक शब्द है।
• चर्च के नियम (सीआर) में कहा गया है कि यदि सिद्धांत सिद्ध करता है $(\forall x\in \mathbb {N} )(\exists y\in \mathbb {N} )\varphi (x,y)$ तो एक प्राकृतिक संख्या e है, जैसे कि सूचकांक $f_{e}$ के साथ गणना योग्य फलन होने पर, सिद्धांत $(\forall x)\varphi (x,f_{e}(x))$ सिद्ध होता है।
• चर्च के नियम का एक प्रकार, CR₁, बताता है कि यदि सिद्धांत सिद्ध करता है ($(\exists f\colon \mathbb {N} \to \mathbb {N} )\psi (f)$ तो एक प्राकृतिक संख्या e है जैसे कि सिद्धांत सिद्ध करता है कि $f_{e}$ कुल है और $\psi (f_{e})$ सिद्ध होता है।

इन गुणों को सीधे रूप पर केवल उन सिद्धांतों के लिए व्यक्त किया जा सकता है जिनमें प्राकृतिक संख्याओं को परिमाणित करने की क्षमता होती है और, CR₁ के लिए, $\mathbb {N}$ को $\mathbb {N}$ तक कार्यों को परिमाणित करने की क्षमता होती है। वास्तव में, कोई कह सकता है कि एक सिद्धांत में इन गुणों में से एक है यदि सिद्धांत के एक निश्चित विस्तार में ऊपर बताई गई गुण है (रथजेन 2005)।

परिणाम

गैर-उदाहरण और उदाहरण

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

हेयटिंग अंकगणित विच्छेदन गुण और (संख्यात्मक) अस्तित्व गुण के लिए प्रसिद्ध है।

जबकि प्रारंभिक परिणाम अंकगणित के रचनात्मक सिद्धांतों के लिए थे, कई परिणाम रचनात्मक सेट सिद्धांतों (रथजेन 2005) के लिए भी जाने जाते हैं। जॉन माइहिल (1973) ने दिखाया कि संग्रह के सिद्धांत के पक्ष में प्रतिस्थापन के सिद्धांत को समाप्त करने के साथ IZF में विच्छेदन संपत्ति, संख्यात्मक अस्तित्व गुण और अस्तित्व गुण है। माइकल रैथजेन (2005) ने सिद्ध किया कि सीजेडएफ के पास विच्छेदन गुण और संख्यात्मक अस्तित्व गुण है।

फ़्रीड और स्केड्रोव (1990) ने देखा कि विच्छेदन गुण मुक्त हेयटिंग बीजगणित और मुक्त टोपोई में उपस्थित है। स्पष्ट शब्दों में, मुक्त टोपोज़ में, यह इस तथ्य से मेल खाता है कि टर्मिनल ऑब्जेक्ट, $\mathbf {1}$, दो उचित उप-वस्तुओं का जोड़ नहीं है। अस्तित्व संपत्ति के साथ यह इस प्रमाण का अनुवाद करता है कि $\mathbf {1}$ एक अविभाज्य प्रक्षेप्य वस्तु है - यह जिस फ़नकार का प्रतिनिधित्व करता है (वैश्विक-खंड फ़नकार) एपिमोर्फिज़्म और सह-उत्पादों को संरक्षित करता है।

गुणों के बीच संबंध

ऊपर चर्चा की गई पांच गुणों के बीच कई संबंध हैं।

अंकगणित की सेटिंग में, संख्यात्मक अस्तित्व गुण विच्छेदन गुण को दर्शाता है। प्रमाण इस तथ्य का उपयोग करता है कि एक विच्छेदन को प्राकृतिक संख्याओं की मात्रा निर्धारित करने वाले अस्तित्वगत सूत्र के रूप में फिर से लिखा जा सकता है:

$A\vee B\equiv (\exists n)[(n=0\to A)\wedge (n\neq 0\to B)]$.

इसलिए, यदि

$A\vee B$ का एक प्रमेय है $T$, ऐसा ही है $\exists n\colon (n=0\to A)\wedge (n\neq 0\to B)$.

इस प्रकार, संख्यात्मक अस्तित्व गुण को मानते हुए, कुछ उपस्थित $s$ ऐसा है कि

$({\bar {s}}=0\to A)\wedge ({\bar {s}}\neq 0\to B)$

एक प्रमेय है. चूँकि ${\bar {s}}$ एक अंक है, कोई ठोस रूप से $s$ के मान की जाँच कर सकता है: यदि $s=0$ तो $A$ एक प्रमेय है और यदि $s\neq 0$ है तो B एक प्रमेय है।

हार्वे फ्रीडमैन (1974) ने सिद्ध किया कि अंतर्ज्ञानवादी अंकगणित के किसी भी पुनरावर्ती गणना योग्य विस्तार में, विच्छेदन संपत्ति का तात्पर्य संख्यात्मक अस्तित्व संपत्ति से है। प्रमाण गोडेल के अपूर्णता प्रमेयों के प्रमाण के समान स्व-संदर्भित वाक्यों का उपयोग करता है। मुख्य चरण एक सूत्र (∃x)A(x) में अस्तित्वगत परिमाणक पर एक सीमा को खोजता है, जो एक परिबद्ध अस्तित्वमूलक सूत्र (∃x<n)A(x) का निर्माण करता है। परिबद्ध सूत्र को एक परिमित वियोजन A(1)∨A(2)∨...∨A(n) के रूप में लिखा जा सकता है। अंत में, विच्छेदन उन्मूलन का उपयोग यह दिखाने के लिए किया जा सकता है कि विच्छेदों में से एक सिद्ध करने योग्य है।

इतिहास

कर्ट गोडेल (1932) ने बिना किसी प्रमाण के कहा कि अंतर्ज्ञानवादी प्रस्तावक तर्क (बिना किसी अतिरिक्त स्वयंसिद्धता के) में विच्छेदन गुण होता है; इस परिणाम को गेरहार्ड जेंटज़न (1934, 1935) द्वारा सिद्ध किया गया और अंतर्ज्ञानवादी विधेय तर्क तक विस्तारित किया गया। स्टीफन कोल क्लेन (1945) ने सिद्ध किया कि हेयटिंग अंकगणित में विच्छेदन गुण और अस्तित्व गुण हैं। क्लेन की विधि ने यथार्थता की तकनीक की प्रारंभ की, जो अब रचनात्मक सिद्धांतों के अध्ययन में मुख्य विधि में से एक है (कोहलेनबैक 2008; ट्रॉलेस्ट्रा 1973)।

यह भी देखें

• रचनात्मक सेट सिद्धांत
• हेटिंग अंकगणित
• बहिष्कृत मध्य का नियम
• साध्यता
• अस्तित्वगत परिमाणक

संदर्भ

• Peter J. Freyd and Andre Scedrov, 1990, Categories, Allegories. North-Holland.
• Harvey Friedman, 1975, The disjunction property implies the numerical existence property, State University of New York at Buffalo.
• Gerhard Gentzen, 1934, "Untersuchungen über das logische Schließen. I", Mathematische Zeitschrift v. 39 n. 2, pp. 176–210.
• Gerhard Gentzen, 1935, "Untersuchungen über das logische Schließen. II", Mathematische Zeitschrift v. 39 n. 3, pp. 405–431.
• Kurt Gödel, 1932, "Zum intuitionistischen Aussagenkalkül", Anzeiger der Akademie der Wissenschaftischen in Wien, v. 69, pp. 65–66.
• Stephen Cole Kleene, 1945, "On the interpretation of intuitionistic number theory," Journal of Symbolic Logic, v. 10, pp. 109–124.
• Ulrich Kohlenbach, 2008, Applied proof theory, Springer.
• John Myhill, 1973, "Some properties of Intuitionistic Zermelo-Fraenkel set theory", in A. Mathias and H. Rogers, Cambridge Summer School in Mathematical Logic, Lectures Notes in Mathematics v. 337, pp. 206–231, Springer.
• Michael Rathjen, 2005, "The Disjunction and Related Properties for Constructive Zermelo-Fraenkel Set Theory", Journal of Symbolic Logic, v. 70 n. 4, pp. 1233–1254.
• Anne S. Troelstra, ed. (1973), Metamathematical investigation of intuitionistic arithmetic and analysis, Springer.

बाहरी संबंध

• Intuitionistic Logic by Joan Moschovakis, Stanford Encyclopedia of Philosophy