प्राकृतिक कटौती

तर्क और प्रमाण सिद्धांत में, प्राकृतिक कटौती एक प्रकार का प्रमाण गणना है जिसमें तार्किक तर्क को तर्क के प्राकृतिक तरीके से निकटता से संबंधित अनुमान नियमों द्वारा व्यक्त किया जाता है। यह हिल्बर्ट-शैली प्रणालियों के विपरीत है, जो निगमनात्मक तर्क के तार्किक नियमों को व्यक्त करने के लिए यथासंभव स्वयंसिद्धों का उपयोग करते हैं।

प्रेरणा

प्राकृतिक कटौती, डेविड हिल्बर्ट, भगवान का शुक्र है फ्रीज और बर्ट्रेंड रसेल (देखें, उदाहरण के लिए, हिल्बर्ट प्रणाली) की प्रणालियों के लिए सामान्य कटौतीत्मक तर्क के स्वयंसिद्धीकरण के साथ असंतोष के संदर्भ से विकसित हुई। इस तरह के स्वयंसिद्धीकरणों का सबसे प्रसिद्ध उपयोग बर्ट्रेंड रसेल और अल्फ्रेड नॉर्थ व्हाइटहेड ने अपने गणितीय ग्रंथ गणितीय सिद्धांत में किया था। 1926 में पोलैंड में जैन लुकासिविक्ज़|लुकासिविज़ द्वारा सेमिनारों की एक श्रृंखला से प्रेरित होकर, जिसमें तर्क के अधिक प्राकृतिक उपचार की वकालत की गई, स्टैनिस्लाव जस्कॉस्की|जाकोव्स्की ने अधिक प्राकृतिक कटौती को परिभाषित करने के शुरुआती प्रयास किए, पहले 1929 में एक आरेखीय संकेतन का उपयोग करके, और बाद में 1934 और 1935 में पत्रों के अनुक्रम में अपने प्रस्ताव को अद्यतन किया। उनके प्रस्तावों ने विभिन्न धारणाओं को जन्म दिया जैसे कि फिच-शैली कैलकुलस (या फिच के आरेख) या पैट्रिक सपेस की विधि जिसके लिए जॉन लेमन ने सिस्टम एल नामक एक संस्करण दिया।

अपने आधुनिक रूप में प्राकृतिक कटौती को स्वतंत्र रूप से जर्मन गणितज्ञ गेरहार्ड जेंटज़न द्वारा 1933 में गौटिंगेन विश्वविद्यालय के गणितीय विज्ञान संकाय को दिए गए एक शोध प्रबंध में प्रस्तावित किया गया था। प्राकृतिक कटौती शब्द (या बल्कि, इसके जर्मन समकक्ष नैचुर्लिचेस श्लीसेन) उस पेपर में गढ़ा गया था:

Ich wollte nun zunächst einmal einen Formalismus aufstellen, der dem wirklichen Schließen möglichst nahe kommt. So ergab sich ein "Kalkül des natürlichen Schließens".

First I wished to construct a formalism that comes as close as possible to actual reasoning. Thus arose a "calculus of natural deduction".

जेंटज़ेन संख्या सिद्धांत की स्थिरता स्थापित करने की इच्छा से प्रेरित थे। वह निरंतरता परिणाम के लिए आवश्यक मुख्य परिणाम, कट उन्मूलन प्रमेय - हाउपट्सत्ज़ - को सीधे प्राकृतिक कटौती के लिए साबित करने में असमर्थ था। इस कारण से उन्होंने अपनी वैकल्पिक प्रणाली, अनुक्रमिक कैलकुलस की शुरुआत की, जिसके लिए उन्होंने शास्त्रीय तर्क और अंतर्ज्ञानवादी तर्क दोनों के लिए हाउपत्सत्ज़ को सिद्ध किया। 1961 और 1962 में सेमिनारों की एक श्रृंखला में डैग प्रवित्ज़ ने प्राकृतिक कटौती गणना का एक व्यापक सारांश दिया, और क्रमिक गणना के साथ जेंटज़ेन के अधिकांश काम को प्राकृतिक कटौती ढांचे में पहुँचाया। उनका 1965 का मोनोग्राफ नेचुरल डिडक्शन: एक प्रमाण-सैद्धांतिक अध्ययन प्राकृतिक कटौती पर एक संदर्भ कार्य बनना था, और इसमें मोडल तर्क और दूसरे-क्रम लॉजिक के अनुप्रयोग शामिल थे।

प्राकृतिक कटौती में, अनुमान नियमों को बार-बार लागू करके परिसर के संग्रह से एक प्रस्ताव निकाला जाता है। इस लेख में प्रस्तुत प्रणाली जेंटज़ेन या प्रविट्ज़ के फॉर्मूलेशन का एक छोटा सा बदलाव है, लेकिन पेर मार्टिन-लोफ के तार्किक निर्णय और संयोजकों के विवरण के करीब से पालन के साथ है।

निर्णय और प्रस्ताव

निर्णय (गणितीय तर्क) कुछ ऐसा है जो जानने योग्य है, अर्थात ज्ञान की वस्तु है। यदि कोई वास्तव में इसे जानता है तो यह स्पष्ट है। इस प्रकार वर्षा हो रही है यह एक निर्णय है, जो उस व्यक्ति के लिए स्पष्ट है जो जानता है कि वास्तव में वर्षा हो रही है; इस मामले में कोई भी व्यक्ति खिड़की से बाहर देखकर या घर से बाहर निकलकर आसानी से फैसले के लिए सबूत पा सकता है। हालाँकि, गणितीय तर्क में, साक्ष्य अक्सर प्रत्यक्ष रूप से देखने योग्य नहीं होते हैं, बल्कि अधिक बुनियादी स्पष्ट निर्णयों से निकाले जाते हैं। कटौती की प्रक्रिया ही प्रमाण बनती है; दूसरे शब्दों में, यदि किसी के पास इसके लिए कोई सबूत है तो निर्णय स्पष्ट होता है।

तर्कशास्त्र में सबसे महत्वपूर्ण निर्णय 'ए' सत्य के रूप में होते हैं। अक्षर A किसी प्रस्ताव का प्रतिनिधित्व करने वाली किसी भी अभिव्यक्ति को दर्शाता है; इस प्रकार सत्य निर्णयों के लिए अधिक आदिम निर्णय की आवश्यकता होती है: ए एक प्रस्ताव है। कई अन्य निर्णयों का अध्ययन किया गया है; उदाहरण के लिए, A गलत है (शास्त्रीय तर्क देखें), A समय t पर सत्य है (लौकिक तर्क देखें), A आवश्यक रूप से सत्य है या A संभवतः सत्य है (अस्थायी तर्क देखें), प्रोग्राम M का प्रकार τ है (प्रोग्रामिंग भाषाएँ देखें और प्रकार सिद्धांत), ए उपलब्ध संसाधनों से प्राप्त किया जा सकता है (रेखीय तर्क देखें), और कई अन्य। आरंभ करने के लिए, हम सबसे सरल दो निर्णयों पर ध्यान देंगे A एक प्रस्ताव है और A सत्य है, जिन्हें क्रमशः A प्रोप और A सत्य के रूप में संक्षिप्त किया गया है।

निर्णय ए प्रोप ए के वैध प्रमाणों की संरचना को परिभाषित करता है, जो बदले में प्रस्तावों की संरचना को परिभाषित करता है। इस कारण से, इस निर्णय के अनुमान नियमों को कभी-कभी गठन नियम के रूप में जाना जाता है। उदाहरण के लिए, यदि हमारे पास दो प्रस्ताव ए और बी हैं (अर्थात, निर्णय ए प्रोप और बी प्रोप स्पष्ट हैं), तो हम संयुक्त प्रस्ताव ए और बी बनाते हैं, जिसे प्रतीकात्मक रूप से लिखा जाता है$A\wedge B$. इसे हम अनुमान नियम के रूप में लिख सकते हैं:

${\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{(A\wedge B){\hbox{ prop}}}}\ \wedge _{F}$

जहां अनुमान नियम को अधिक संक्षिप्त बनाने के लिए कोष्ठक हटा दिए गए हैं:

${\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\wedge B{\hbox{ prop}}}}\ \wedge _{F}$

यह अनुमान नियम योजनाबद्ध है: ए और बी को किसी भी अभिव्यक्ति के साथ त्वरित किया जा सकता है। अनुमान नियम का सामान्य रूप है:

${\frac {J_{1}\qquad J_{2}\qquad \cdots \qquad J_{n}}{J}}\ {\hbox{name}}$

जहां प्रत्येक $J_{i}$ एक निर्णय है और अनुमान नियम को नाम दिया गया है। रेखा के ऊपर के निर्णयों को परिसर के रूप में जाना जाता है, और रेखा के नीचे के निर्णयों को निष्कर्ष के रूप में जाना जाता है। अन्य सामान्य तार्किक प्रस्ताव विच्छेदन हैं ($A\vee B$), निषेध ($\neg A$), निहितार्थ ($A\supset B$), और तार्किक स्थिरांक सत्य ($\top$) और झूठ ($\bot$). इनके गठन के नियम नीचे हैं.

${\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\vee B{\hbox{ prop}}}}\ \vee _{F}\qquad {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\supset B{\hbox{ prop}}}}\ \supset _{F}$

${\frac {\hbox{ }}{\top {\hbox{ prop}}}}\ \top _{F}\qquad {\frac {\hbox{ }}{\bot {\hbox{ prop}}}}\ \bot _{F}\qquad {\frac {A{\hbox{ prop}}}{\neg A{\hbox{ prop}}}}\ \neg _{F}$

परिचय और उन्मूलन

अब हम सच्चे निर्णय पर चर्चा करते हैं। अनुमान नियम जो निष्कर्ष में एक तार्किक संयोजक का परिचय देते हैं उन्हें परिचय नियम के रूप में जाना जाता है। संयोजनों का परिचय देने के लिए, यानी, प्रस्ताव ए और बी के लिए ए और बी सत्य का निष्कर्ष निकालने के लिए, किसी को ए सत्य और बी सत्य के लिए साक्ष्य की आवश्यकता होती है। एक अनुमान नियम के रूप में:

${\frac {A{\hbox{ true}}\qquad B{\hbox{ true}}}{(A\wedge B){\hbox{ true}}}}\ \wedge _{I}$

यह समझना चाहिए कि ऐसे नियमों में वस्तुएँ प्रस्ताव हैं। अर्थात्, उपरोक्त नियम वास्तव में इसका संक्षिप्त रूप है:

${\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}\qquad A{\hbox{ true}}\qquad B{\hbox{ true}}}{(A\wedge B){\hbox{ true}}}}\ \wedge _{I}$

यह भी लिखा जा सकता है:

${\frac {A\wedge B{\hbox{ prop}}\qquad A{\hbox{ true}}\qquad B{\hbox{ true}}}{(A\wedge B){\hbox{ true}}}}\ \wedge _{I}$

इस रूप में प्रथम आधार को संतुष्ट किया जा सकता है $\wedge _{F}$ गठन नियम, पिछले फॉर्म के पहले दो परिसर दे रहा है। इस लेख में हम उन प्रोप निर्णयों को विस्तार से बताएंगे जहां उन्हें समझा जाता है। निरर्थक मामले में, कोई भी बिना किसी आधार के सत्य प्राप्त कर सकता है।

${\frac {\ }{\top {\hbox{ true}}}}\ \top _{I}$

यदि किसी प्रस्ताव की सत्यता को एक से अधिक तरीकों से स्थापित किया जा सकता है, तो संबंधित संयोजक में कई परिचय नियम होते हैं।

${\frac {A{\hbox{ true}}}{A\vee B{\hbox{ true}}}}\ \vee _{I1}\qquad {\frac {B{\hbox{ true}}}{A\vee B{\hbox{ true}}}}\ \vee _{I2}$

ध्यान दें कि अशक्त मामले में, यानी झूठ के लिए, कोई परिचय नियम नहीं हैं। इस प्रकार कोई भी सरल निर्णयों से कभी भी झूठ का अनुमान नहीं लगा सकता।

दोहरे से परिचय नियम उन्मूलन नियम हैं जो यह वर्णन करते हैं कि किसी यौगिक प्रस्ताव के बारे में जानकारी को उसके घटकों के बारे में जानकारी में कैसे विघटित किया जाए। इस प्रकार, A ∧ B true से, हम यह निष्कर्ष निकाल सकते हैं कि A सत्य है और B सत्य है:

${\frac {A\wedge B{\hbox{ true}}}{A{\hbox{ true}}}}\ \wedge _{E1}\qquad {\frac {A\wedge B{\hbox{ true}}}{B{\hbox{ true}}}}\ \wedge _{E2}$

अनुमान नियमों के उपयोग के एक उदाहरण के रूप में, संयोजन की क्रमविनिमेयता पर विचार करें। यदि A ∧ B सत्य है, तो B ∧ A सत्य है; यह व्युत्पत्ति अनुमान नियमों को इस तरह से बनाकर निकाली जा सकती है कि निचले अनुमान का परिसर अगले उच्च अनुमान के निष्कर्ष से मेल खाता हो।

${\cfrac {{\cfrac {A\wedge B{\hbox{ true}}}{B{\hbox{ true}}}}\ \wedge _{E2}\qquad {\cfrac {A\wedge B{\hbox{ true}}}{A{\hbox{ true}}}}\ \wedge _{E1}}{B\wedge A{\hbox{ true}}}}\ \wedge _{I}$

अब तक हमने जो अनुमान आंकड़े देखे हैं, वे निहितार्थ परिचय या विच्छेदन उन्मूलन के नियमों को बताने के लिए पर्याप्त नहीं हैं; इनके लिए, हमें काल्पनिक व्युत्पत्ति की अधिक सामान्य धारणा की आवश्यकता है।

काल्पनिक व्युत्पत्तियाँ

गणितीय तर्क में एक व्यापक ऑपरेशन मान्यताओं से तर्क करना है। उदाहरण के लिए, निम्नलिखित व्युत्पत्ति पर विचार करें:

${\cfrac {A\wedge \left(B\wedge C\right){\hbox{ true}}}{{\cfrac {B\wedge C{\hbox{ true}}}{B{\hbox{ true}}}}\ \wedge _{E1}}}\ \wedge _{E2}$

यह व्युत्पत्ति बी की सच्चाई को इस तरह स्थापित नहीं करती है; बल्कि, यह निम्नलिखित तथ्य स्थापित करता है:

यदि A ∧ (B ∧ C) सत्य है तो B सत्य है।

तर्क में, कोई कहता है कि A ∧ (B ∧ C) सत्य है, हम दिखाते हैं कि B सत्य है; दूसरे शब्दों में, निर्णय बी सत्य कल्पित निर्णय ए ∧ (बी ∧ सी) सत्य पर निर्भर करता है। यह एक काल्पनिक व्युत्पत्ति है, जिसे हम इस प्रकार लिखते हैं:

${\begin{matrix}A\wedge \left(B\wedge C\right){\hbox{ true}}\\\vdots \\B{\hbox{ true}}\end{matrix}}$

व्याख्या यह है: B true, A ∧ (B ∧ C) true से व्युत्पन्न है। बेशक, इस विशिष्ट उदाहरण में हम वास्तव में A ∧ (B ∧ C) true से B true की व्युत्पत्ति जानते हैं, लेकिन सामान्य तौर पर हम व्युत्पत्ति को पहले से नहीं जानते होंगे। काल्पनिक व्युत्पत्ति का सामान्य रूप है:

${\begin{matrix}D_{1}\quad D_{2}\ \cdots \ D_{n}\\\vdots \\J\end{matrix}}$

प्रत्येक काल्पनिक व्युत्पत्ति में पूर्ववर्ती व्युत्पत्तियों का संग्रह होता है (डी_i) शीर्ष पंक्ति पर लिखा है, और एक अनुवर्ती निर्णय (जे) नीचे की पंक्ति पर लिखा है। प्रत्येक परिसर स्वयं एक काल्पनिक व्युत्पत्ति हो सकता है। (सरलता के लिए, हम किसी निर्णय को आधार-रहित व्युत्पत्ति के रूप में लेते हैं।)

काल्पनिक निर्णय की धारणा को निहितार्थ के संयोजक के रूप में आंतरिक किया गया है। परिचय और उन्मूलन नियम इस प्रकार हैं।

${\cfrac {\begin{matrix}{\cfrac {}{A{\hbox{ true}}}}\ u\\\vdots \\B{\hbox{ true}}\end{matrix}}{A\supset B{\hbox{ true}}}}\ \supset _{I^{u}}\qquad {\cfrac {A\supset B{\hbox{ true}}\quad A{\hbox{ true}}}{B{\hbox{ true}}}}\ \supset _{E}$

परिचय नियम में यू नामक पूर्ववृत्त को निष्कर्ष में हटा दिया जाता है। यह परिकल्पना के दायरे को सीमित करने के लिए एक तंत्र है: इसके अस्तित्व का एकमात्र कारण बी को सत्य स्थापित करना है; इसका उपयोग किसी अन्य उद्देश्य के लिए नहीं किया जा सकता है, और विशेष रूप से, इसका उपयोग परिचय के नीचे नहीं किया जा सकता है। उदाहरण के तौर पर, A ⊃ (B ⊃ (A ∧ B)) की व्युत्पत्ति पर विचार करें:

${\cfrac {{\cfrac {{\cfrac {}{A{\hbox{ true}}}}\ u\quad {\cfrac {}{B{\hbox{ true}}}}\ w}{A\wedge B{\hbox{ true}}}}\ \wedge _{I}}{{\cfrac {B\supset \left(A\wedge B\right){\hbox{ true}}}{A\supset \left(B\supset \left(A\wedge B\right)\right){\hbox{ true}}}}\ \supset _{I^{u}}}}\ \supset _{I^{w}}$

इस पूर्ण व्युत्पत्ति का कोई असंतुष्ट आधार नहीं है; हालाँकि, उप-व्युत्पत्तियाँ काल्पनिक हैं। उदाहरण के लिए, B ⊃ (A ∧ B) सत्य की व्युत्पत्ति पूर्ववर्ती A सत्य (जिसे u नाम दिया गया है) के साथ काल्पनिक है।

काल्पनिक व्युत्पत्तियों के साथ, अब हम विच्छेदन के लिए विलोपन नियम लिख सकते हैं:

${\cfrac {A\vee B{\hbox{ true}}\quad {\begin{matrix}{\cfrac {}{A{\hbox{ true}}}}\ u\\\vdots \\C{\hbox{ true}}\end{matrix}}\quad {\begin{matrix}{\cfrac {}{B{\hbox{ true}}}}\ w\\\vdots \\C{\hbox{ true}}\end{matrix}}}{C{\hbox{ true}}}}\ \vee _{E^{u,w}}$

शब्दों में, यदि A ∨ B सत्य है, और हम A सत्य और B सत्य दोनों से C सत्य प्राप्त कर सकते हैं, तो C वास्तव में सत्य है। ध्यान दें कि यह नियम A true या B true के लिए प्रतिबद्ध नहीं है। शून्य-एरी मामले में, यानी झूठ के लिए, हम निम्नलिखित उन्मूलन नियम प्राप्त करते हैं:

${\frac {\perp {\hbox{ true}}}{C{\hbox{ true}}}}\ \perp _{E}$

इसे इस प्रकार पढ़ा जाता है: यदि झूठ सत्य है, तो कोई भी प्रस्ताव C सत्य है।

निषेध निहितार्थ के समान है।

${\cfrac {\begin{matrix}{\cfrac {}{A{\hbox{ true}}}}\ u\\\vdots \\p{\hbox{ true}}\end{matrix}}{\lnot A{\hbox{ true}}}}\ \lnot _{I^{u,p}}\qquad {\cfrac {\lnot A{\hbox{ true}}\quad A{\hbox{ true}}}{C{\hbox{ true}}}}\ \lnot _{E}$

परिचय नियम परिकल्पना यू के नाम और अनुवर्ती पी दोनों को निर्वहन करता है, यानी, प्रस्ताव पी निष्कर्ष ए में नहीं होना चाहिए। चूंकि ये नियम योजनाबद्ध हैं, इसलिए परिचय नियम की व्याख्या है: यदि ए से सच है तो हम कर सकते हैं प्रत्येक प्रस्ताव p के लिए यह निष्कर्ष निकालें कि p सत्य है, तो A असत्य होना चाहिए, अर्थात, A सत्य नहीं है। उन्मूलन के लिए, यदि ए और ए नहीं दोनों को सत्य दिखाया जाता है, तो एक विरोधाभास होता है, जिस स्थिति में प्रत्येक प्रस्ताव सी सत्य होता है। क्योंकि निहितार्थ और निषेध के नियम बहुत समान हैं, इसलिए यह देखना काफी आसान होना चाहिए कि ए और ए ⊃ ⊥ समतुल्य नहीं हैं, यानी, प्रत्येक दूसरे से व्युत्पन्न है।

संगति, पूर्णता, और सामान्य रूप

एक सिद्धांत (गणितीय तर्क) को सुसंगत कहा जाता है यदि झूठ सिद्ध नहीं किया जा सकता है (बिना किसी धारणा के) और पूर्ण है यदि प्रत्येक प्रमेय या उसका निषेध तर्क के अनुमान नियमों का उपयोग करके सिद्ध किया जा सकता है। ये संपूर्ण तर्क के बारे में कथन हैं, और आमतौर पर एक मॉडल सिद्धांत की कुछ धारणा से जुड़े होते हैं। हालाँकि, स्थिरता और पूर्णता की स्थानीय धारणाएँ हैं जो अनुमान नियमों पर विशुद्ध रूप से वाक्यात्मक जाँच हैं, और मॉडलों के लिए किसी अपील की आवश्यकता नहीं है। इनमें से पहला स्थानीय स्थिरता है, जिसे स्थानीय रिड्यूसिबिलिटी के रूप में भी जाना जाता है, जो कहता है कि किसी भी व्युत्पत्ति में एक संयोजक का परिचय होता है जिसके तुरंत बाद उसका उन्मूलन होता है, जिसे इस चक्कर के बिना समकक्ष व्युत्पत्ति में बदला जा सकता है। यह उन्मूलन नियमों की ताकत की जाँच है: उन्हें इतना मजबूत नहीं होना चाहिए कि उनमें वह ज्ञान शामिल हो जो पहले से ही उनके परिसर में शामिल नहीं है। उदाहरण के तौर पर, संयोजकों पर विचार करें।

${\begin{aligned}{\cfrac {{\cfrac {{\cfrac {}{A\ {\text{true}}}}u\qquad {\cfrac {}{B\ {\text{true}}}}w}{A\wedge B\ {\text{true}}}}\wedge _{I}}{A\ {\text{true}}}}\wedge _{E1}\end{aligned}}\quad \Rightarrow \quad {\cfrac {}{A\ {\text{true}}}}u$

दोहरी रूप से, स्थानीय पूर्णता का कहना है कि उन्मूलन नियम इतने मजबूत हैं कि किसी संयोजक को उसके परिचय नियम के लिए उपयुक्त रूपों में विघटित कर सकते हैं। संयोजनों के लिए फिर से:

${\cfrac {}{A\wedge B\ {\text{true}}}}u\quad \Rightarrow \quad {\begin{aligned}{\cfrac {{\cfrac {{\cfrac {}{A\wedge B\ {\text{true}}}}u}{A\ {\text{true}}}}\wedge _{E1}\qquad {\cfrac {{\cfrac {}{A\wedge B\ {\text{true}}}}u}{B\ {\text{true}}}}\wedge _{E2}}{A\wedge B\ {\text{true}}}}\wedge _{I}\end{aligned}}$

ये धारणाएं करी-हावर्ड का उपयोग करते हुए लैम्ब्डा कैलकुलस में लैम्ब्डा कैलकुलस#.CE.B2-रिडक्शन|β-रिडक्शन (बीटा रिडक्शन) और लैम्ब्डा कैलकुलस#.CE.B7-कन्वर्ज़न|η-कन्वर्ज़न (eta रूपांतरण) से बिल्कुल मेल खाती हैं। समरूपता. स्थानीय पूर्णता से, हम देखते हैं कि प्रत्येक व्युत्पत्ति को एक समतुल्य व्युत्पत्ति में परिवर्तित किया जा सकता है जहां प्रमुख संयोजक पेश किया गया है। वास्तव में, यदि संपूर्ण व्युत्पत्ति परिचय के बाद निष्कासन के इस क्रम का पालन करती है, तो इसे सामान्य कहा जाता है। सामान्य व्युत्पत्ति में सभी विलोपन परिचय के ऊपर होते हैं। अधिकांश तर्कशास्त्रों में, प्रत्येक व्युत्पत्ति में एक समतुल्य सामान्य व्युत्पत्ति होती है, जिसे सामान्य रूप (सार पुनर्लेखन) कहा जाता है। सामान्य रूपों के अस्तित्व को आम तौर पर केवल प्राकृतिक कटौती का उपयोग करके साबित करना कठिन होता है, हालांकि ऐसे विवरण साहित्य में मौजूद हैं, विशेष रूप से 1961 में डैग प्रविट्ज़ द्वारा। कटौती उन्मूलन | कट-फ्री अनुक्रमिक कैलकुलस प्रस्तुति के माध्यम से इसे अप्रत्यक्ष रूप से दिखाना बहुत आसान है।

प्रथम और उच्च-क्रम एक्सटेंशन

प्रथम-क्रम प्रणाली का सारांश

पिछले अनुभाग का तर्क एकल-क्रमबद्ध तर्क का एक उदाहरण है, यानी, एक ही प्रकार की वस्तु वाला तर्क: प्रस्ताव। इस सरल ढांचे के कई विस्तार प्रस्तावित किए गए हैं; इस खंड में हम इसे दूसरे प्रकार के व्यक्तियों या पद (तर्क) के साथ विस्तारित करेंगे। अधिक सटीक रूप से, हम एक नए प्रकार का निर्णय जोड़ेंगे, t एक शब्द है (या t पद) जहां t योजनाबद्ध है। हम चरों का एक गणनीय सेट V, फ़ंक्शन प्रतीकों का एक और गणनीय सेट F तय करेंगे, और निम्नलिखित गठन नियमों के साथ शब्दों का निर्माण करेंगे:

${\frac {v\in V}{v{\hbox{ term}}}}{\hbox{ var}}_{F}$

और

${\frac {f\in F\qquad t_{1}{\hbox{ term}}\qquad t_{2}{\hbox{ term}}\qquad \cdots \qquad t_{n}{\hbox{ term}}}{f(t_{1},t_{2},\cdots ,t_{n}){\hbox{ term}}}}{\hbox{ app}}_{F}$

प्रस्तावों के लिए, हम विधेय (गणितीय तर्क) के तीसरे गणनीय सेट पी पर विचार करते हैं, और निम्नलिखित गठन नियम के साथ परमाणु विधेय को परिभाषित करते हैं:

${\frac {\phi \in P\qquad t_{1}{\hbox{ term}}\qquad t_{2}{\hbox{ term}}\qquad \cdots \qquad t_{n}{\hbox{ term}}}{\phi (t_{1},t_{2},\cdots ,t_{n}){\hbox{ prop}}}}{\hbox{ pred}}_{F}$

गठन के पहले दो नियम एक शब्द की परिभाषा प्रदान करते हैं जो प्रभावी रूप से शब्द बीजगणित और मॉडल सिद्धांत में परिभाषित परिभाषा के समान है, हालांकि अध्ययन के उन क्षेत्रों का फोकस प्राकृतिक कटौती से काफी अलग है। गठन का तीसरा नियम परमाणु सूत्र को प्रभावी ढंग से परिभाषित करता है, जैसा कि प्रथम-क्रम तर्क में, और फिर मॉडल सिद्धांत में।

इनमें गठन नियमों की एक जोड़ी जोड़ी गई है, जो परिमाणक (तर्क) प्रस्तावों के लिए अंकन को परिभाषित करती है; सार्वभौमिक (∀) और अस्तित्वगत (∃) परिमाणीकरण के लिए एक:

${\frac {x\in V\qquad A{\hbox{ prop}}}{\forall x.A{\hbox{ prop}}}}\;\forall _{F}\qquad \qquad {\frac {x\in V\qquad A{\hbox{ prop}}}{\exists x.A{\hbox{ prop}}}}\;\exists _{F}$

सार्वभौमिक परिमाणक में परिचय और उन्मूलन नियम हैं:

${\cfrac {\begin{array}{c}{\cfrac {}{a{\text{ term}}}}{\text{ u}}\\\vdots \\{}[a/x]A{\text{ true}}\end{array}}{\forall x.A{\text{ true}}}}\;\forall _{I^{u,a}}\qquad \qquad {\frac {\forall x.A{\text{ true}}\qquad t{\text{ term}}}{[t/x]A{\text{ true}}}}\;\forall _{E}$

अस्तित्वगत परिमाणक में परिचय और उन्मूलन नियम हैं:

${\frac {[t/x]A{\hbox{ true}}}{\exists x.A{\hbox{ true}}}}\;\exists _{I}\qquad \qquad {\cfrac {\begin{array}{cc}&\underbrace {\,{\cfrac {}{a{\hbox{ term}}}}{\hbox{ u}}\quad {\cfrac {}{[a/x]A{\hbox{ true}}}}{\hbox{ v}}\,} \\&\vdots \\\exists x.A{\hbox{ true}}\quad &C{\hbox{ true}}\\\end{array}}{C{\hbox{ true}}}}\exists _{E^{a,u,v}}$

इन नियमों में, अंकन [t/x] A, कैप्चर से बचने के लिए, A में x के प्रत्येक (दृश्यमान) उदाहरण के लिए t के प्रतिस्थापन को दर्शाता है। जैसा कि पहले नाम पर सुपरस्क्रिप्ट उन घटकों के लिए खड़े होते हैं जिन्हें डिस्चार्ज किया जाता है: शब्द a ∀I के निष्कर्ष में नहीं हो सकता है (ऐसे शब्दों को eigenvariables या पैरामीटर के रूप में जाना जाता है), और ∃E में u और v नामक परिकल्पनाओं को स्थानीयकृत किया जाता है एक काल्पनिक व्युत्पत्ति में दूसरा आधार. हालाँकि पहले अनुभागों का प्रस्तावात्मक तर्क निर्णयात्मकता (तर्क) था, लेकिन क्वांटिफ़ायर जोड़ने से तर्क अनिर्णीत हो जाता है।

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

${\cfrac {\begin{matrix}{\cfrac {}{p{\hbox{ prop}}}}{\hbox{ u}}\\\vdots \\A{\hbox{ prop}}\\\end{matrix}}{\forall p.A{\hbox{ prop}}}}\;\forall _{F^{u}}\qquad \qquad {\cfrac {\begin{matrix}{\cfrac {}{p{\hbox{ prop}}}}{\hbox{ u}}\\\vdots \\A{\hbox{ prop}}\\\end{matrix}}{\exists p.A{\hbox{ prop}}}}\;\exists _{F^{u}}$

उच्च-क्रम तर्क के लिए परिचय और उन्मूलन प्रपत्रों की चर्चा इस लेख के दायरे से बाहर है। प्रथम-क्रम और उच्च-क्रम तर्कशास्त्र के बीच होना संभव है। उदाहरण के लिए, दूसरे क्रम के तर्क में दो प्रकार के प्रस्ताव होते हैं, एक प्रकार का शब्दों पर परिमाणीकरण, और दूसरे प्रकार का पहले प्रकार के प्रस्तावों पर परिमाणीकरण।

प्राकृतिक कटौती की विभिन्न प्रस्तुतियाँ

वृक्ष-जैसी प्रस्तुतियाँ

काल्पनिक निर्णयों को आंतरिक बनाने के लिए उपयोग किए जाने वाले जेंटज़ेन के डिस्चार्जिंग एनोटेशन को ए सच्चे निर्णयों के पेड़ के बजाय अनुक्रमों के पेड़ के रूप में साक्ष्य का प्रतिनिधित्व करके टाला जा सकता है।

अनुक्रमिक प्रस्तुतियाँ

जैस्कोवस्की के प्राकृतिक कटौती के निरूपण से फिच-शैली कैलकुलस (या फिच के आरेख) या पैट्रिक सुप्प्स विधि जैसे विभिन्न नोटेशन सामने आए, जिनमें से जॉन लेमन ने सिस्टम एल नामक एक संस्करण दिया। ऐसी प्रस्तुति प्रणाली, जिन्हें सारणीबद्ध के रूप में अधिक सटीक रूप से वर्णित किया गया है, में शामिल हैं निम्नलिखित।

• 1940: एक पाठ्यपुस्तक में, क्वीन सपेस के 1957 लाइन-संख्या अंकन का अनुमान लगाते हुए, वर्गाकार कोष्ठकों में पंक्ति संख्याओं द्वारा पूर्ववर्ती निर्भरताएँ दर्शाई गईं।
• 1950: एक पाठ्यपुस्तक में, Quine (1982, pp. 241–255) निर्भरता को इंगित करने के लिए प्रमाण की प्रत्येक पंक्ति के बाईं ओर एक या अधिक तारांकन का उपयोग करने की एक विधि का प्रदर्शन किया। यह क्लेन की ऊर्ध्वाधर पट्टियों के बराबर है। (यह पूरी तरह से स्पष्ट नहीं है कि क्वीन का तारांकन अंकन मूल 1950 संस्करण में दिखाई दिया था या बाद के संस्करण में जोड़ा गया था।)
• 1957: पाठ्यपुस्तक में व्यावहारिक तर्क प्रमेय का परिचय Suppes (1999, pp. 25–150). इसने प्रत्येक पंक्ति के बाईं ओर पंक्ति संख्याओं द्वारा निर्भरता (अर्थात पूर्ववर्ती प्रस्ताव) को दर्शाया।
• 1963: Stoll (1979, pp. 183–190, 215–219) प्राकृतिक कटौती अनुमान नियमों के आधार पर अनुक्रमिक तार्किक तर्कों की पंक्तियों की पूर्ववर्ती निर्भरता को इंगित करने के लिए पंक्ति संख्याओं के सेट का उपयोग करता है।
• 1965: संपूर्ण पाठ्यपुस्तक Lemmon (1965) सपेस पर आधारित विधि का उपयोग करके तर्क प्रमाणों का एक परिचय है।
• 1967: एक पाठ्यपुस्तक में, Kleene (2002, pp. 50–58, 128–130) संक्षेप में दो प्रकार के व्यावहारिक तर्क प्रमाणों का प्रदर्शन किया, एक प्रणाली प्रत्येक पंक्ति के बाईं ओर पूर्ववर्ती प्रस्तावों के स्पष्ट उद्धरणों का उपयोग करती है, दूसरी प्रणाली निर्भरता को इंगित करने के लिए बाईं ओर ऊर्ध्वाधर बार-लाइनों का उपयोग करती है।

प्रमाण और प्रकार सिद्धांत

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

──── u1 ──── u2 ... ──── un J1 J2 Jn ⋮ J

⇒

u1:J1, u2:J2, ..., un:Jn ⊢ J

परिकल्पनाओं के संग्रह को Γ के रूप में लिखा जाएगा जब उनकी सटीक रचना प्रासंगिक नहीं होगी। प्रमाणों को स्पष्ट करने के लिए, हम प्रमाण-रहित निर्णय A सत्य से निर्णय की ओर बढ़ते हैं: π (A true) का प्रमाण है, जिसे प्रतीकात्मक रूप से π : A true के रूप में लिखा जाता है। मानक दृष्टिकोण का पालन करते हुए, निर्णय π प्रमाण के लिए प्रमाणों को उनके स्वयं के गठन नियमों के साथ निर्दिष्ट किया जाता है। सबसे सरल संभव प्रमाण एक लेबल वाली परिकल्पना का उपयोग है; इस मामले में साक्ष्य लेबल ही है।

u ∈ V ─────── proof-F u proof

───────────────────── hyp u:A true ⊢ u : A true

संक्षिप्तता के लिए, हम इस लेख के बाकी हिस्से में निर्णयात्मक लेबल को सत्य छोड़ देंगे, यानी, Γ ⊢ π : A लिखेंगे। आइए स्पष्ट प्रमाणों के साथ कुछ संयोजकों की पुनः जाँच करें। संयोजन के लिए, हम संयोजन के प्रमाणों के रूप की खोज के लिए परिचय नियम ∧I को देखते हैं: उन्हें दो संयोजनों के प्रमाणों की एक जोड़ी होनी चाहिए। इस प्रकार:

π1 proof π2 proof ──────────────────── pair-F (π1, π2) proof

Γ ⊢ π1 : A Γ ⊢ π2 : B ───────────────────────── ∧I Γ ⊢ (π1, π2) : A ∧ B

उन्मूलन नियम ∧E₁ और ∧E₂ बाएँ या दाएँ संयुक्त संयोजन का चयन करें; इस प्रकार प्रमाण अनुमानों की एक जोड़ी हैं - पहला (fst) और दूसरा (snd)।

π proof ─────────── fst-F fst π proof		Γ ⊢ π : A ∧ B ───────────── ∧E1 Γ ⊢ fst π : A
π proof ─────────── snd-F snd π proof		Γ ⊢ π : A ∧ B ───────────── ∧E2 Γ ⊢ snd π : B

निहितार्थ के लिए, परिचय प्रपत्र λ का उपयोग करके लिखी गई परिकल्पना को स्थानीय बनाता है या बांधता है; यह डिस्चार्ज किए गए लेबल से मेल खाता है। नियम में, Γ, u:A अतिरिक्त परिकल्पना u के साथ परिकल्पना Γ के संग्रह को दर्शाता है।

π proof ──────────── λ-F λu. π proof		Γ, u:A ⊢ π : B ───────────────── ⊃I Γ ⊢ λu. π : A ⊃ B
π1 proof π2 proof ─────────────────── app-F π1 π2 proof		Γ ⊢ π1 : A ⊃ B Γ ⊢ π2 : A ──────────────────────────── ⊃E Γ ⊢ π1 π2 : B

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

प्रतिस्थापन प्रमेय

यदि Γ ⊢ π₁ : ए और Γ, यू:ए ⊢ π₂ : बी, फिर Γ ⊢ [पी₁/ऊपर₂ : बी।

अब तक निर्णय Γ ⊢ π : A की पूर्णतया तार्किक व्याख्या हुई है। प्रकार सिद्धांत में, वस्तुओं के अधिक कम्प्यूटेशनल दृश्य के लिए तार्किक दृश्य का आदान-प्रदान किया जाता है। तार्किक व्याख्या में प्रस्तावों को अब प्रकार के रूप में देखा जाता है, और लैम्ब्डा कैलकुलस में प्रमाणों को प्रोग्राम के रूप में देखा जाता है। इस प्रकार π: A की व्याख्या यह है कि प्रोग्राम π का ​​प्रकार A है। तार्किक संयोजकों को भी एक अलग रीडिंग दी जाती है: संयोजन को उत्पाद प्रकार (×) के रूप में देखा जाता है, निहितार्थ को फ़ंक्शन फ़ंक्शन प्रकार (→) आदि के रूप में देखा जाता है। हालांकि, अंतर केवल कॉस्मेटिक हैं। प्रकार सिद्धांत में गठन, परिचय और उन्मूलन नियमों के संदर्भ में एक प्राकृतिक कटौती प्रस्तुति है; वास्तव में, पाठक पिछले अनुभागों से जिसे सरल प्रकार के सिद्धांत के रूप में जाना जाता है, उसका आसानी से पुनर्निर्माण कर सकता है।

तर्क और प्रकार सिद्धांत के बीच अंतर मुख्य रूप से प्रकार (प्रस्ताव) से कार्यक्रमों (प्रमाण) पर ध्यान का बदलाव है। टाइप थ्योरी मुख्य रूप से कार्यक्रमों की परिवर्तनीयता या न्यूनता में रुचि रखती है। प्रत्येक प्रकार के लिए, उस प्रकार के विहित कार्यक्रम होते हैं जो अपरिवर्तनीय होते हैं; इन्हें विहित रूप या मान के रूप में जाना जाता है। यदि प्रत्येक प्रोग्राम को विहित रूप में कम किया जा सकता है, तो प्रकार सिद्धांत को सामान्यीकरण गुण (अमूर्त पुनर्लेखन) (या कमजोर रूप से सामान्यीकरण) कहा जाता है। यदि विहित रूप अद्वितीय है, तो सिद्धांत को दृढ़ता से सामान्यीकरण करने वाला कहा जाता है। सामान्यीकरण अधिकांश गैर-तुच्छ प्रकार के सिद्धांतों की एक दुर्लभ विशेषता है, जो तार्किक दुनिया से एक बड़ा विचलन है। (याद रखें कि लगभग हर तार्किक व्युत्पत्ति में एक समान सामान्य व्युत्पत्ति होती है।) कारण को रेखांकित करने के लिए: उन प्रकार के सिद्धांतों में जो पुनरावर्ती परिभाषाओं को स्वीकार करते हैं, ऐसे प्रोग्राम लिखना संभव है जो कभी भी एक मूल्य से कम नहीं होते हैं; ऐसे लूपिंग प्रोग्राम को आम तौर पर कोई भी प्रकार दिया जा सकता है। विशेष रूप से, लूपिंग प्रोग्राम का प्रकार ⊥ है, हालाँकि ⊥ true का कोई तार्किक प्रमाण नहीं है। इस कारण से, प्रकार के रूप में प्रस्ताव; प्रोग्राम प्रतिमान के रूप में प्रमाण केवल एक ही दिशा में काम करते हैं, यदि ऐसा होता भी है: एक प्रकार के सिद्धांत को तर्क के रूप में व्याख्या करना आम तौर पर एक असंगत तर्क देता है।

उदाहरण: आश्रित प्रकार सिद्धांत

तर्क की तरह, प्रकार सिद्धांत के कई विस्तार और प्रकार हैं, जिनमें प्रथम-क्रम और उच्च-क्रम संस्करण शामिल हैं। एक शाखा, जिसे आश्रित प्रकार सिद्धांत के रूप में जाना जाता है, का उपयोग कई कंप्यूटर-सहायता प्राप्त प्रमाण प्रणालियों में किया जाता है। आश्रित प्रकार का सिद्धांत क्वांटिफायरों को स्वयं कार्यक्रमों की सीमा तय करने की अनुमति देता है। इन परिमाणित प्रकारों को ∀ और ∃ के बजाय Π और Σ के रूप में लिखा जाता है, और निम्नलिखित गठन नियम हैं:

Γ ⊢ A type Γ, x:A ⊢ B type ───────────────────────────── Π-F Γ ⊢ Πx:A. B type

Γ ⊢ A type Γ, x:A ⊢ B type ──────────────────────────── Σ-F Γ ⊢ Σx:A. B type

ये प्रकार क्रमशः तीर और उत्पाद प्रकार के सामान्यीकरण हैं, जैसा कि उनके परिचय और उन्मूलन नियमों से पता चलता है।

Γ, x:A ⊢ π : B ──────────────────── ΠI Γ ⊢ λx. π : Πx:A. B

Γ ⊢ π1 : Πx:A. B Γ ⊢ π2 : A ───────────────────────────── ΠE Γ ⊢ π1 π2 : [π2/x] B

Γ ⊢ π1 : A Γ, x:A ⊢ π2 : B ───────────────────────────── ΣI Γ ⊢ (π1, π2) : Σx:A. B

Γ ⊢ π : Σx:A. B ──────────────── ΣE1 Γ ⊢ fst π : A

Γ ⊢ π : Σx:A. B ──────────────────────── ΣE2 Γ ⊢ snd π : [fst π/x] B

पूर्ण व्यापकता में आश्रित प्रकार का सिद्धांत बहुत शक्तिशाली है: यह प्रोग्राम की लगभग किसी भी बोधगम्य संपत्ति को सीधे प्रोग्राम के प्रकारों में व्यक्त करने में सक्षम है। यह व्यापकता भारी कीमत पर आती है - या तो टाइपचेकिंग अनिर्णीत है (विस्तारित प्रकार सिद्धांत ), या एक्सटेंशनल रीजनिंग अधिक कठिन है (गहन प्रकार का सिद्धांत )। इस कारण से, कुछ आश्रित प्रकार के सिद्धांत मनमाने कार्यक्रमों पर परिमाणीकरण की अनुमति नहीं देते हैं, बल्कि किसी दिए गए निर्णायक सूचकांक डोमेन के कार्यक्रमों तक ही सीमित रहते हैं, उदाहरण के लिए पूर्णांक, स्ट्रिंग या रैखिक कार्यक्रम।

चूंकि आश्रित प्रकार के सिद्धांत प्रकारों को कार्यक्रमों पर निर्भर होने की अनुमति देते हैं, इसलिए यह पूछना स्वाभाविक है कि क्या कार्यक्रमों के लिए प्रकारों या किसी अन्य संयोजन पर निर्भर होना संभव है। ऐसे सवालों के कई तरह के जवाब होते हैं. प्रकार सिद्धांत में एक लोकप्रिय दृष्टिकोण कार्यक्रमों को प्रकारों पर परिमाणित करने की अनुमति देना है, जिसे पैरामीट्रिक बहुरूपता के रूप में भी जाना जाता है; इसके दो मुख्य प्रकार हैं: यदि प्रकार और कार्यक्रमों को अलग रखा जाता है, तो कुछ हद तक अधिक अच्छी तरह से व्यवहार की जाने वाली प्रणाली प्राप्त होती है जिसे विधेय बहुरूपता कहा जाता है; यदि प्रोग्राम और प्रकार के बीच का अंतर धुंधला हो जाता है, तो व्यक्ति को उच्च-क्रम तर्क का प्रकार-सैद्धांतिक एनालॉग प्राप्त होता है, जिसे इम्प्रेडिकेटिव बहुरूपता के रूप में भी जाना जाता है। साहित्य में निर्भरता और बहुरूपता के विभिन्न संयोजनों पर विचार किया गया है, जिनमें से सबसे प्रसिद्ध हेन्क बेरेन्ड्रेट का लैम्ब्डा क्यूब है।

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

शास्त्रीय और मोडल तर्क

सरलता के लिए, अब तक प्रस्तुत तर्क अंतर्ज्ञानवादी तर्क रहे हैं। शास्त्रीय तर्क एक अतिरिक्त स्वयंसिद्ध या बहिष्कृत मध्य के सिद्धांत के साथ अंतर्ज्ञानवादी तर्क का विस्तार करता है:

किसी भी प्रस्ताव p के लिए, प्रस्ताव p ∨ ¬p सत्य है।

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

────────────── XM1 A ∨ ¬A true

¬¬A true ────────── XM2 A true

──────── u ¬A true ⋮ p true ────── XM3u, p A true

(एक्सएम₃ मात्र एक्सएम है₂ ई के संदर्भ में व्यक्त) बहिष्कृत मध्य का यह उपचार, शुद्धतावादी दृष्टिकोण से आपत्तिजनक होने के अलावा, सामान्य रूपों की परिभाषा में अतिरिक्त जटिलताओं का परिचय देता है।

अकेले परिचय और उन्मूलन नियमों के संदर्भ में शास्त्रीय प्राकृतिक कटौती का तुलनात्मक रूप से अधिक संतोषजनक उपचार पहली बार 1992 में मिशेल पैरिगोट द्वारा लैम्ब्डा-म्यू कैलकुलस|λμ नामक शास्त्रीय लैम्ब्डा कैलकुलस के रूप में प्रस्तावित किया गया था। उनके दृष्टिकोण की मुख्य अंतर्दृष्टि एक सत्य-केंद्रित निर्णय को एक अधिक शास्त्रीय धारणा के साथ प्रतिस्थापित करना था, जो अनुक्रमिक कैलकुलस की याद दिलाता है: स्थानीय रूप में, Γ ⊢ A के बजाय, उन्होंने Γ ⊢ Δ का उपयोग किया, Δ के साथ प्रस्तावों का एक संग्रह Γ के समान. Γ को संयोजन के रूप में और Δ को विच्छेद के रूप में माना जाता था। यह संरचना अनिवार्य रूप से शास्त्रीय अनुक्रम कैलकुलस से सीधे उठाई गई है, लेकिन λμ में नवाचार एलआईएसपी और उसके वंशजों में देखे गए कॉलसीसी या थ्रो/कैच तंत्र के संदर्भ में शास्त्रीय प्राकृतिक कटौती प्रमाणों को एक कम्प्यूटेशनल अर्थ देना था। (यह भी देखें: प्रथम श्रेणी नियंत्रण।)

एक अन्य महत्वपूर्ण विस्तार मोडल लॉजिक और अन्य तर्कों के लिए था, जिन्हें सत्य के मूल निर्णय से कहीं अधिक की आवश्यकता होती है। इन्हें पहली बार 1965 में डैग प्रवित्ज़ द्वारा प्राकृतिक कटौती शैली में एलेथिक मोडल लॉजिक्स एस4 (मोडल लॉजिक) और एस5 (मोडल लॉजिक) के लिए वर्णित किया गया था।और तब से संबंधित कार्यों का एक बड़ा भंडार जमा हो गया है। एक सरल उदाहरण देने के लिए, मोडल लॉजिक S4 को एक नए निर्णय, A वैध की आवश्यकता होती है, जो सत्य के संबंध में स्पष्ट है:

यदि A प्रपत्र B सत्य की किसी भी धारणा के तहत सत्य नहीं है, तो A मान्य है।

इस स्पष्ट निर्णय को निम्नलिखित परिचय और उन्मूलन नियमों के साथ एक एकल संयोजक ◻ए (आवश्यक रूप से ए पढ़ें) के रूप में आंतरिक किया गया है:

A valid ──────── ◻I ◻ A true

◻ A true ──────── ◻E A true

ध्यान दें कि आधार A वैध में कोई परिभाषित नियम नहीं हैं; इसके स्थान पर वैधता की स्पष्ट परिभाषा का उपयोग किया जाता है। जब परिकल्पनाएँ स्पष्ट होती हैं तो यह विधा स्थानीय रूप में स्पष्ट हो जाती है। हम Ω;Γ ⊢ एक सत्य लिखते हैं जहां Γ में पहले की तरह सच्ची परिकल्पनाएं शामिल हैं, और Ω में वैध परिकल्पनाएं हैं। दाहिनी ओर केवल एक ही निर्णय है 'ए सत्य'; यहां वैधता की आवश्यकता नहीं है क्योंकि Ω ⊢ A वैध परिभाषा के अनुसार Ω;⋅ ⊢ A true के समान है। परिचय और उन्मूलन प्रपत्र इस प्रकार हैं:

Ω;⋅ ⊢ π : A true ──────────────────── ◻I Ω;⋅ ⊢ box π : ◻ A true

Ω;Γ ⊢ π : ◻ A true ────────────────────── ◻E Ω;Γ ⊢ unbox π : A true

मोडल परिकल्पनाओं में परिकल्पना नियम और प्रतिस्थापन प्रमेय का अपना संस्करण होता है।

─────────────────────────────── valid-hyp Ω, u: (A valid) ; Γ ⊢ u : A true

मोडल प्रतिस्थापन प्रमेय

यदि Ω;⋅ ⊢ π₁ : A सत्य और Ω, u: (A मान्य); Γ ⊢ π₂ : C सत्य है, तो Ω?Γ ⊢ [p₁/ऊपर₂ : सी सच.

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

सूत्रों में लेबल जोड़ने से उन स्थितियों पर अधिक बेहतर नियंत्रण की अनुमति मिलती है जिनके तहत नियम लागू होते हैं, जिससे विश्लेषणात्मक झांकी की अधिक लचीली तकनीकों को लागू किया जा सकता है, जैसा कि लेबल कटौती के मामले में किया गया है। लेबल क्रिपके शब्दार्थ में दुनिया के नामकरण की भी अनुमति देते हैं; Simpson (1993) संकर तर्क के प्राकृतिक कटौती औपचारिकरण में क्रिप्के सिमेंटिक्स में मोडल लॉजिक्स की फ्रेम स्थितियों को अनुमान नियमों में परिवर्तित करने के लिए एक प्रभावशाली तकनीक प्रस्तुत करता है। Stouppa (2004) कई प्रमाण सिद्धांतों के अनुप्रयोग का सर्वेक्षण करता है, जैसे कि एवरॉन और पोटिंगर के हाइपरसेक्वेंट और बेलनैप के एस5 और बी जैसे मोडल लॉजिक के प्रदर्शन तर्क।

अन्य मूलभूत दृष्टिकोणों के साथ तुलना

गणना अनुसरण करती है

Main article: Sequent calculus

गणितीय तर्क की नींव के रूप में अनुक्रमिक कलन प्राकृतिक कटौती का मुख्य विकल्प है। प्राकृतिक कटौती में सूचना का प्रवाह द्वि-दिशात्मक होता है: उन्मूलन नियम जानकारी को विखंडन द्वारा नीचे की ओर प्रवाहित करते हैं, और परिचय नियम जानकारी को संयोजन द्वारा ऊपर की ओर प्रवाहित करते हैं। इस प्रकार, एक प्राकृतिक कटौती प्रमाण में पूरी तरह से नीचे से ऊपर या ऊपर से नीचे की रीडिंग नहीं होती है, जिससे यह प्रमाण खोज में स्वचालन के लिए अनुपयुक्त हो जाता है। इस तथ्य को संबोधित करने के लिए, 1935 में गेरहार्ड जेंटज़ेन ने अपने अनुक्रमिक कैलकुलस का प्रस्ताव रखा, हालांकि उन्होंने शुरुआत में इसे विधेय तर्क की स्थिरता को स्पष्ट करने के लिए एक तकनीकी उपकरण के रूप में इरादा किया था। स्टीफन कोल क्लेन ने 1952 में अपनी मौलिक पुस्तक इंट्रोडक्शन टू मेटामैथमेटिक्स में आधुनिक शैली में अनुक्रमिक कैलकुलस का पहला सूत्रीकरण दिया। अनुक्रमिक कलन में सभी अनुमान नियमों का पाठन पूरी तरह से नीचे से ऊपर की ओर होता है। अनुमान नियम टर्नस्टाइल (प्रतीक) के दोनों तरफ के तत्वों पर लागू हो सकते हैं। (प्राकृतिक कटौती से अंतर करने के लिए, यह लेख अनुक्रमों के लिए सही कील ⊢ के बजाय एक डबल तीर ⇒ का उपयोग करता है।) प्राकृतिक कटौती के परिचय नियमों को अनुक्रम गणना में सही नियमों के रूप में देखा जाता है, और संरचनात्मक रूप से बहुत समान हैं। दूसरी ओर उन्मूलन नियम अनुक्रमिक गणना में बाएँ नियमों में बदल जाते हैं। उदाहरण देने के लिए, विच्छेदन पर विचार करें; सही नियम परिचित हैं:

Γ ⇒ A ───────── ∨R1 Γ ⇒ A ∨ B

Γ ⇒ B ───────── ∨R2 Γ ⇒ A ∨ B

बाईं तरफ:

Γ, u:A ⇒ C Γ, v:B ⇒ C ─────────────────────────── ∨L Γ, w: (A ∨ B) ⇒ C

स्थानीय रूप में प्राकृतिक कटौती के ∨E नियम को याद करें:

Γ ⊢ A ∨ B Γ, u:A ⊢ C Γ, v:B ⊢ C ─────────────────────────────────────── ∨E Γ ⊢ C

प्रस्ताव A ∨ B, जो ∨E में एक आधार का अनुवर्ती है, बाएं नियम ∨L में निष्कर्ष की एक परिकल्पना में बदल जाता है। इस प्रकार, बाएँ नियम को एक प्रकार के उल्टे उन्मूलन नियम के रूप में देखा जा सकता है। इस अवलोकन को इस प्रकार चित्रित किया जा सकता है:

natural deduction		sequent calculus
────── hyp | | elim. rules | ↓ ────────────────────── ↑↓ meet ↑ | | intro. rules | conclusion	⇒	─────────────────────────── init ↑ ↑ | | | left rules | right rules | | conclusion

अनुक्रमिक कैलकुलस में, बाएँ और दाएँ नियमों को लॉक-स्टेप में निष्पादित किया जाता है जब तक कि कोई प्रारंभिक अनुक्रम तक नहीं पहुँच जाता है, जो प्राकृतिक कटौती में उन्मूलन और परिचय नियमों के मिलन बिंदु से मेल खाता है। ये प्रारंभिक नियम सतही तौर पर प्राकृतिक कटौती के परिकल्पना नियम के समान हैं, लेकिन अनुक्रमिक गणना में वे बाएँ और दाएँ प्रस्ताव के स्थानान्तरण या हाथ मिलाने का वर्णन करते हैं:

────────── init Γ, u:A ⇒ A

अनुक्रमिक कैलकुलस और प्राकृतिक कटौती के बीच पत्राचार ध्वनि और पूर्णता प्रमेयों की एक जोड़ी है, जो दोनों एक आगमनात्मक तर्क के माध्यम से सिद्ध करने योग्य हैं।

⇒ wrt की ध्वनि. ⊢

यदि Γ ⇒ A, तो Γ ⊢ A.

⇒ wrt की पूर्णता. ⊢

यदि Γ ⊢ A, तो Γ ⇒ A.

इन प्रमेयों से यह स्पष्ट है कि अनुक्रमिक कलन सत्य की धारणा को नहीं बदलता है, क्योंकि प्रस्तावों का वही संग्रह सत्य रहता है। इस प्रकार, कोई व्यक्ति अनुक्रमिक कैलकुलस व्युत्पत्तियों में पहले की तरह समान प्रमाण वस्तुओं का उपयोग कर सकता है। उदाहरण के तौर पर संयोजकों पर विचार करें। सही नियम वस्तुतः परिचय नियम के समान है

sequent calculus		natural deduction
Γ ⇒ π1 : A Γ ⇒ π2 : B ─────────────────────────── ∧R Γ ⇒ (π1, π2) : A ∧ B		Γ ⊢ π1 : A Γ ⊢ π2 : B ───────────────────────── ∧I Γ ⊢ (π1, π2) : A ∧ B

हालाँकि, बायाँ नियम कुछ अतिरिक्त प्रतिस्थापन करता है जो संबंधित उन्मूलन नियमों में नहीं किया जाता है।

sequent calculus		natural deduction
Γ, u:A ⇒ π : C ──────────────────────────────── ∧L1 Γ, v: (A ∧ B) ⇒ [fst v/u] π : C		Γ ⊢ π : A ∧ B ───────────── ∧E1 Γ ⊢ fst π : A
Γ, u:B ⇒ π : C ──────────────────────────────── ∧L2 Γ, v: (A ∧ B) ⇒ [snd v/u] π : C		Γ ⊢ π : A ∧ B ───────────── ∧E2 Γ ⊢ snd π : B

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

प्राकृतिक कटौती का प्रतिस्थापन प्रमेय एक संरचनात्मक नियम या संरचनात्मक प्रमेय का रूप लेता है जिसे अनुक्रमिक कलन में कटौती के रूप में जाना जाता है।

कट (प्रतिस्थापन)

यदि Γ ⇒ π₁ : ए और Γ, यू:ए ⇒ पी₂ : सी, फिर Γ ⇒ [पी₁/ऊपर₂ : सी।

अधिकांश अच्छे व्यवहार वाले तर्कों में, कटौती एक अनुमान नियम के रूप में अनावश्यक है, हालांकि यह मेटा-प्रमेय के रूप में सिद्ध करने योग्य है; कट नियम की अतिश्योक्ति को आमतौर पर एक कम्प्यूटेशनल प्रक्रिया के रूप में प्रस्तुत किया जाता है, जिसे कट उन्मूलन के रूप में जाना जाता है। इसमें प्राकृतिक कटौती के लिए एक दिलचस्प अनुप्रयोग है; आमतौर पर मामलों की असीमित संख्या के कारण कुछ संपत्तियों को सीधे प्राकृतिक कटौती में साबित करना बेहद कठिन होता है। उदाहरण के लिए, यह दर्शाने पर विचार करें कि कोई दिया गया प्रस्ताव प्राकृतिक कटौती में सिद्ध करने योग्य नहीं है। एक सरल आगमनात्मक तर्क ∨E या E जैसे नियमों के कारण विफल हो जाता है जो मनमाना प्रस्ताव प्रस्तुत कर सकते हैं। हालाँकि, हम जानते हैं कि अनुक्रमिक कैलकुलस प्राकृतिक कटौती के संबंध में पूर्ण है, इसलिए अनुक्रमिक कैलकुलस में इस अप्रमाणिकता को दिखाने के लिए यह पर्याप्त है। अब, यदि कट एक अनुमान नियम के रूप में उपलब्ध नहीं है, तो सभी अनुक्रमिक नियम या तो दाईं ओर या बाईं ओर एक संयोजक पेश करते हैं, इसलिए अनुक्रमिक व्युत्पत्ति की गहराई अंतिम निष्कर्ष में संयोजकों द्वारा पूरी तरह से सीमित होती है। इस प्रकार, अप्राप्यता दिखाना बहुत आसान है, क्योंकि विचार करने के लिए केवल सीमित संख्या में मामले हैं, और प्रत्येक मामला पूरी तरह से निष्कर्ष के उप-प्रस्तावों से बना है। इसका एक सरल उदाहरण वैश्विक स्थिरता प्रमेय है: ⋅ ⊢ ⊥ सत्य सिद्ध करने योग्य नहीं है। अनुक्रमिक कैलकुलस संस्करण में, यह स्पष्ट रूप से सत्य है क्योंकि ऐसा कोई नियम नहीं है जिसके निष्कर्ष के रूप में ⋅ ⇒ ⊥ हो सकता है! प्रमाण सिद्धांतकार अक्सर ऐसे गुणों के कारण कट-फ्री अनुक्रमिक कैलकुलस फॉर्मूलेशन पर काम करना पसंद करते हैं।