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

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

प्रेरणा

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

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

मुझे लगता है कि मैं औपचारिक रूप से काम नहीं कर रहा हूं, जो कि उनके काम को सरल बनाता है। तो एरगैब सिच एइन "कलकुल डेस नेचुरल श्लीसेन".

पहले मैं एक ऐसी औपचारिकता का निर्माण करना चाहता था जो वास्तविक तर्क के जितना निकट हो सके। इस प्रकार "प्राकृतिक अल्पब्यापी की गणना" उत्पन्न हुई।

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

प्राकृतिक अल्पव्यापी में, बार-बार अनुमान नियमों को प्रयुक्त करके परिसर के संग्रह से प्रस्ताव घटाया जाता है। इस आलेख में प्रस्तुत प्रणाली जेंटजन या प्रविट्ज़ के सूत्रीकरण की सामान्य भिन्नता है। किन्तु प्रति मार्टिन-लोफ के तार्किक निर्णयों और संयोजकों के विवरण के निकट है।

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

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

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

निर्णय A प्रस्ताव A के मान्य प्रमाणों की संरचना को परिभाषित करता है, जो बदले में प्रस्तावों की संरचना को परिभाषित करता है। इस कारण से, इस निर्णय के अनुमान नियम को कभी-कभी गठन नियम के रूप में जाना जाता है। वर्णन करने के लिए, यदि हमारे पास दो प्रस्ताव a और b हैं (अर्थात निर्णय a प्रोप और b प्रोप स्पष्ट हैं), तो हम यौगिक प्रस्ताव a और b बनाते हैं, जो प्रतीकात्मक रूप से $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}$

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

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

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

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

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

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

यदि 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}}$

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

${\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 सत्य या B सत्य के लिए प्रतिबद्ध नहीं है। शून्य-एरी स्थिति में, अर्थात असत्य के लिए, हम निम्नलिखित विलोपन नियम प्राप्त करते हैं।

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

परिचय नियम परिकल्पना U, और उत्तराधिकारी p दोनों के नाम का निर्वहन करता है। अर्थात, प्रस्ताव p निष्कर्ष a में नहीं होना चाहिए। चूंकि ये नियम योजनाबद्ध हैं, परिचय नियम की व्याख्या है। यदि एक सत्य से हम कर सकते हैं। प्रत्येक तर्कवाक्य 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 के पेड़ के रूप में सबूतों का प्रतिनिधित्व करके टाला जा सकता है।

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

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

• 1940: पाठ्यपुस्तक में, क्वीन वर्गाकार कोष्ठकों में रेखा संख्याओं द्वारा पूर्ववर्ती निर्भरताओं का संकेत दिया गया, जो कि सपेस के 1957 के पंक्ति-संख्या संकेतन का अनुमान था।
• 1950: पाठ्यपुस्तक में, क्वीन (1982, pp. 241–255) ने निर्भरता को इंगित करने के लिए प्रमाण की प्रत्येक पंक्ति के बाईं ओर एक या अधिक तारांकनों का उपयोग करने की विधि का प्रदर्शन किया। यह क्लेन की खड़ी पट्टियों के बराबर है। (यह पूरी तरह से स्पष्ट नहीं है कि क्विन का तारांकन चिह्न मूल 1950 के संस्करण में दिखाई दिया था या बाद के संस्करण में जोड़ा गया था।)
• 1957: द्वारा पाठ्यपुस्तक में व्यावहारिक तर्क प्रमेय को सिद्ध करने का परिचय सुप्पेस (1999, pp. 25–150). यह प्रत्येक पंक्ति के बाईं ओर लाइन नंबरों द्वारा निर्भरताओं (अर्थात पूर्ववर्ती प्रस्तावों) को इंगित करता है।
• 1963: स्टॉल (1979, pp. 183–190, 215–219) प्राकृतिक अल्पव्यापी अनुमान नियमों के आधार पर अनुक्रमिक तार्किक तर्कों की पंक्तियों की पूर्ववर्ती निर्भरताओं को इंगित करने के लिए पंक्ति संख्याओं के समुच्चय का उपयोग करता है।
• 1965: संपूर्ण पाठ्यपुस्तक द्वारा लेमन (1965) सपेस के आधार पर एक विधि का उपयोग करके तर्क प्रमाण का परिचय है।
• 1967: पाठ्यपुस्तक में, क्लीन (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₂ या तो बाएँ या दाएँ संयोजन का चयन करें; इस प्रकार प्रमाण अनुमानों की एक जोड़ी है।

π 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 और Γ, u:A ⊢ π₂ : B, फिर Γ ⊢ [π₁/u] π₂ : B।

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

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

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

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

Γ ⊢ 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

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

अकेले परिचय और उन्मूलन नियमों के संदर्भ में मौलिक प्राकृतिक अल्पव्यापी का तुलनात्मक रूप से अधिक संतोषजनक उपचार पहली बार 1992 में क्लासिकल लैम्ब्डा कैलकुलस के रूप में प्रस्तावित किया गया था जिसे लैम्ब्डा-म्यू कैलकुलस|λμ कहा जाता है। उनके दृष्टिकोण की मुख्य अंतर्दृष्टि सत्य-केंद्रित निर्णय A सत्य को अधिक मौलिक धारणा के साथ बदलना था, अनुक्रमिक गणना की याद दिलाती है: स्थानीयकृत रूप में, Γ ⊢ 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

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

यदि Ω;⋅ ⊢ π₁ : A सत्य और Ω, U: ( मान्य); Γ ⊢ π₂ : C सत्य है, तो Ω;Γ ⊢ [π₁/u] π₂ : C सत्य।

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

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

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

गणना का पालन करें

Main article: अनुक्रमिक गणना

गणितीय तर्क की नींव के रूप में अनुक्रमिक गणना प्राकृतिक अल्पव्यापी का मुख्य विकल्प है। प्राकृतिक अल्पव्यापी में सूचना का प्रवाह द्वि-दिशात्मक होता है: विलोपन नियम विखंडन द्वारा सूचना को नीचे की ओर प्रवाहित करते हैं, और परिचय नियम विधानसभा द्वारा सूचना को ऊपर की ओर प्रवाहित करते हैं। इस प्रकार, प्राकृतिक अल्पव्यापी प्रमाण में विशुद्ध रूप से नीचे-ऊपर या ऊपर-नीचे पढ़ना नहीं होता है। जिससे यह प्रमाण खोज में स्वचालन के लिए अनुपयुक्त हो जाता है। इस तथ्य को संबोधित करने के लिए, 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 में निष्कर्ष की परिकल्पना में बदल जाता है। इस प्रकार, वाम नियमों को एक प्रकार के उल्टे उन्मूलन नियम के रूप में देखा जा सकता है। इस अवलोकन को इस प्रकार चित्रित किया जा सकता है।

प्राकृतिक अल्पव्यापी		अनुक्रमिक गणना
────── hyp | | elim. rules | ↓ ────────────────────── ↑↓ meet ↑ | | intro. rules | conclusion	⇒	─────────────────────────── init ↑ ↑ | | | left rules | right rules | | conclusion

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

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

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

⇒ wrt की ध्वनि। ⊢

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

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

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

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

अनुक्रमिक गणना		प्राकृतिक अल्पव्यापी
Γ ⇒ π1 : A Γ ⇒ π2 : B ─────────────────────────── ∧R Γ ⇒ (π1, π2) : A ∧ B		Γ ⊢ π1 : A Γ ⊢ π2 : B ───────────────────────── ∧I Γ ⊢ (π1, π2) : A ∧ B

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

अनुक्रमिक गणना		प्राकृतिक अल्पव्यापी
Γ, 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

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

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

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

यदि Γ ⇒ π₁ : A और Γ, u:A ⇒ π₂ : C, फिर Γ ⇒ [π₁/u] π₂ : C

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