क्रमिक विश्लेषण
प्रमाण सिद्धांत में, क्रमसूचक विश्लेषण गणितीय सिद्धांतों को उनकी शक्ति के माप के रूप में क्रमसूचक संख्या (प्रायः बड़े गणनीय क्रमसूचक) प्रदान करता है। यदि सिद्धांतों में प्रमाण-सैद्धांतिक क्रमसूचक हैं, तो वे प्रायः समानता रखते हैं, और यदि सिद्धांत में दूसरे की तुलना में बड़ा प्रमाण-सैद्धांतिक क्रमसूचक है, तो यह प्रायः दूसरे सिद्धांत की निरंतरता को प्रमाणित कर सकता है।
इतिहास
क्रमसूचक विश्लेषण के क्षेत्र का निर्माण तब हुआ, जब 1934 में गेरहार्ड जेंटजन ने आधुनिक शब्दों में यह प्रमाणित करने के लिए कटौती उन्मूलन का उपयोग किया कि पीनो अंकगणित का प्रमाण-सैद्धांतिक क्रमांक ε0 (गणित) है, जेंटजन का कंसिस्टेंसी प्रमाण देखें।
परिभाषा
क्रमसूचक विश्लेषण का संबंध सही, प्रभावी (पुनरावर्ती) सिद्धांतों से है जो अंकगणित के पर्याप्त भाग की व्याख्या क्रमसूचक संकेतन के विषय में वर्णन करने के लिए कर सकते हैं।
ऐसे सिद्धांत का प्रमाण-सैद्धांतिक क्रम सभी क्रमसूचक संकेतन के क्रम प्रकारों का सर्वोच्च है (अनिवार्य रूप से पुनरावर्ती क्रमसूचक, खंड देखें) जो सिद्धांत सिद्ध कर सकता है कि वे उत्तम रूप से स्थापित संबंध हैं - सभी क्रमसूचकों का सर्वोच्च जिसके लिए अंकन उपस्थित है क्लेन के अर्थ में ऐसा है यह प्रमाणित करता है क्रमिक संकेतन है। समान रूप से, यह सभी अध्यादेशों का सर्वोच्च है जैसे कि संगणनीय फंक्शन उपस्थित है पर (प्राकृतिक संख्याओं का समुच्चय) जो इसे क्रमसूचक के साथ व्यवस्थित करता है और ऐसा के लिए अंकगणितीय कथनों का परिमित प्रवर्तन प्रमाणित करता है।
साधारण अंकन
कुछ सिद्धांतों, जैसे कि दूसरे क्रम के अंकगणित के उप-प्रणालियों के पास परिमित ऑर्डर के विषय में तर्क देने की कोई अवधारणा या प्रविधि नहीं है। उदाहरण के लिए, Z2 के उपप्रणाली के लिए इसका क्या अर्थ है, इसे औपचारिक रूप देने के लिए प्रमाणित करना सुव्यवस्थित, इसके अतिरिक्त क्रमसूचक संकेतन का निर्माण करते हैं आदेश प्रकार के साथ अब विभिन्न परिमित प्रवर्तन सिद्धांतों के साथ कार्य कर सकते हैं , जो समुच्चय-सैद्धांतिक अध्यादेशों के विषय में तर्क के लिए स्थानापन्न करता है।
चूंकि, कुछ पैथोलॉजिकल नोटेशन प्रणाली उपस्थित हैं जिनके साथ कार्य करना अप्रत्याशित रूप से जटिल होता है। उदाहरण के लिए, राथजेन आदिम पुनरावर्ती संकेतन प्रणाली देता है, यह उचित रूप से स्थापित है यदि पीए सुसंगत है,[1] आदेश प्रकार होने केतत्पश्चात - पीए के क्रमिक विश्लेषण में इस प्रकार के अंकन को सम्मिलित करने से झूठी समानता होगी।
ऊपरी बाध्य
किसी भी सिद्धांत के लिए दोनों -स्वयंसिद्ध और -ध्वनि हैं, पुनरावर्ती आदेश का अस्तित्व जो सिद्धांत प्रमाणित करने में विफल रहता है वह सुव्यवस्थित है, बाउंडिंग प्रमेय, और कहा कि सिद्ध रूप से उचित रूप से स्थापित क्रमिक अंकन वास्तव में उचित रूप से सुदृढ़ता स्थापित हैं। इस प्रकार प्रमाण-सैद्धांतिक क्रमसूचक ध्वनि सिद्धांत जिसमें स्वयंसिद्धीकरण सदैव (गणनीय) पुनरावर्ती क्रमसूचक होगा, जो कि चर्च-क्लेन क्रमसूचक से कम है। [2]
उदाहरण
सिद्धांत-सिद्धांत क्रमसूचक ω के साथ सिद्धांत
- Q, रॉबिन्सन अंकगणित (चूंकि इस प्रकार के शक्तिहीन सिद्धांतों के लिए प्रमाण-सैद्धांतिक क्रमसूचक की परिभाषा को परिवर्तित करना होगा)।
- PA– विवेकपूर्ण रूप से आदेशित रिंग के गैर-नकारात्मक भाग का प्रथम-क्रम सिद्धांत है।
प्रमाण-सिद्धांत क्रमसूचक ω वाले सिद्धांत
- RFA, अल्पविकसित कार्य अंकगणित।[3]
- IΔ0 Δ0 पर प्रेरण के साथ अंकगणित-बिना किसी स्वयंसिद्ध के भविष्यवाणी करता है कि घातांक कुल है।
प्रमाण-सिद्धांत क्रमसूचक ω2 के साथ सिद्धांत3
- ईएफए, प्रारंभिक कार्य अंकगणित।
- IΔ0 + ऍक्स्प Δ0- विधेय पर प्रेरण के साथ अंकगणित स्वयंसिद्ध द्वारा संवर्धित विधेय जो यह प्रभुत्व करता है कि घातांक कुल है।
- RCA*
0, ईएफए का दूसरा क्रम रूप कभी-कभी रिवर्स गणित में प्रयोग किया जाता है। - WKL*
0 ईएफए का दूसरा क्रम रूप कभी-कभी रिवर्स गणित में प्रयोग किया जाता है।
फ्रीडमैन के भव्य अनुमान से ज्ञात होता है कि अधिक सामान्य गणित को शक्तिहीन प्रणालियों में सिद्ध किया जा सकता है, जो कि उनके प्रमाण-सैद्धांतिक क्रमसूचक हैं।
प्रमाण-सिद्धांत क्रमसूचक ωn के साथ सिद्धांत (n = 2, 3, ... ω के लिए)
- IΔ0 या ईएफए स्वयंसिद्ध द्वारा संवर्धित है जो यह सुनिश्चित करता है कि n-वें स्तर के प्रत्येक तत्व ग्रेज़गोर्स्की पदानुक्रम कुल है।
प्रमाण-सिद्धांत क्रमसूचक ωω के साथ सिद्धांत
- RCA0 पुनरावर्ती विचार।
- WKL0 शक्तिहीन कोनिग प्रमेयिका।
- PRA, आदिम पुनरावर्ती अंकगणित।
- IΣ1पर प्रेरण के साथ अंकगणित Σ1 विधेय।
प्रमाण-सैद्धांतिक क्रमसूचक ε0 के साथ सिद्धांत
- PA, पियानो अंकगणित (कट एलिमिनेशन का उपयोग करके लोग द्वारा जेंटज़ेन की स्थिरता प्रमाण)।
- ACA0, अंकगणितीय विचार।
प्रमाण-सैद्धांतिक क्रमसूचक के साथ सिद्धांत
- ATR0, अंकगणितीय परिमित पुनरावर्तन।
- मनमाने ढंग से कई परिमित स्तर के ब्रह्मांडों के साथ मार्टिन-लोफ प्रकार का सिद्धांत।
इस क्रमसूचक को कभी-कभी विधेयात्मक सिद्धांतों की ऊपरी सीमा माना जाता है।
प्रमाण-सैद्धांतिक क्रमसूचक के साथ सिद्धांत बाचमन-हावर्ड ऑर्डिनल
- ID1, आगमनात्मक परिभाषाओं का प्रथम सिद्धांत।
- KP, कृप्के-प्लेटेक सेट सिद्धांत अनंत के स्वयंसिद्ध के साथ।
- CZF, Aczel का CZF रचनात्मक ज़र्मेलो-फ्रेंकेल सेट सिद्धांत।
- ईओएन, सोलोमन फेफरमैन की स्पष्ट गणित प्रणाली T0 का शक्तिहीन संस्करण है।
कृप्के-प्लेटेक या CZF समुच्चय सिद्धांत सभी उपसमुच्चयों के सेट के रूप में दिए गए पूर्ण पावरसेट के लिए सिद्धांतों के बिना शक्तिहीन सेट सिद्धांत हैं। इसके अतिरिक्त, वे या तो प्रतिबंधित पृथक्करण और नए सेटों के गठन के स्वयंसिद्ध हैं, या वे उन्हें बड़े संबंधों से भिन्न करने के अतिरिक्त कुछ फ़ंक्शन रिक्त स्थान (घातांक) का अस्तित्व प्रदान करते हैं।
बड़े प्रमाण-सैद्धांतिक अध्यादेशों के साथ सिद्धांत
पूर्ण द्वितीय क्रम अंकगणित का प्रमाण-सैद्धांतिक क्रम क्या है?[4]
- Π11 दूसरा क्रम अंकगणित विचार में बड़ा प्रमाण-सैद्धांतिक क्रमसूचक है, जिसे ताकुती द्वारा क्रमसूचक आरेखों के संदर्भ में वर्णित किया गया था, डायग्राम और जो बुखोल्ज़ के अंकन में ψ0(Ωω) से घिरा हुआ है। उसका भी क्रम है , परिमित रूप से पुनरावृत्त आगमनात्मक परिभाषाओं का सिद्धांत। और अनुक्रमित W-प्रकार के साथ MLW, मार्टिन-लोफ प्रकार सिद्धांत का क्रम भी है।
- IDω, बुखोल्ज़ की आईडी पदानुक्रम-पुनरावृत्त आगमनात्मक परिभाषाओं का सिद्धांत, इसका प्रमाण-सैद्धांतिक क्रमसूचक ताकुती-फ़ेफ़रमैन-बुखोलज़ क्रमसूचक के समान है।
- T0, फेफ़रमैन की स्पष्ट गणित की रचनात्मक प्रणाली में बड़ा प्रमाण-सैद्धांतिक क्रमसूचक है, जो KPi का प्रमाण-सैद्धांतिक क्रमसूचक भी है, क्रिप्के-प्लेटेक सेट सिद्धांत पुनरावृत्त स्वीकार्यता के साथ होते है।
- केपीआई, स्वीकार्य क्रमसूचक पर आधारित क्रिप्के-प्लेटेक सेट सिद्धांत का विस्तार है, जिसमें अत्यधिक बड़ा प्रमाण-सैद्धांतिक क्रमसूचक है जैगर और पोहलर्स के 1983 के पेपर में वर्णित है, जहां सबसे अल्प दुर्गम है।[5] यह क्रमसूचक भी प्रमाण-सैद्धांतिक क्रमसूचक है।
- केपीएम, स्वीकार्य क्रमसूचक पर आधारित क्रिप्के-प्लेटेक सेट सिद्धांत का विस्तार है, जिसका अत्यधिक बड़ा प्रमाण-सैद्धांतिक क्रमसूचक θ है, जिसे राथजेन (1990) द्वारा वर्णित किया गया था।
- एमएलएम, महलो-ब्रह्मांड द्वारा मार्टिन-लोफ प्रकार के सिद्धांत का विस्तार, भी बड़ा प्रमाण-सैद्धांतिक क्रमसूचक ψΩ1(ΩM + ω) है।.
- के समान प्रमाण-सैद्धांतिक क्रमसूचक है, जहाँ राथजेन के फ़ंक्शन का उपयोग करते हुए पूर्व शक्तिहीन कॉम्पैक्ट को संदर्भित करता है।
- के समान प्रमाण-सैद्धांतिक क्रमसूचक है, जहाँ अवर्णनीय और , स्टीगर्ट के साई फ़ंक्शन का उपयोग करके को संदर्भित करता है।
- के समान प्रमाण-सैद्धांतिक क्रमसूचक है जहाँ कम से कम क्रमसूचक का कार्डिनल एनालॉग है, जो - है सभी के लिए स्थिर और , स्टीगर्ट के साई फ़ंक्शन का उपयोग करते है।
प्राकृतिक संख्याओं के पावर सेट का वर्णन करने में सक्षम अधिकांश सिद्धांतों में प्रमाण-सैद्धांतिक अध्यादेश हैं जो इतने बड़े हैं कि अभी तक कोई स्पष्ट संयोजक विवरण नहीं दिया गया है। यह भी सम्मिलित है, पूर्ण दूसरे क्रम का अंकगणित () और ज़र्मेलो-फ्रेंकेल सेट थ्योरी और ZFC के साथ पॉवरसेट के साथ सिद्धांतों को सेट करें, अंतर्ज्ञानवादी नियम ZF (IZF) की शक्ति ZF के समान है।
क्रमिक विश्लेषण की तालिका
क्रमवाचक | प्रथम क्रम अंकगणित | दूसरे क्रम का अंकगणित | कृपके-प्लेटक सेट सिद्धांत | प्रकार सिद्धांत | रचनात्मक सेट सिद्धांत | स्पष्ट गणित |
---|---|---|---|---|---|---|
, | ||||||
, | ||||||
, | , | |||||
[1] | , | |||||
, | , | |||||
, , | ||||||
, | ||||||
[2] | ||||||
, | , | , | ||||
[3] | , | |||||
[4] | ||||||
, | ||||||
[5] | ||||||
[6] | ||||||
, | ||||||
[7] | ||||||
[8] | , | |||||
[9] | ||||||
[10] | ||||||
[11] | ||||||
[12] | ||||||
[13] | ||||||
[14] | ||||||
[15] | ||||||
[6] |
कुंजी
यह इस तालिका में प्रयुक्त प्रतीकों की सूची है:
- ψ Buchholz psi फ़ंक्शंस का प्रतिनिधित्व करता है | Buchholz का psi जब तक अन्यथा न कहा गया हो।
- Ψ या तो राथजेन या स्टीगर्ट के साई का प्रतिनिधित्व करता है।
- φ वेब्लेन के कार्य का प्रतिनिधित्व करता है।
- ω पहले परिमित ऑर्डिनल का प्रतिनिधित्व करता है।
- εα एप्सिलॉन संख्या (गणित) का प्रतिनिधित्व करता है।
- जीα गामा संख्या का प्रतिनिधित्व करता है (Γ0 फ़ेफ़रमैन-शुट्टे क्रमसूचक है)
- Ωα बेशुमार अध्यादेशों का प्रतिनिधित्व करते हैं (Ω1, संक्षिप्त Ω, पहला बेशुमार क्रमसूचक है|ω1).
यह इस तालिका में प्रयुक्त संक्षिप्त रूपों की एक सूची है:
- प्रथम क्रम अंकगणित
- रॉबिन्सन अंकगणित है
- विवेकपूर्ण रूप से आदेशित रिंग के गैर-नकारात्मक भाग का प्रथम-क्रम सिद्धांत है।
- जेन्सेन पदानुक्रम अंकगणित है।
- Δ0- तक सीमित प्रेरण के साथ अंकगणितीय है, बिना किसी स्वयं सिद्ध के भविष्यवाणी करता है कि घातांक कुल है।
- प्राथमिक कार्य अंकगणितीय है।
- Δ0- तक सीमित प्रेरण के साथ अंकगणितीय है, एक्सिओम द्वारा संवर्धित विधेय जो यह प्रमाणित करता है कि घातांक कुल है।
- प्राथमिक कार्य अंकगणित स्वयंसिद्ध द्वारा संवर्धित है जो यह सुनिश्चित करता है कि n-वें स्तर का प्रत्येक तत्व ग्रेज़गोर्स्की पदानुक्रम कुल है।
- स्वयंसिद्ध द्वारा संवर्धित यह सुनिश्चित करता है कि n-वें स्तर का प्रत्येक तत्व ग्रेज़गोर्स्की पदानुक्रम कुल है।
- आदिम पुनरावर्ती अंकगणित है।
- Σ1- तक सीमित प्रेरण के साथ अंकगणितीय विधेय है।
- पीआनो अभिगृहीत है।
- किन्तु केवल सकारात्मक सूत्रों के लिए प्रेरण के साथ है।
- मोनोटोन ऑपरेटरों के ν पुनरावृत्त निश्चित बिंदुओं द्वारा PA का विस्तार करता है।
- वास्तव में प्रथम-क्रम अंकगणितीय प्रणाली नहीं है, किन्तु प्राकृतिक संख्याओं के आधार पर भविष्यवाणिय तर्क द्वारा प्राप्त की जा सकने वाली वस्तु को कैप्चर करता है।
- पर ऑटोमोर्फिज्म है।
- मोनोटोन ऑपरेटरों के ν पुनरावृत्त कम से कम निश्चित बिंदुओं द्वारा PA का विस्तार करता है।
- वास्तव में प्रथम-क्रम अंकगणितीय प्रणाली नहीं है, किन्तु ν-बार पुनरावृत्त सामान्यीकृत आगमनात्मक परिभाषाओं के आधार पर विधेय तर्क द्वारा प्राप्त किया जा सकता है।
- पर ऑटोमोर्फिज्म है।
- का शक्तिहीन संस्करण डब्ल्यू प्रकार के आधार पर है।
- दूसरे क्रम का अंकगणित
- का दूसरा क्रम रूप है कभी-कभी रिवर्स गणित में प्रयोग किया जाता है।
- का दूसरा क्रम रूप है कभी-कभी रिवर्स गणित में प्रयोग किया जाता है।
- दूसरे क्रम का अंकगणित पुनरावर्ती विचार है।
- उलटा गणित शक्तिहीन कोनिग प्रमेयिका है।
- द्वितीय क्रम अंकगणितीय विचार है।
- साथ ही पूर्ण द्वितीय-क्रम प्रेरण योजना है।
- उलटा गणित अंकगणितीय परिमित रिकर्सन है।
- साथ ही पूर्ण द्वितीय-क्रम प्रेरण योजना है।
- साथ ही अभिकथन "प्रत्येक सत्य मानकों के साथ वाक्य (गणनीय कोडित) -का मॉडल में होता है।
- कृपके-प्लेटक समुच्चय सिद्धांत है।
- अनंत के स्वयंसिद्ध के साथ कृपके-प्लेटक सेट सिद्धांत है।
- क्रिप्के-प्लेटेक समुच्चय सिद्धांत है, जिसका ब्रह्माण्ड स्वीकार्य समुच्चय है।
- का शक्तिहीन संस्करण डब्ल्यू प्रकार के आधार पर है।
- अधिकार करता है कि ब्रह्मांड स्वीकार्य सेट की सीमा है।
- का शक्तिहीन संस्करण डब्ल्यू प्रकार के आधार पर है।
- अधिकार करता है कि ब्रह्मांड अप्राप्य सेट है।
- अधिकार करता है कि ब्रह्मांड अति दुर्गम सेट और दुर्गम सेट की सीमा है।
- अधिकार करता है कि ब्रह्मांड महलो सेट है।
- निश्चित प्रथम-क्रम प्रतिबिंब योजना द्वारा संवर्धित है।
- KPi स्वयंसिद्ध द्वारा संवर्धित है।
- क्या KPI को कम से कम पुनरावर्ती महलो क्रमसूचक अस्तित्व के स्वत्व से संवर्धित किया गया है।
सुपरस्क्रिप्ट शून्य इंगित करता है कि -प्रवर्तन को विस्थापित कर दिया जाता है।
- सिद्धांत टाइप करें
- प्रिमिटिव रिकर्सिव कंस्ट्रक्शन का हर्बेलिन-पेटी कैलकुलस है।
- प्रकार सिद्धांत बिना डब्ल्यू-प्रकार और साथ में ब्रह्मांड है।
- डब्ल्यू-टाइप के बिना टाइप थ्योरी है और अधिक ब्रह्मांडों के साथ है।
- आगामी ब्रह्मांड ऑपरेटर के साथ टाइप थ्योरी है।
- डब्ल्यू-प्रकार के बिना और सुपरयूनिवर्स के साथ टाइप थ्योरी है।
- डब्ल्यू-प्रकार के बिना टाइप थ्योरी पर ऑटोमोर्फिज्म है।
- ब्रह्माण्ड वाला प्रकार सिद्धांत है और Aczel के पुनरावृत्त सेट का प्रकार है।
- इंडेक्स्ड W-टाइप्स के साथ टाइप थ्योरी है।
- डब्ल्यू-प्रकार और ब्रह्मांड के साथ टाइप थ्योरी है।
- डब्ल्यू-प्रकार और अंततः कई ब्रह्मांडों के साथ प्रकार सिद्धांत है।
- डब्ल्यू-प्रकार के साथ प्रकार सिद्धांत पर ऑटोमोर्फिज्म है।
- Mahlo ब्रह्मांड के साथ प्रकार सिद्धांत है।
- रचनात्मक सेट सिद्धांत
- Aczel का रचनात्मक समुच्चय सिद्धांत है।
- है प्लस नियमित विस्तार स्वयंसिद्ध।
- साथ ही साथ ही फुल-सेकंड ऑर्डर प्रवर्तन स्कीम है।
- महलो ब्रह्मांड के साथ है।
- स्पष्ट गणित
- आधार स्पष्ट गणित और प्राथमिक विचार है।
- प्लस नियम में सम्मिलित होते है।
- प्लस स्वयंसिद्धों में सम्मिलित होते है।
- सोलोमन फेफ़रमैन का शक्तिहीन रूप है।
- , जहाँ है आगमनात्मक पीढ़ी है।
- ,है, जहाँ पूर्ण द्वितीय क्रम प्रेरण योजना है।
यह भी देखें
- समानता
- बड़ी कार्डिनल संपत्ति
- फ़ेफ़रमैन-शुट्टे क्रमसूचक
- बछमन-हावर्ड ऑर्डिनल
- जटिलता वर्ग
- Gentzen's कंसिस्टेंसी प्रूफ
टिप्पणियाँ
- 1.^ For
- 2.^ The Veblen function with countably infinitely iterated least fixed points.
- 3.^ Can also be commonly written as in Madore's ψ.
- 4.^ Uses Madore's ψ rather than Buchholz's ψ.
- 5.^ Can also be commonly written as in Madore's ψ.
- 6.^ represents the first recursively weakly compact ordinal. Uses Arai's ψ rather than Buchholz's ψ.
- 7.^ Also the proof-theoretic ordinal of , as the amount of weakening given by the W-types is not enough.
- 8.^ represents the first inaccessible cardinal. Uses Jäger's ψ rather than Buchholz's ψ.
- 9.^ represents the limit of the -inaccessible cardinals. Uses (presumably) Jäger's ψ.
- 10.^ represents the limit of the -inaccessible cardinals. Uses (presumably) Jäger's ψ.
- 11.^ represents the first Mahlo cardinal. Uses Rathjen's ψ rather than Buchholz's ψ.
- 12.^ represents the first weakly compact cardinal. Uses Rathjen's Ψ rather than Buchholz's ψ.
- 13.^ represents the first -indescribable cardinal. Uses Stegert's Ψ rather than Buchholz's ψ.
- 14.^ is the smallest such that ' is -indescribable') and ' is -indescribable '). Uses Stegert's Ψ rather than Buchholz's ψ.
- 15.^ represents the first Mahlo cardinal. Uses (presumably) Rathjen's ψ.
उद्धरण
- ↑ Rathjen, The Realm of Ordinal Analysis (p.3). Accessed 2021 September 29.
- ↑ M. Rathjen, The Realm of Ordinal Analysis (theorem 2.21). Accessed 3 October 2022.
- ↑ Krajicek, Jan (1995). परिबद्ध अंकगणित, प्रस्तावपरक तर्क और जटिलता सिद्धांत. Cambridge University Press. pp. 18–20. ISBN 9780521452052. defines the rudimentary sets and rudimentary functions, and proves them equivalent to the Δ0-predicates on the naturals. An ordinal analysis of the system can be found in Rose, H. E. (1984). Subrecursion: functions and hierarchies. University of Michigan: Clarendon Press. ISBN 9780198531890.
- ↑ M. Rathjen, Proof Theory: From Arithmetic to Set Theory (p.28). Accessed 14 August 2022.
- ↑ D. Madore, A Zoo of Ordinals (2017, p.2). Accessed 12 August 2022.
- ↑ Arai, Toshiyasu (2022-01-10). "An ordinal analysis of $\Pi_{1}$-Collection". arXiv:2112.09871 [math.LO].
संदर्भ
- Buchholz, W.; Feferman, S.; Pohlers, W.; Sieg, W. (1981), Iterated inductive definitions and sub-systems of analysis, Lecture Notes in Math., vol. 897, Berlin: Springer-Verlag, doi:10.1007/BFb0091894, ISBN 978-3-540-11170-2
- Pohlers, Wolfram (1989), Proof theory, Lecture Notes in Mathematics, vol. 1407, Berlin: Springer-Verlag, doi:10.1007/978-3-540-46825-7, ISBN 3-540-51842-8, MR 1026933
- Pohlers, Wolfram (1998), "Set Theory and Second Order Number Theory", Handbook of Proof Theory, Studies in Logic and the Foundations of Mathematics, vol. 137, Amsterdam: Elsevier Science B. V., pp. 210–335, doi:10.1016/S0049-237X(98)80019-0, ISBN 0-444-89840-9, MR 1640328
- Rathjen, Michael (1990), "Ordinal notations based on a weakly Mahlo cardinal.", Arch. Math. Logic, 29 (4): 249–263, doi:10.1007/BF01651328, MR 1062729, S2CID 14125063
- Rathjen, Michael (2006), "The art of ordinal analysis" (PDF), International Congress of Mathematicians, vol. II, Zürich: Eur. Math. Soc., pp. 45–69, MR 2275588, archived from the original on 2009-12-22
{{citation}}
: CS1 maint: bot: original URL status unknown (link) - Rose, H.E. (1984), Subrecursion. Functions and Hierarchies, Oxford logic guides, vol. 9, Oxford, New York: Clarendon Press, Oxford University Press
- Schütte, Kurt (1977), Proof theory, Grundlehren der Mathematischen Wissenschaften, vol. 225, Berlin-New York: Springer-Verlag, pp. xii+299, ISBN 3-540-07911-4, MR 0505313
- Setzer, Anton (2004), "Proof theory of Martin-Löf type theory. An Overview", Mathématiques et Sciences Humaines. Mathematics and Social Sciences (165): 59–99
- Takeuti, Gaisi (1987), Proof theory, Studies in Logic and the Foundations of Mathematics, vol. 81 (Second ed.), Amsterdam: North-Holland Publishing Co., ISBN 0-444-87943-9, MR 0882549