निगमन की चार तकनीकें

आरंभिक उपकरण

औपचारिक निगमन प्रणालियों पर पाठ में लुकासिएविच प्रणाली निर्धारित की गई। उसकी भाषा वृत्तों और चक्रिकाओं की भाषा है, जो प्रस्तावात्मक तर्क की भाषा पर पाठ के आधिकारिक संक्षेपणों से लिखी जाती है; उसके अभिगृहीत निम्नलिखित तीन योजनाओं के सभी दृष्टांत हैं, जहाँ $\varphi$, $\psi$ और $\chi$ कोई भी सूत्र हैं, और उसका एकमात्र नियम मोडस पोनेन्स है।

• A1: $(\varphi \rightarrow (\psi \rightarrow \varphi))$।
• A2: $((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi)))$।
• A3: $((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi))$।
• MP: $\varphi$ और $(\varphi \rightarrow \psi)$ से $\psi$ निगमित होता है।

$\varphi$ का निगमन, सूत्रों के किसी समुच्चय $\Gamma$ से, सूत्रों का एक परिमित अनुक्रम है जो $\varphi$ पर समाप्त होता है और जिसमें प्रत्येक सूत्र या तो अभिगृहीत है, या $\Gamma$ का अवयव, या दो पूर्ववर्ती सूत्रों पर मोडस पोनेन्स लागू करने का परिणाम; यदि ऐसा निगमन हो, तो $\Gamma \vdash \varphi$ लिखा जाता है, और यदि $\Gamma$ रिक्त हो, तो $\vdash \varphi$, और कहा जाता है कि $\varphi$ एक प्रमेय है। उसी पाठ में वे अधिप्रमेय सिद्ध किए गए जिनका हम यहाँ उपयोग करेंगे: स्वतुल्यता (Refl: यदि $\varphi \in \Gamma$, तो $\Gamma \vdash \varphi$), एकदिष्टता (Mon: यदि $\Gamma \subseteq \Delta$ और $\Gamma \vdash \varphi$, तो $\Delta \vdash \varphi$), निगमनों के बीच मोडस पोनेन्स (यदि $\Gamma \vdash \varphi$ और $\Gamma \vdash (\varphi \rightarrow \psi)$, तो $\Gamma \vdash \psi$), कर्तन (Cut: यदि $\Gamma \vdash \varphi_{i}$, $i$ के $1$ से $n$ तक के प्रत्येक मान के लिए, और $\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi$, तो $\Gamma \vdash \psi$), परिमितता (यदि $\Gamma \vdash \varphi$, तो $\Gamma$ का कोई परिमित उपसमुच्चय पर्याप्त है), निगमन प्रमेय (DT: यदि $\Gamma \cup \{\varphi\} \vdash \psi$, तो $\Gamma \vdash (\varphi \rightarrow \psi)$) और उसका विलोम (CDT), तथा प्रमेय $\vdash (\varphi \rightarrow \varphi)$, जिसे औचित्यों में हम Id लिखेंगे। अंत में, $\varphi \dashv\vdash \psi$ (निगमनतः तुल्यता) का अर्थ है कि $\{\varphi\} \vdash \psi$ और $\{\psi\} \vdash \varphi$।

यह स्मरण रखना उचित है कि $\neg$ और $\rightarrow$ आधार-भाषा के प्रतीक नहीं, बल्कि संक्षेपण हैं: $\neg\varphi$ शृंखला $(\varphi \downarrow \varphi)$ है, और $(\varphi \rightarrow \psi)$, $(\neg\varphi \vee \psi)$ है, अर्थात् $\neg(\neg\varphi \downarrow \psi)$। तीनों अभिगृहीत केवल निषेधों और सोपाधिकों की बात करते हैं, और उसी पाठ ने $0$ और $1$ मानों वाले एक अंकन से, जिसे वे और मोडस पोनेन्स संरक्षित रखते हैं, इससे निकलने वाली सीमा दिखाई: लुकासिएविच प्रणाली में $(v_{1} \downarrow v_{2})$ से $(\neg\neg v_{1} \downarrow v_{2})$ निगमित नहीं होता, और संयुक्त निषेध आंशिक रूप से उसकी पहुँच से बाहर रहता है। अतः यह पाठ दो चरणों में आगे बढ़ता है। दोहरे निषेध तक (उसे सम्मिलित करके), $\vdash$ लुकासिएविच प्रणाली को सूचित करता है, और जो कुछ सिद्ध होता है उसमें से कुछ भी संक्षेपणों को खोलने पर निर्भर नहीं करता। दोहरा निषेध सिद्ध होने के बाद, प्रणाली में दूसरा मूल नियम जोड़ा जाता है, दोहरे निषेध का प्रतिस्थापन, जो खोली गई शृंखला पर कार्य करता है; उस बिंदु से, $\vdash$ पाठ्यक्रम की प्रणाली को सूचित करता है, अर्थात् लुकासिएविच प्रणाली के साथ यह नियम। चूँकि पहली प्रणाली का प्रत्येक निगमन दूसरी का भी निगमन है, इसलिए पहले सिद्ध की गई कोई भी बात खोती नहीं।

निगमन की दो शैलियाँ

निगमन लिखने के दो तरीके हैं, और दोनों का उपयोग होगा। पहला है वास्तविक अर्थ में निगमन, सूत्रों का एक अनुक्रम जिसमें प्रत्येक पंक्ति अभिगृहीत, आधार-वाक्य या मोडस पोनेन्स का परिणाम है; प्रत्येक पंक्ति का औचित्य A1, A2, A3, आधार-वाक्य या MP$(i, j)$ से दिया जाता है, जहाँ पंक्ति $i$ पूर्वपद है और पंक्ति $j$ वह सोपाधिक है जिसका पूर्वपद ठीक-ठीक पंक्ति $i$ है (और, नया नियम लाने के बाद, RDN$(i)$ भी)। दूसरा है निगमनों पर निगमन, जिसकी पंक्तियाँ सूत्र नहीं, बल्कि $\Gamma \vdash \varphi$ रूप के कथन हैं; प्रत्येक का औचित्य किसी पहले से सिद्ध अधिप्रमेय से दिया जाता है, और पूरा अनुक्रम अधिभाषा की एक युक्ति है जो यह सुनिश्चित करती है कि पहली शैली का एक निगमन विद्यमान है, यद्यपि वह उसे लिखती नहीं। इस दूसरी शैली के औचित्य इस प्रकार पढ़े जाते हैं।

• Refl: दाईं ओर का सूत्र बाईं ओर के समुच्चय का अवयव है।
• A1, A2, A3: दाईं ओर का सूत्र योजना का दृष्टांत है; किसी अभिगृहीत का दृष्टांत किसी भी $\Gamma$ से एक ही पंक्ति के निगमन द्वारा निगमित होता है।
• MP$(i, j)$: निगमनों के बीच मोडस पोनेन्स, जो पंक्ति $i$, $\Gamma \vdash \varphi$, और पंक्ति $j$, $\Gamma \vdash (\varphi \rightarrow \psi)$, पर एक ही $\Gamma$ के साथ लागू किया गया है।
• DT$(i)$ और CDT$(i)$: पंक्ति $i$ पर लागू निगमन प्रमेय या उसका विलोम।
• पहले से सिद्ध किसी प्रमेय का नाम, जैसे Id या DN: दाईं ओर का सूत्र उस प्रमेय का दृष्टांत है, और एकदिष्टता से किसी भी $\Gamma$ से निगमित होता है, क्योंकि रिक्त समुच्चय $\Gamma$ में अंतर्विष्ट है।
• आधार-वाक्य, निगमनों पर निगमन में: पंक्ति उस नियम की परिकल्पनाओं में से एक है जिसे सिद्ध किया जा रहा है।

इस पाठ का प्रत्येक परिणाम अधिचरों से कहा जाता है और इसलिए किन्हीं भी सूत्रों के लिए मान्य है: उसकी उपपत्ति एक योजना है, और उसमें प्रत्येक अधिचर के स्थान पर कोई सूत्र रखने पर एक अन्य उपपत्ति मिलती है, क्योंकि अभिगृहीत-योजना के दृष्टांत दृष्टांत ही रहते हैं और मोडस पोनेन्स का प्रत्येक अनुप्रयोग वैसा ही रहता है (नए नियम के प्रत्येक अनुप्रयोग के लिए भी यही होगा)। इस प्रकार, $\vdash (\varphi \rightarrow \varphi)$ से $\vdash (\neg\psi \rightarrow \neg\psi)$ प्राप्त होता है, $\neg\psi$ को $\varphi$ के स्थान पर रखकर। यह साधन, किसी परिणाम को कथन के सूत्र से अधिक जटिल सूत्र पर लागू करना, आगे सबसे अधिक उपयोगी है।

परिणाम से नियम तक

इस पाठ की तकनीकें $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)$ जैसे स्थिर आधार-वाक्यों से सिद्ध की जाती हैं; पर उनका उपयोग अन्य आधार-वाक्यों वाले निगमनों के बीच में होता है, जहाँ $(\varphi \rightarrow \psi)$ और $(\psi \rightarrow \chi)$ आधार-वाक्य नहीं, बल्कि पहले से निगमित सूत्र हैं। निम्नलिखित प्रमेयिका, जो एकदिष्टता और कर्तन का सीधा परिणाम है, इस उपयोग को एक ही बार में सदा के लिए अधिकृत करती है।

इससे यह निकलता है कि आधार-वाक्यों से सिद्ध प्रत्येक तकनीक के तीन रूप हैं: स्वयं परिणाम, उसके आधार-वाक्यों को मुक्त करके प्राप्त प्रमेय, और किसी भी $\Gamma$ के अंतर्गत लागू होने वाला नियम। निगमनों पर निगमन में, नियम का उल्लेख तकनीक के नाम और उन पंक्तियों की संख्याओं से किया जाता है जिन पर वह लागू होता है, जैसे HS$(3, 4)$, और प्रमेयिका सुनिश्चित करती है कि वह चरण वैध है।