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

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

परिभाषाएँ

• विच्छेदन गुण एक सिद्धांत से संतुष्ट होता है यदि, जब भी एक वाक्य (गणितीय तर्क) ए ∨ बी एक प्रमेय है, तो या तो ए एक प्रमेय है, या बी एक प्रमेय है.
• अस्तित्व संपत्ति या गवाह संपत्ति एक सिद्धांत से संतुष्ट है, जब भी एक वाक्य (∃x)A(x) एक प्रमेय है, जहां A(x) के पास कोई अन्य मुक्त चर नहीं है, तो कुछ प्रथम-क्रम तर्क#गठन नियम हैं जिससे सिद्धांत सिद्ध होता है 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)$ तो वहाँ एक प्राकृतिक संख्या ई ऐसी है कि, दे रही है $f_{e}$ सूचकांक ई के साथ गणना योग्य फ़ंक्शन बनें, सिद्धांत साबित होता है $(\forall x)\varphi (x,f_{e}(x))$.
• चर्च के नियम का एक प्रकार, सीआर₁, बताता है कि यदि सिद्धांत सिद्ध होता है $(\exists f\colon \mathbb {N} \to \mathbb {N} )\psi (f)$ तब एक प्राकृत संख्या e होती है जैसे कि सिद्धांत सिद्ध करता है $f_{e}$ समग्र है और सिद्ध होता है $\psi (f_{e})$.

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

परिणाम

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

लगभग परिभाषा के अनुसार, एक सिद्धांत जो स्वतंत्र कथनों के साथ बहिष्कृत मध्य को स्वीकार करता है, उसमें विच्छेदन गुण नहीं होता है। इसलिए रॉबिन्सन अंकगणित को व्यक्त करने वाले सभी शास्त्रीय सिद्धांतों में यह नहीं है। अधिकांश शास्त्रीय सिद्धांत, जैसे कि पीनो अंकगणित ज़र्मेलो-फ्रेंकेल सेट सिद्धांत सिद्धांत, अस्तित्व संपत्ति को मान्य नहीं करते हैं, उदाहरण के लिए। क्योंकि वे न्यूनतम संख्या सिद्धांत के अस्तित्व के दावे को मान्य करते हैं। लेकिन कुछ शास्त्रीय सिद्धांत, जैसे कि ZFC प्लस रचनाशीलता का सिद्धांत, अस्तित्व संपत्ति का एक कमजोर रूप है (रथजेन 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