क्रमिक विश्लेषण
प्रमाण सिद्धांत में, क्रमसूचक विश्लेषण गणितीय सिद्धांतों को उनकी शक्ति के माप के रूप में क्रमसूचक संख्या (प्रायः बड़े गणनीय क्रमसूचक) प्रदान करता है। यदि सिद्धांतों में प्रमाण-सैद्धांतिक क्रमसूचक हैं, तो वे प्रायः समानता रखते हैं, और यदि सिद्धांत में दूसरे की तुलना में बड़ा प्रमाण-सैद्धांतिक क्रमसूचक है, तो यह प्रायः दूसरे सिद्धांत की निरंतरता को प्रमाणित कर सकता है।
इतिहास
क्रमसूचक विश्लेषण के क्षेत्र का निर्माण तब हुआ, जब 1934 में गेरहार्ड जेंटजन ने आधुनिक शब्दों में यह प्रमाणित करने के लिए कटौती उन्मूलन का उपयोग किया कि पीनो अंकगणित का प्रमाण-सैद्धांतिक क्रमांक ε0 (गणित) है, जेंटजन का कंसिस्टेंसी प्रमाण देखें।
परिभाषा
क्रमसूचक विश्लेषण का संबंध सही, प्रभावी (पुनरावर्ती) सिद्धांतों से है जो अंकगणित के पर्याप्त भाग की व्याख्या क्रमसूचक संकेतन के विषय में वर्णन करने के लिए कर सकते हैं।
ऐसे सिद्धांत का प्रमाण-सैद्धांतिक क्रम सभी क्रमसूचक संकेतन के क्रम प्रकारों का सर्वोच्च है (अनिवार्य रूप से पुनरावर्ती क्रमसूचक, खंड देखें) जो सिद्धांत सिद्ध कर सकता है कि वे उत्तम रूप से स्थापित संबंध हैं - सभी क्रमसूचकों का सर्वोच्च जिसके लिए अंकन उपस्थित है क्लेन के अर्थ में ऐसा है यह प्रमाणित करता है क्रमिक संकेतन है। समान रूप से, यह सभी अध्यादेशों का सर्वोच्च है जैसे कि संगणनीय फंक्शन उपस्थित है पर (प्राकृतिक संख्याओं का समुच्चय) जो इसे क्रमसूचक के साथ व्यवस्थित करता है और ऐसा के लिए अंकगणितीय कथनों का ट्रांसफिनिट इंडक्शन प्रमाणित करता है।
साधारण अंकन
कुछ सिद्धांतों, जैसे कि दूसरे क्रम के अंकगणित के उप-प्रणालियों के पास ट्रांसफिनिट ऑर्डर के विषय में तर्क देने की कोई अवधारणा या प्रविधि नहीं है। उदाहरण के लिए, Z के उपप्रणाली के लिए इसका क्या अर्थ है, इसे औपचारिक रूप देने के लिए2 प्रमाणित करना सुव्यवस्थित , हम इसके बजाय एक क्रमसूचक संकेतन का निर्माण करते हैं आदेश प्रकार के साथ . अब विभिन्न ट्रांसफिनिट इंडक्शन सिद्धांतों के साथ काम कर सकते हैं , जो सेट-सैद्धांतिक अध्यादेशों के बारे में तर्क के लिए स्थानापन्न करता है।
हालाँकि, कुछ पैथोलॉजिकल नोटेशन सिस्टम उपस्थित हैं जिनके साथ काम करना अप्रत्याशित रूप से कठिन है। उदाहरण के लिए, राथजेन एक आदिम पुनरावर्ती संकेतन प्रणाली देता है यह अच्छी तरह से स्थापित है अगर पीए सुसंगत है,[1] आदेश प्रकार होने के बावजूद - पीए के क्रमिक विश्लेषण में इस तरह के अंकन को शामिल करने से झूठी समानता होगी .
ऊपरी बाध्य
किसी भी सिद्धांत के लिए दोनों हैं -स्वयंसिद्ध और -ध्वनि, एक पुनरावर्ती आदेश का अस्तित्व जो सिद्धांत प्रमाणित करने में विफल रहता है वह सुव्यवस्थित है बाउंडिंग प्रमेय, और कहा कि सिद्ध रूप से अच्छी तरह से स्थापित क्रमिक अंकन वास्तव में अच्छी तरह से स्थापित हैं -सुदृढ़ता। इस प्रकार एक का प्रमाण-सैद्धांतिक क्रमसूचक ध्वनि सिद्धांत जिसमें एक है स्वयंसिद्धीकरण हमेशा एक (गणनीय) पुनरावर्ती क्रमसूचक होगा, जो कि चर्च-क्लेन क्रमसूचक से कम है . [2]
उदाहरण
सिद्धांत-सिद्धांत क्रमसूचक ω के साथ सिद्धांत
- क्यू, रॉबिन्सन अंकगणित (हालांकि इस तरह के कमजोर सिद्धांतों के लिए सबूत-सैद्धांतिक क्रमसूचक की परिभाषा को बदलना होगा)[citation needed].
- कुंआ– , एक विवेकपूर्ण रूप से आदेशित रिंग के गैर-नकारात्मक भाग का प्रथम-क्रम सिद्धांत।
सिद्धांत-सिद्धांत क्रमसूचक ω के साथ सिद्धांत2
- RFA, अल्पविकसित कार्य अंकगणित।[3]
- मैं0, Δ पर प्रेरण के साथ अंकगणित0-बिना किसी स्वयंसिद्ध के भविष्यवाणी करता है कि घातांक कुल है।
सिद्धांत-सिद्धांत क्रमसूचक ω के साथ सिद्धांत3
- ईएफए, प्रारंभिक कार्य अंकगणित।
- मैं0 + ऍक्स्प, Δ पर प्रेरण के साथ अंकगणित0-एक एक्सिओम द्वारा संवर्धित विधेय जो यह दावा करता है कि घातांक कुल है।
- आरसीए*
0, ईएफए का दूसरा क्रम रूप कभी-कभी रिवर्स गणित में प्रयोग किया जाता है। - डब्ल्यूकेएल*
0, ईएफए का दूसरा क्रम रूप कभी-कभी रिवर्स गणित में प्रयोग किया जाता है।
फ्रीडमैन के भव्य अनुमान से पता चलता है कि बहुत सामान्य गणित को कमजोर प्रणालियों में सिद्ध किया जा सकता है, जो कि उनके प्रमाण-सैद्धांतिक क्रमसूचक हैं।
सिद्धांत-सिद्धांत क्रमसूचक ω के साथ सिद्धांतn (n = 2, 3, ... ω के लिए)
- पहचान0 या ईएफए एक स्वयंसिद्ध द्वारा संवर्धित है जो यह सुनिश्चित करता है कि एन-वें स्तर के प्रत्येक तत्व ग्रेज़गोर्स्की पदानुक्रम कुल है।
सिद्धांत-सिद्धांत क्रमसूचक ω के साथ सिद्धांतओ
- आरसीए0, दूसरे क्रम का अंकगणित # पुनरावर्ती समझ।
- डब्ल्यूकेएल0, उलटा गणित#कमजोर कोनिग प्रमेयिका WKL0|कमजोर कोनिग प्रमेयिका।
- PRA, आदिम पुनरावर्ती अंकगणित।
- मैं1, Σ पर प्रेरण के साथ अंकगणित1-विधेय।
प्रमाण-सैद्धांतिक क्रमसूचक ε के साथ सिद्धांत0
- पीए, पियानो अंकगणित (कट एलिमिनेशन का उपयोग करके लोग द्वारा जेंटज़ेन की स्थिरता प्रमाण)।
- एसीए0, अंकगणितीय समझ।
प्रूफ-सैद्धांतिक क्रमसूचक के साथ सिद्धांत0
- एटीआर0, अंकगणितीय ट्रांसफिनिट रिकर्सन।
- मार्टिन-लोफ प्रकार का सिद्धांत मनमाने ढंग से कई परिमित स्तर के ब्रह्मांडों के साथ।
इस क्रमसूचक को कभी-कभी विधेयात्मक सिद्धांतों की ऊपरी सीमा माना जाता है।
प्रूफ-थ्योरिटिक ऑर्डिनल के साथ सिद्धांत बाचमन-हावर्ड ऑर्डिनल
- पहचान1, पहला बुखोलज़ आईडी पदानुक्रम।
- केपी, कृप्के-प्लेटेक सेट थ्योरी विथ द इनफिनिटी ऑफ इनफिनिटी।
- CZF, Aczel का CZF|रचनात्मक ज़र्मेलो-फ्रेंकेल सेट सिद्धांत।
- ईओएन, सोलोमन फेफरमैन की स्पष्ट गणित प्रणाली टी का एक कमजोर संस्करण0.
Kripke-Platek या CZF सेट सिद्धांत सभी उपसमुच्चयों के सेट के रूप में दिए गए पूर्ण पावरसेट के लिए सिद्धांतों के बिना कमजोर सेट सिद्धांत हैं। इसके बजाय, वे या तो प्रतिबंधित पृथक्करण और नए सेटों के गठन के स्वयंसिद्ध हैं, या वे उन्हें बड़े संबंधों से अलग करने के बजाय कुछ फ़ंक्शन रिक्त स्थान (घातांक) का अस्तित्व प्रदान करते हैं।
बड़े प्रमाण-सैद्धांतिक अध्यादेशों के साथ सिद्धांत
What is the proof-theoretic ordinal of full second-order arithmetic?[4]
- , दूसरा क्रम अंकगणित | Π11 समझ में एक बड़ा प्रमाण-सैद्धांतिक क्रमसूचक है, जिसे ताकुती द्वारा क्रमसूचक आरेखों के संदर्भ में वर्णित किया गया था, और जो Psi0(Omega omega)|ψ से घिरा हुआ है0(ओहω) बुखोल्ज़ के अंकन में। का भी क्रम है , परिमित रूप से पुनरावृत्त आगमनात्मक परिभाषाओं का सिद्धांत। और अनुक्रमित W-प्रकार के साथ MLW, मार्टिन-लोफ प्रकार सिद्धांत का क्रम भी Setzer (2004).
- पहचानω, बुखोल्ज़ की आईडी पदानुक्रम | ω-पुनरावृत्त आगमनात्मक परिभाषाओं का सिद्धांत। इसका प्रमाण-सैद्धांतिक क्रमसूचक Takeuti-Feferman-Buchholz ordinal | Takeuti-Feferman-Buchholz ordinal के बराबर है।
- टी0, फेफ़रमैन की स्पष्ट गणित की रचनात्मक प्रणाली में एक बड़ा प्रूफ-सैद्धांतिक क्रमसूचक है, जो KPi का प्रूफ-सैद्धांतिक क्रमसूचक भी है, क्रिप्के-प्लेटेक सेट सिद्धांत पुनरावृत्त स्वीकार्यता के साथ और .
- केपीआई, एक स्वीकार्य क्रमसूचक पर आधारित क्रिप्के-प्लेटेक सेट सिद्धांत का एक विस्तार है, जिसमें एक बहुत बड़ा प्रमाण-सैद्धांतिक क्रमसूचक है जैगर और पोहलर्स के 1983 के पेपर में वर्णित है, जहां I सबसे छोटा दुर्गम है।[5] यह क्रमसूचक भी प्रमाण-सैद्धांतिक क्रमसूचक है .
- केपीएम, एक स्वीकार्य क्रमसूचक पर आधारित क्रिप्के-प्लेटेक सेट सिद्धांत का एक विस्तार है, जिसका एक बहुत बड़ा प्रमाण-सैद्धांतिक क्रमसूचक θ है, जिसे इसके द्वारा वर्णित किया गया था Rathjen (1990).
- एमएलएम, एक महलो-ब्रह्मांड द्वारा मार्टिन-लोफ प्रकार के सिद्धांत का एक विस्तार, एक और भी बड़ा प्रमाण-सैद्धांतिक क्रमसूचक ψ हैΩ1</ उप> (ओहM + ω).
- के बराबर एक सबूत-सैद्धांतिक क्रमसूचक है , कहाँ राथजेन के साई फ़ंक्शन का उपयोग करते हुए पहले कमजोर कॉम्पैक्ट को संदर्भित करता है
- के बराबर एक सबूत-सैद्धांतिक क्रमसूचक है , कहाँ पहले को संदर्भित करता है -अवर्णनीय और , स्टीगर्ट के साई फ़ंक्शन का उपयोग करके।
- के बराबर एक सबूत-सैद्धांतिक क्रमसूचक है कहाँ कम से कम क्रमसूचक का एक कार्डिनल एनालॉग है जो है - सभी के लिए स्थिर और , स्टीगर्ट के साई फ़ंक्शन का उपयोग करके।
प्राकृतिक संख्याओं के पावर सेट का वर्णन करने में सक्षम अधिकांश सिद्धांतों में सबूत-सैद्धांतिक अध्यादेश हैं जो इतने बड़े हैं कि अभी तक कोई स्पष्ट संयोजक विवरण नहीं दिया गया है। यह भी शामिल है , पूरे दूसरे क्रम का अंकगणित () और ज़र्मेलो-फ्रेंकेल सेट थ्योरी और ZFC सहित पॉवरसेट के साथ सिद्धांतों को सेट करें। अंतर्ज्ञानवादी तर्क ZF (IZF) की ताकत ZF के बराबर है।
क्रमिक विश्लेषण की तालिका
Ordinal | First-order arithmetic | Second-order arithmetic | Kripke-Platek set theory | Type theory | Constructive set theory | Explicit mathematics |
---|---|---|---|---|---|---|
, | ||||||
, | ||||||
, | , | |||||
[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 का विस्तार करता है।
- वास्तव में प्रथम-क्रम अंकगणितीय प्रणाली नहीं है, लेकिन प्राकृतिक संख्याओं के आधार पर भविष्यवाणिय तर्क द्वारा प्राप्त की जा सकने वाली चीज़ों को कैप्चर करता है।
- पर एक automorphism है .
- मोनोटोन ऑपरेटरों के ν पुनरावृत्त कम से कम निश्चित बिंदुओं द्वारा PA का विस्तार करता है।
- वास्तव में एक प्रथम-क्रम अंकगणितीय प्रणाली नहीं है, लेकिन ν-बार पुनरावृत्त सामान्यीकृत आगमनात्मक परिभाषाओं के आधार पर विधेय तर्क द्वारा प्राप्त किया जा सकता है।
- पर एक ऑटोमोर्फिज्म है .
- का कमजोर संस्करण है डब्ल्यू प्रकार के आधार पर।
- दूसरे क्रम का अंकगणित
- का दूसरा क्रम रूप है कभी-कभी रिवर्स गणित में प्रयोग किया जाता है।
- का दूसरा क्रम रूप है कभी-कभी रिवर्स गणित में प्रयोग किया जाता है।
- दूसरे क्रम का अंकगणित # पुनरावर्ती समझ है।
- उलटा गणित है#कमजोर कोनिग प्रमेयिका WKL0|कमजोर कोनिग प्रमेयिका।
- द्वितीय क्रम अंकगणित # अंकगणितीय समझ है।
- है साथ ही पूर्ण द्वितीय-क्रम प्रेरण योजना।
- उलटा गणित है #अंकगणितीय ट्रांसफिनिट रिकर्सन ATR0.
- है साथ ही पूर्ण द्वितीय-क्रम प्रेरण योजना।
- है साथ ही दावा हर सच है -मानकों के साथ वाक्य एक (गणनीय कोडित) में होता है -का मॉडल .
- कृपके-प्लेटक समुच्चय सिद्धांत
- Kripke-Platek सेट सिद्धांत है | अनंत के स्वयंसिद्ध के साथ Kripke-Platek सेट सिद्धांत।
- क्रिप्के-प्लेटेक समुच्चय सिद्धांत है, जिसका ब्रह्माण्ड एक स्वीकार्य समुच्चय है .
- का कमजोर संस्करण है डब्ल्यू प्रकार के आधार पर।
- दावा करता है कि ब्रह्मांड स्वीकार्य सेट की एक सीमा है।
- का कमजोर संस्करण है डब्ल्यू प्रकार के आधार पर।
- दावा करता है कि ब्रह्मांड अप्राप्य सेट है।
- दावा करता है कि ब्रह्मांड अति दुर्गम है: एक दुर्गम सेट और दुर्गम सेट की एक सीमा।
- दावा करता है कि ब्रह्मांड एक महलो सेट है।
- है एक निश्चित प्रथम-क्रम प्रतिबिंब योजना द्वारा संवर्धित।
- 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