नेचुरल डिडक्शन

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

प्रेरणा

डेविड हिल्बर्ट, गोटलॉब फ्रेगे, और बर्ट्रेंड रसेल (उदाहरण के लिए, हिल्बर्ट प्रणाली देखें) की प्रणालियों के लिए आम निगमनात्मक तर्क के स्वयंसिद्धों के साथ असंतोष के संदर्भ में प्राकृतिक कटौती उत्पन्न हुई। बर्ट्रेंड रसेल और अल्फ्रेड नॉर्थ व्हाइटहेड ने अपने गणितीय ग्रंथ गणितीय सिद्धांत में इस तरह के स्वयंसिद्धों का सबसे प्रसिद्ध रूप से उपयोग किया था। 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".

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

प्राकृतिक कटौती में, बार-बार अनुमान नियमों को लागू करके परिसर के संग्रह से एक प्रस्ताव घटाया जाता है। इस आलेख में प्रस्तुत प्रणाली Gentzen's या Prawitz के सूत्रीकरण की एक मामूली भिन्नता है, लेकिन Per Martin-Löf|Martin-Löf के तार्किक निर्णयों और संयोजकों के विवरण के करीब पालन के साथ।

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

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

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

निर्णय 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 सत्य से, हम 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 सत्य है; दूसरे शब्दों में, निर्णय B सत्य कल्पित निर्णय A ∧ (B ∧ C) सत्य पर निर्भर करता है। यह एक काल्पनिक व्युत्पत्ति है, जिसे हम इस प्रकार लिखते हैं:

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

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

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

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

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

${\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}$

प्रस्तावना नियम में उ नाम का पूर्वपद निष्कर्ष में विमोचित होता है। यह परिकल्पना के दायरे को परिसीमित करने का एक तंत्र है: इसके अस्तित्व का एकमात्र कारण B सत्य को स्थापित करना है; इसका उपयोग किसी अन्य उद्देश्य के लिए नहीं किया जा सकता है, और विशेष रूप से, इसका उपयोग परिचय के नीचे नहीं किया जा सकता है। एक उदाहरण के रूप में, 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 सत्य नहीं है। उन्मूलन के लिए, यदि A और A दोनों को सत्य नहीं दिखाया जाता है, तो एक विरोधाभास होता है, इस स्थिति में प्रत्येक प्रस्ताव C सत्य होता है। क्योंकि निहितार्थ और निषेध के नियम इतने समान हैं, यह देखना काफी आसान होना चाहिए कि 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-रूपांतरण|η-रूपांतरण (ईटा रूपांतरण) लैम्ब्डा कैलकुलस में करी-हावर्ड का उपयोग करते हुए सटीक रूप से मेल खाती हैं समरूपता। स्थानीय पूर्णता से, हम देखते हैं कि प्रत्येक व्युत्पत्ति को समतुल्य व्युत्पत्ति में परिवर्तित किया जा सकता है जहां प्रमुख संयोजक पेश किया जाता है। वास्तव में, यदि संपूर्ण व्युत्पत्ति विलोपन के इस क्रम का पालन करती है, जिसके बाद परिचय होता है, तो इसे सामान्य कहा जाता है। एक सामान्य व्युत्पत्ति में सभी विलोपन परिचय से ऊपर होते हैं। अधिकांश लॉजिक्स में, प्रत्येक व्युत्पत्ति का एक समान सामान्य व्युत्पत्ति होती है, जिसे सामान्य रूप (सार पुनर्लेखन) कहा जाता है। सामान्य रूपों का अस्तित्व आम तौर पर अकेले प्राकृतिक कटौती का उपयोग करके साबित करना कठिन होता है, हालांकि ऐसे खाते साहित्य में मौजूद हैं, विशेष रूप से 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}$

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

${\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 के प्रतिस्थापन के लिए है। जैसा कि नाम पर सुपरस्क्रिप्ट से पहले उन घटकों के लिए खड़ा होता है जिन्हें डिस्चार्ज किया जाता है: शब्द ∀I के निष्कर्ष में नहीं हो सकता है (ऐसे शब्दों को ईजेनवेरिएबल्स या पैरामीटर के रूप में जाना जाता है), और ∃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}}$

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

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

पेड़ जैसी प्रस्तुतियाँ

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

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

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

• 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 सत्य) का प्रमाण है, जिसे प्रतीकात्मक रूप से π: A सत्य के रूप में लिखा जाता है। मानक दृष्टिकोण का पालन करते हुए, निर्णय π प्रमाण के लिए प्रमाण अपने स्वयं के गठन नियमों के साथ निर्दिष्ट किए जाते हैं। सबसे सरल संभव प्रमाण एक लेबल वाली परिकल्पना का उपयोग है; इस मामले में सबूत ही लेबल है।

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 परिकल्पनाओं के संग्रह के लिए खड़ा है, साथ में अतिरिक्त परिकल्पना यू।

π 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

यदि Ω;⋅ ⊢ π₁ : एक सच और Ω, यू: (एक मान्य); जी ⊢ π₂ : सी सच है, तो Ω?Γ ⊢ [पी₁/ऊपर₂ : सी सच।

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

फ़ार्मुलों में लेबल जोड़ने से उन शर्तों पर बेहतर नियंत्रण मिलता है जिनके तहत नियम लागू होते हैं, जिससे विश्लेषणात्मक झांकी की अधिक लचीली तकनीकों को लागू किया जा सकता है, जैसा कि लेबल कटौती के मामले में किया गया है। लेबल भी कृपके सिमेंटिक्स में दुनिया के नामकरण की अनुमति देते हैं; Simpson (1993) संकर तर्क के एक प्राकृतिक कटौती औपचारिकता में क्रिपके सिमेंटिक्स में मोडल लॉजिक्स की फ्रेम स्थितियों को परिवर्तित करने के लिए एक प्रभावशाली तकनीक प्रस्तुत करता है। Stouppa (2004) कई प्रूफ सिद्धांतों के अनुप्रयोग का सर्वेक्षण करता है, जैसे एवरॉन और पोटिंगर के hypersequent ्स और बेलनाप के एस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 जैसे नियमों के कारण एक साधारण आगमनात्मक तर्क विफल हो जाता है जो मनमाना प्रस्तावों को प्रस्तुत कर सकता है। हालाँकि, हम जानते हैं कि अनुक्रमिक कलन प्राकृतिक कटौती के संबंध में पूर्ण है, इसलिए यह अनुक्रमिक कलन में इस अप्राप्यता को दर्शाने के लिए पर्याप्त है। अब, यदि कट एक अनुमान नियम के रूप में उपलब्ध नहीं है, तो सभी अनुक्रमिक नियम या तो दाएं या बाएं पर एक संयोजक का परिचय देते हैं, इसलिए अनुक्रम व्युत्पत्ति की गहराई अंतिम निष्कर्ष में संयोजकों द्वारा पूरी तरह से बंधी हुई है। इस प्रकार, अप्राप्यता दिखाना बहुत आसान है, क्योंकि विचार करने के लिए केवल सीमित संख्या में मामले हैं, और प्रत्येक मामला पूरी तरह से निष्कर्ष के उप-प्रस्तावों से बना है। इसका एक सरल उदाहरण वैश्विक संगति प्रमेय है: ⋅ ⊢ ⊥ true सिद्ध करने योग्य नहीं है। अनुक्रमिक कैलकुस संस्करण में, यह स्पष्ट रूप से सत्य है क्योंकि ऐसा कोई नियम नहीं है जो निष्कर्ष के रूप में ⋅ ⇒ ⊥ हो सकता है! ऐसे गुणों के कारण प्रूफ सिद्धांतकार अक्सर कट-फ्री सीक्वेंस कैलकुलस फॉर्मूलेशन पर काम करना पसंद करते हैं।