न्यूनतम तर्क

न्यूनतम तर्क, या न्यूनतम कलन, एक गणितीय तर्क प्रणाली है जिसे मूल रूप से Ingebrigt Johansson द्वारा विकसित किया गया था। यह एक अंतर्ज्ञानवादी तर्क और परासंगत तर्क है, जो बहिष्कृत मध्य के कानून के साथ-साथ विस्फोट के सिद्धांत (पूर्व मिथ्या क्वाडलिबेट) दोनों को अस्वीकार करता है, और इसलिए निम्नलिखित दो व्युत्पत्तियों में से कोई भी मान्य नहीं है:

$\vdash (B\lor \neg B)$

$(A\land \neg A)\vdash$

कहाँ $A$ और $B$ कोई प्रस्ताव हैं। अधिकांश रचनात्मक तर्क केवल पूर्व को अस्वीकार करते हैं, अपवर्जित मध्य का नियम। शास्त्रीय तर्कशास्त्र में, भूतपूर्व कानून भी झूठे होते हैं

$(A\land \neg A)\to B,$ :$\neg (A\lor \neg A)\to B,$ :$\neg A\to (A\to B),$ साथ ही साथ उनके वेरिएंट $A$ और $\neg A$ स्विच्ड, एक दूसरे के समतुल्य और मान्य हैं। मिनिमल लॉजिक भी उन सिद्धांतों को खारिज करता है।

स्वयंसिद्धीकरण

मिनिमल लॉजिक को अंतर्ज्ञानवादी तर्क के List_of_Hilbert_systems#Positive_propositional_calculus पर स्वयंसिद्ध किया गया है। इन दोनों लॉजिक्स को समान स्वयंसिद्धों और का उपयोग करके भाषा में तैयार किया जा सकता है तार्किक निहितार्थ $\to$, तार्किक संयोजन $\land$ और तार्किक विच्छेदन $\lor$ बुनियादी तार्किक संयोजक के रूप में, लेकिन न्यूनतम तर्क जोड़ता है falsum $\bot$भाषा के हिस्से के रूप में। वैकल्पिक रूप से, निषेध के प्रत्यक्ष अभिगृहीतों की चर्चा नीचे की गई है।

प्रमेय

यहां केवल ऐसे प्रमेय शामिल हैं जो धनात्मक कलन में पहले से ही सिद्ध नहीं किए जा सकते हैं।

निषेध परिचय

निहितार्थ और निषेध कानूनों का एक त्वरित विश्लेषण इस बात का एक अच्छा संकेत देता है कि यह तर्क, जिसमें पूर्ण विस्फोट की कमी है, क्या साबित कर सकता है और क्या नहीं।

निषेध के साथ एक भाषा में एक प्राकृतिक कथन, जैसे कि न्यूनतम तर्क, उदाहरण के लिए, निषेध परिचय का सिद्धांत है, जिससे किसी कथन का निषेध इसे मानकर और एक विरोधाभास प्राप्त करके सिद्ध होता है। औपचारिक रूप से, इसे किन्हीं दो प्रस्तावों के रूप में व्यक्त किया जा सकता है,

$(B\to (A\land \neg A))\to \neg B$.

के लिए $B$ विरोधाभास के रूप में लिया $A\land \neg A$ स्वयं, यह गैर-विरोधाभास के कानून को स्थापित करता है

$\neg (A\land \neg A)$.

कोई मानते हैं $C$भौतिक सशर्त का परिचय नियम देता है $B\to C$, वह भी कब $B$ और $C$ प्रासंगिकता तर्क संबंधित नहीं हैं। इसके साथ और निहितार्थ उन्मूलन, उपरोक्त परिचय सिद्धांत का तात्पर्य है

$(A\land \neg A)\to \neg B$,

यानी किसी भी विरोधाभास को मानते हुए, हर प्रस्ताव को नकारा जा सकता है। न्यूनतम तर्क में निषेध का परिचय संभव है, इसलिए यहाँ एक विरोधाभास भी हर दोहरे निषेध को सिद्ध करता है $\neg \neg B$. विस्फोट बाद के दोहरे निषेध को दूर करने की अनुमति देगा, लेकिन यह सिद्धांत नहीं अपनाया गया है।

इसके अलावा, उपरोक्त का उपयोग करना

${\big (}(A\lor B)\land \neg A{\big )}\to {\big (}(B\lor \neg B)\land \neg \neg B){\big )}$.

इसकी तुलना पूर्ण वियोजन न्यायवाक्य से की जानी है।

असावधानी के माध्यम से स्वयंसिद्धीकरण

सकारात्मक कलन को न्यूनतम तर्क तक विस्तारित करने की एक संभावित योजना उपचार करना है $\neg B$ एक निहितार्थ के रूप में, जिस मामले में एक तर्क के इम्प्लीकेशनल प्रोपोज़िशनल कैलकुलस से प्रमेय निषेधात्मक बयानों तक ले जाते हैं। इस कोने तक, $\bot$ एक प्रस्ताव के रूप में पेश किया जाता है, जब तक कि सिस्टम असंगत और नकारा न हो, तब तक साबित नहीं किया जा सकता $\neg B$ इसके बाद एक संक्षिप्त नाम के रूप में माना जाता है $B\to \bot$. रचनात्मक रूप से, $\bot$ एक प्रस्ताव का प्रतिनिधित्व करता है जिसके लिए विश्वास करने का कोई कारण नहीं हो सकता है।

पहले से ही चर्चा किए गए सिद्धांत सकारात्मक खंड पर प्रमेय से हो सकते हैं। निषेध परिचय, पिछले अनुभाग में लिखा गया है, केवल एक विशेष मामले के रूप में निहित है

$(B\to (A\land (A\to C)))\to (B\to C)$

कब $C=\bot$. इस तरह, न्यूनतम तर्क को नकारात्मक उन्मूलन (उर्फ विस्फोट) के बिना एक रचनात्मक तर्क के रूप में वर्णित किया जा सकता है। उपरोक्त कैन को मूड सेट करना के माध्यम से सिद्ध किया जा सकता है, जिसे एक प्रस्ताव के रूप में पढ़ा जाता है

$(A\land (A\to C))\to C$

और वास्तव में उपरोक्त का एक विशेष मामला है, जब $B$ क्या सच है। के माध्यम से निषेध की परिभाषा के साथ $\bot$, मोडस पोनेन्स कथन स्वयं उसी तरह से फिर से विशिष्ट हो सकता है, और फिर गैर-विरोधाभास सिद्धांत स्थापित करता है, जो पहले से ही ऊपर वर्णित है। कढ़ी तुल्यता सहित सभी सामान्य अंतर्ज्ञानात्मक_तर्क #ऑपरेटरों की गैर-अंतर-परिभाषा_योग्यता प्राप्त की जा सकती है। एक उदाहरण के लिए, यह महत्वपूर्ण तुल्यता पर बल देने योग्य है

$((A\lor B)\to C)\leftrightarrow ((A\to C)\land (B\to C))$,

यह व्यक्त करते हुए कि दोनों कहने के दो समान तरीके हैं $A$ और $B$ मतलब $C$. सबसे पहले, डी मॉर्गन के दो परिचित नियम प्राप्त होते हैं,

$\neg (A\lor B)\leftrightarrow (\neg A\land \neg B)$.

तीसरा मान्य डी मॉर्गन नियम भी व्युत्पन्न किया जा सकता है।

दूसरे, साथ $A$ जैसा $B\to C$ ऊपर, यह इस प्रकार है

$((B\lor (B\to C))\to C)\to C$

और यह बहिष्कृत मध्य के दोहरे निषेध को कम करता है

$\neg \neg (B\lor \neg B)$

निहितार्थ परिचय द्वारा,

$C\to (B\to C)$

इसका तात्पर्य भी है $\bot \to (B\to \bot )$ सीधे दिखा रहा है कि कैसे मानते हैं $\bot$ न्यूनतम तर्क में सभी निषेधों को सिद्ध करता है। यह ऊपर भी बताया गया है, लेकिन यहाँ इसे छोटा किया जा सकता है

$\bot \to \neg B.$

यदि असावधानी आदिम है, तो पूर्ण विस्फोट को भी कहा जा सकता है $\bot \to B$.

अधिक सिद्धांतों के माध्यम से स्वयंसिद्धीकरण

से $B\to ((B\to C)\to C)$ इस प्रकार $(((B\to C)\to C)\to D)\to (B\to D)$. इसलिए

$B\to \neg \neg B$ और

$\neg \neg \neg B\leftrightarrow \neg B$

निषेध परिचय सिद्धांत से संबंधित, से

$(A\to B)\to ((B\to C)\to (A\to C))$.

न्यूनतम तर्क विरोधाभास साबित करता है

$(A\to B)\to (\neg B\to \neg A).$

उपरोक्त सिद्धांतों को संयोजन में सकारात्मक कलन से प्रमेयों का उपयोग करके भी प्राप्त किया गया है $\bot$.

उपरोक्त दोहरे निषेध सिद्धांत को अपनाने के साथ-साथ गर्भनिरोधक सिद्धांत के साथ अंतर्ज्ञानवादी तर्क के सकारात्मक अंश पर न्यूनतम तर्क का एक वैकल्पिक स्वयंसिद्धता प्रदान करता है।

अप्रमाणिक वाक्य

सामान्यीकरण की युक्ति $\neg A$ को $A\to C$ दोहरे निषेधों से जुड़े सभी शास्त्रीय रूप से मान्य कथनों को सिद्ध करने के लिए काम नहीं करता है। ध्यान दें कि वाक्य रचनात्मक आकार का कोई भी स्कीमा $(A\to C)\to B$ साबित करने के लिए बहुत मजबूत है: अगर यह साबित करने योग्य था, तो कोई सच्चा प्रस्ताव $C$ कोई अन्य प्रस्ताव साबित करेगा $B$. अब यहाँ रुचि का एक प्रकार है जहाँ $A$ द्वारा प्रतिस्थापित किया जाए $(B\to C)$. यह दिखाता है, संभवतः आश्चर्यजनक रूप से, कि दोहरे निषेध का भोला सामान्यीकरण $\neg \neg B\to B$ इस प्रकार सिद्ध नहीं किया जा सकता।

विनती $\neg \neg (B\lor \neg B)$ न्यूनतम तर्क का प्रमेय है, जैसा है $(A\land \neg A)\to \neg \neg B$. इसलिए, पूर्ण दोहरे निषेध सिद्धांत को अपनाना $\neg \neg B\to B$ न्यूनतम तर्क में कलन को शास्त्रीय तर्क में वापस लाता है, साथ ही सभी मध्यवर्ती तर्कों को छोड़ देता है।

ऐसे प्रस्तावात्मक तर्क कथन भी हैं जो न्यूनतम तर्क में अप्राप्य हैं, लेकिन सहज रूप से धारण करते हैं। अस्वीकृत कथनों के विस्फोट के साथ, पूर्ण विस्फोट इसके विशेष मामले के बराबर है $((\neg B)\land \neg (\neg B))\to B$. बाद वाले को अस्वीकृत प्रस्तावों के लिए दोहरे निषेध उन्मूलन के रूप में अभिव्यक्त किया जा सकता है, $\neg B\to (\neg \neg B\to B)$. यह सिद्धांत तत्काल पूर्ण वियोगात्मक न्यायवाक्य को भी सिद्ध करता है। तो यह अपेक्षाकृत कमजोर स्कीमा है जो मजबूत अंतर्ज्ञानवादी तर्क के लिए अग्रणी है।

जैसा कि ऊपर देखा गया है, किसी भी प्रस्ताव के लिए डबल अस्वीकृत बहिष्कृत मध्य न्यूनतम तर्क में पहले से ही सिद्ध है। हालांकि, यह जोर देने योग्य है कि विधेय कलन में, न्यूनतम तर्क के नियम बहिष्कृत मध्य कथनों के अनंत संयोजन के दोहरे निषेध के प्रमाण को सक्षम नहीं करते हैं। दरअसल, डबल नेगेशन शिफ्ट स्कीमा (DNS)

${\big (}\forall (n\in {\mathbb {N} }).\neg \neg P(n){\big )}\to \neg \neg \forall (n\in {\mathbb {N} }).P(n)$ अंतर्ज्ञानवादी रूप से भी मान्य नहीं है और न ही है

$\neg \neg \forall (n\in {\mathbb {N} }).Q(n)\lor \neg Q(n)$.

दोहरे-निषेध_अनुवाद#परिणामों से परे, यह गैर-शास्त्रीय सिद्धांतों की अनुमति देता है।

अंतर्ज्ञानवादी तर्क से संबंध

कोई भी सूत्र केवल उपयोग कर रहा है $\land ,\lor ,\to$ न्यूनतम तर्क में सिद्ध किया जा सकता है अगर और केवल अगर यह अंतर्ज्ञानवादी तर्क में सिद्ध होता है।

विस्फोट का सिद्धांत अंतर्ज्ञानवादी तर्क में मान्य है और व्यक्त करता है कि किसी भी और सभी प्रस्तावों को प्राप्त करने के लिए, कोई भी बेतुकापन प्राप्त करके ऐसा कर सकता है। न्यूनतम तर्क में, यह सिद्धांत स्वयंसिद्ध रूप से मनमाना प्रस्तावों के लिए नहीं है। जैसा कि न्यूनतम तर्क अंतर्ज्ञानवादी तर्क के केवल सकारात्मक अंश का प्रतिनिधित्व करता है, यह अंतर्ज्ञानवादी तर्क का एक उपतंत्र है और सख्ती से कमजोर है।

संक्षेप में तैयार किया गया, अंतर्ज्ञानवादी तर्क में विस्फोट वास्तव में दोहरे निषेध उन्मूलन सिद्धांत के विशेष मामलों को अनुदान देता है जो कि न्यूनतम तर्क के पास नहीं है।

वियोगात्मक न्यायवाक्य

व्यावहारिक रूप से, अंतर्ज्ञानवादी संदर्भ में, विस्फोट का सिद्धांत वियोगात्मक न्यायवाक्य को सक्षम बनाता है:

$((A\lor B)\land \neg A)\to B.$

इसे इस प्रकार पढ़ा जा सकता है: के रचनात्मक प्रमाण को देखते हुए $A\lor B$ और रचनात्मक अस्वीकृति $A$, एक बिना शर्त के सकारात्मक मामले के विकल्प के लिए अनुमति देता है $B$. इस प्रकार, न्यायवाक्य वियोजन के लिए एक अनपैकिंग सिद्धांत है। इसे विस्फोट के औपचारिक परिणाम के रूप में देखा जा सकता है और इसका तात्पर्य भी है। ऐसा इसलिए है क्योंकि अगर $A\lor B$ सिद्ध करके सिद्ध किया था $B$ तब $B$ पहले से ही सिद्ध है, जबकि अगर $A\lor B$ सिद्ध करके सिद्ध किया था $A$, तब $B$ यह भी अनुसरण करता है, क्योंकि अंतर्ज्ञानवादी प्रणाली विस्फोट की अनुमति देती है।

उदाहरण के लिए, एक रचनात्मक तर्क दिया गया है कि एक सिक्के के पलटने का परिणाम या तो हेड या टेल होता है ($A$ या $B$), एक रचनात्मक तर्क के साथ कि परिणाम वास्तव में हेड्स नहीं था, न्यायवाक्य अभिव्यक्त करता है कि तब यह पहले से ही एक तर्क का गठन करता है कि टेल्स हुआ।

यदि अंतर्ज्ञानवादी तर्क प्रणाली को मेटालॉजिकल रूप से सुसंगत माना जाता है, तो न्यायवाक्य को यह कहते हुए पढ़ा जा सकता है कि एक रचनात्मक प्रदर्शन $A\lor B$ और $\neg A$, प्रदर्शन करने वाले अन्य गैर-तार्किक स्वयंसिद्धों के अभाव में $B$, वास्तव में का एक प्रदर्शन शामिल है $B$.

न्यूनतम तर्क में, कोई इसका प्रमाण प्राप्त नहीं कर सकता है $B$ इस प्रकार से। हालाँकि, एक ही आधार का तात्पर्य दोहरे-नकारात्मक से है $B$, अर्थात। $\neg \neg B$. यदि न्यूनतम तर्क प्रणाली को मेटालॉजिकल रूप से सुसंगत माना जाता है, तो उस निहितार्थ सूत्र को यह कहकर व्यक्त किया जा सकता है $B$ केवल अस्वीकार नहीं किया जा सकता है।

विस्फोट के कमजोर रूप वियोगात्मक न्यायवाक्य को सिद्ध करते हैं और दूसरी दिशा में, न्यायवाक्य के उदाहरण के साथ $A=\neg B$ पढ़ता $((B\lor \neg B)\land \neg \neg B)\to B$ और उन प्रस्तावों के लिए दोहरे निषेध उन्मूलन के समतुल्य है जिनके लिए बीच में बहिष्कृत किया गया है

$(B\lor \neg B)\to (\neg \neg B\to B)$.

चूंकि सामग्री सशर्त अनुदान सिद्ध प्रस्तावों के लिए डबल-निषेध उन्मूलन प्रदान करता है, यह फिर से अस्वीकृत प्रस्तावों के लिए डबल-निषेध उन्मूलन के बराबर है।

सिद्धांत में उपयोग का अंतर्ज्ञानवादी उदाहरण

निम्नलिखित Heyting अंकगणितीय प्रमेय अस्तित्व के दावों के प्रमाण के लिए अनुमति देता है जो विस्फोट सिद्धांत के बिना, इस सामान्य परिणाम के माध्यम से सिद्ध नहीं किया जा सकता है। परिणाम अनिवार्य रूप से सरल दोहरे निषेध उन्मूलन दावों का एक परिवार है, $\exists$-वाक्य एक संगणनीय विधेय को बांधता है।

होने देना $P$ कोई भी परिमाणक-मुक्त विधेय हो, और इस प्रकार सभी संख्याओं के लिए निर्णायक हो $n$, ताकि बहिष्कृत मध्य धारण करे,

$P(n)\lor \neg P(n)$.

फिर इंडक्शन द्वारा $m$,

$\forall m.\ \neg {\big (}\forall (n<m).\neg P(n){\big )}\to \exists (b<m).P(b)$

शब्दों में: संख्याओं के लिए $n$ तक सीमित दायरे में $m$, अगर इस बात से इंकार किया जा सकता है कि कोई मामला मान्य नहीं है, यानी अगर यह खारिज किया जा सकता है कि हर संख्या के लिए, मान लीजिए $n=a$, संगत प्रस्ताव $P(a)$ हमेशा अस्वीकार्य रहेगा, तो इसका तात्पर्य है कि कुछ है $n=b$ उनके बीच $n$जिसके लिए है $P(b)$ साध्य है।

जैसा कि पहले चर्चा किए गए उदाहरणों के साथ, इसके प्रमाण के लिए बिना निषेध के प्रस्तावों को प्राप्त करने के लिए पूर्ववर्ती पक्ष पर विस्फोट की आवश्यकता होती है। यदि प्रस्ताव को प्रारंभ के रूप में तैयार किया गया है $m=0$, तो यह प्रारंभिक मामला पहले से ही एक रिक्त खंड से विस्फोट का रूप देता है

$\bot \to \exists (b<0).P(b)$.

अगला मामला $m=1$ एक निर्णायक विधेय के लिए दोहरा निषेध उन्मूलन बताता है,

$\neg \neg P(0)\to P(0)$. $m=2$ h> मामला पढ़ता है

$\neg {\big (}\neg P(0)\land \neg P(1){\big )}\to {\big (}P(0)\lor P(1){\big )}$,

जो, जैसा कि पहले ही उल्लेख किया गया है, के बराबर है

$\neg \neg {\big (}P(0)\lor P(1){\big )}\to {\big (}P(0)\lor P(1){\big )}$.

दोनों $m=0$ और $m=1$ एक निर्णायक विधेय के लिए फिर से दोहरे निषेध उन्मूलन के मामले हैं। बेशक, एक बयान $\exists (b<m).P(b)$ निश्चित के लिए $m$ और $P$ न्यूनतम तर्क के सिद्धांतों का उपयोग करके, अन्य माध्यमों से सिद्ध किया जा सकता है।

एक तरफ के रूप में, सामान्य निर्णायक भविष्यवाणियों के लिए असीमित स्कीमा भी अंतर्ज्ञानवादी रूप से सिद्ध नहीं है, मार्कोव के सिद्धांत को देखें।

टाइप थ्योरी से संबंध

निषेध का प्रयोग

मूर्खता $\bot$ न केवल प्राकृतिक कटौती में प्रयोग किया जाता है, बल्कि करी-हावर्ड पत्राचार के तहत सैद्धांतिक फॉर्मूलेशन में भी प्रयोग किया जाता है। टाइप सिस्टम में, $\bot$ अक्सर खाली प्रकार के रूप में भी पेश किया जाता है।

कई संदर्भों में, $\bot$ तर्क में एक अलग स्थिरांक होने की आवश्यकता नहीं है लेकिन इसकी भूमिका को किसी भी अस्वीकृत प्रस्ताव से बदला जा सकता है। उदाहरण के लिए, इसे परिभाषित किया जा सकता है $a=b$ कहाँ $a,b$ विशिष्ट होना चाहिए। उस प्रस्ताव के लिए सबूत के अस्तित्व में न होने का दावा तब स्थिरता का दावा है।

के लिए एक उदाहरण लक्षण वर्णन $\bot$ है $0=1$ एक सिद्धांत में प्राकृतिक संख्या शामिल है। इसे सादे रचनात्मक तर्क के लिए भी अपनाया जा सकता है। इससे सिद्ध होता है $3^{4}=8$ झूठा होना, अर्थात् $\neg (3^{4}=8)$, बस साबित करने का मतलब है $(3^{4}=8)\to (0=1)$. हम नोटेशन पेश कर सकते हैं $3^{4}\neq 8$ दावे पर कब्जा करने के लिए भी। और वास्तव में, अंकगणित का प्रयोग करके, ${\tfrac {3^{4}-8}{73}}=1$ रखता है, लेकिन $(3^{4}=8)$ भी तात्पर्य है ${\tfrac {3^{4}-8}{73}}=0$. तो इसका मतलब होगा $1=0$ और इसलिए हम प्राप्त करते हैं $\neg (3^{4}=8)$. है

सरल प्रकार

कार्यात्मक प्रोग्रामिंग गणना पहले से ही मुख्य रूप से निहितार्थ संयोजी पर निर्भर करती है, उदाहरण के लिए देखें एक विधेय तर्क ढांचे के लिए निर्माण की गणना।

इस खंड में हम न्यूनतम तर्क को केवल निहितार्थ तक सीमित करके प्राप्त प्रणाली का उल्लेख करते हैं, और औपचारिक रूप से इसका वर्णन करते हैं। इसे निम्नलिखित अनुक्रमिक कलन नियमों द्वारा परिभाषित किया जा सकता है:

${\dfrac {}{\Gamma \cup \{A\}\vdash A}}{\mbox{ axiom}}$         ${\dfrac {\Gamma \cup \{A\}\vdash B}{\Gamma \vdash A\to B}}{\mbox{ intro}}$         ${\dfrac {\Gamma \vdash A\to B~~~~~~~~~~\Delta \vdash A}{\Gamma \cup \Delta \vdash B}}{\mbox{ elim.}}$

इस प्रतिबंधित न्यूनतम तर्क का प्रत्येक सूत्र सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस में एक प्रकार से मेल खाता है, देखें करी-हावर्ड पत्राचार # प्राकृतिक कटौती और लैम्ब्डा कैलकुलस | करी-हावर्ड पत्राचार। उस संदर्भ में, न्यूनतम तर्क वाक्यांश का उपयोग कभी-कभी न्यूनतम तर्क के इस प्रतिबंध के अर्थ में किया जाता है। मिनिमल लॉजिक का यह इम्प्लीकेशनल फ्रैगमेंट हिल्बर्ट सिस्टम्स की सूची के समान है#Positive_implicational_calculus|पॉजिटिव, इंप्लीकेशनल फ्रैगमेंट ऑफ इंट्यूशनिस्टिक लॉजिक चूंकि मिनिमम लॉजिक पहले से ही इंट्यूशनिस्टिक लॉजिक का पॉजिटिव फ्रैगमेंट है।

शब्दार्थ

न्यूनतम तर्क के शब्दार्थ हैं जो अंतर्ज्ञानवादी तर्क के फ्रेम-अर्थशास्त्र को प्रतिबिंबित करते हैं, पैराकंसिस्टेंट तर्क में शब्दार्थ की चर्चा देखें। यहां प्रस्तावों के लिए सत्यता और असत्यता निर्दिष्ट करने वाले मूल्यांकन कार्य कम बाधाओं के अधीन हो सकते हैं।

यह भी देखें

• अंतर्ज्ञानवादी तर्क
• परासंगत तर्क
• इम्प्लीकेशनल प्रोपोज़िशनल कैलकुलस
• तर्क प्रणालियों की सूची

संदर्भ

• A.S. Troelstra and H. Schwichtenberg, 2000, Basic Proof Theory, Cambridge University Press, ISBN 0521779111