संयोजकों की सममितियाँ

क्या उपयोग होता है और क्या सिद्ध करना है

औपचारिक निगमन प्रणालियों पर पाठ ने लुकासिएविच प्रणाली निर्धारित की: अभिगृहीत A1, A2 और A3 तथा मोडस पोनेन्स। उसने इसके अतिरिक्त स्वतुल्यता (Refl: यदि $\varphi \in \Gamma$, तो $\Gamma \vdash \varphi$), एकदिष्टता (Mon), कर्तन (Cut: यदि $\Gamma \vdash \varphi_{i}$ प्रत्येक $i$ के लिए, और $\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi$, तो $\Gamma \vdash \psi$), निगमन प्रमेय (DT) और उसका विलोम (CDT) तथा निगमनतः तुल्यता $\varphi \dashv\vdash \psi$ स्थापित की, जिसका अर्थ है कि $\{\varphi\} \vdash \psi$ और $\{\psi\} \vdash \varphi$; और ऐसे अंकन से, जिसे अभिगृहीत और मोडस पोनेन्स संरक्षित रखते हैं, दिखाया कि वह प्रणाली संयुक्त निषेध के बारे में कुछ सूत्रों को निगमित नहीं करती। निगमन की चार तकनीकों वाले पाठ ने प्राकल्पिक न्यायवाक्य (HS: $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)$), आधार-वाक्यों का विनिमय (IP), दोहरा निषेध (DN: $\varphi \dashv\vdash \neg\neg\varphi$, अपने दो प्रमेयों $\vdash (\neg\neg\varphi \rightarrow \varphi)$ और $\vdash (\varphi \rightarrow \neg\neg\varphi)$ के साथ) और प्रतिपरिवर्तन (CP) उसके तीन रूपों में जोड़े:

दोहरे निषेध को सिद्ध करने के बाद, उसी पाठ ने पाठ्यक्रम की प्रणाली को एक दूसरे मूल नियम, दोहरे निषेध के प्रतिस्थापन (RDN), से पूरा किया: यदि $\chi'$, $\chi$ से किसी उपसूत्र $\theta$ की एक उपस्थिति को $\neg\neg\theta$ से, या किसी उपसूत्र $\neg\neg\theta$ की एक उपस्थिति को $\theta$ से प्रतिस्थापित करने पर प्राप्त होता है, तो $\chi$ से $\chi'$ का अनुमान किया जाता है। पंक्ति $i$ से इस प्रकार प्राप्त पंक्ति का औचित्य RDN$(i)$ से दिया जाता है। उस बिंदु से आगे, $\vdash$ पाठ्यक्रम की प्रणाली (A1 से A3, मोडस पोनेन्स और RDN) को सूचित करता है, जिसमें Refl, Mon, Cut, DT और CDT मान्य बने रहते हैं। नियम आधार-भाषा की प्रतीक-शृंखला पर कार्य करता है, जिससे वह उन उपस्थितियों तक भी पहुँचता है जिन्हें कोई संक्षेपण छिपाता है, और संयुक्त निषेध के दोनों संकार्यों में से किसी में भी; उसके तात्कालिक परिणामों में ये हैं

और, व्यापक रूप से, $\chi \dashv\vdash \chi'$, जब भी $\chi'$, $\chi$ से RDN द्वारा प्राप्त होता है। इस रूप की तुल्यता वाली पंक्ति का औचित्य, पंक्ति संख्या के बिना, “RDN” से दिया जाता है, उसी तरह जैसे “DN” या “CP” वाली पंक्ति किसी पहले से सिद्ध तुल्यता का उद्धरण देती है। वहाँ की तरह, पहले से सिद्ध प्रमेय को किसी निगमन की पंक्ति के रूप में लिखा जा सकता है, क्योंकि उसका अपना निगमन उस स्थान पर बीच में रखा जा सकता है; और उस पाठ की “परिणाम से नियम तक” प्रमेयिका से, प्रत्येक तकनीक आधार-वाक्यों के किसी भी समुच्चय $\Gamma$ के अंतर्गत नियम के रूप में भी लागू होती है, जिसका उद्धरण उन पंक्तियों की संख्याओं के साथ दिया जाता है जिन पर वह लागू होती है, जैसे CP$(i)$ या HS$(i, j)$। निगमनों पर निगमनों में, “आधार-वाक्य” सिद्ध किए जा रहे नियम की किसी परिकल्पना को सूचित करता है।

प्रस्तावात्मक तर्क की भाषा पर पाठ में निर्धारित आधिकारिक संक्षेपण संयोजकों की एकमात्र परिभाषाएँ हैं:

“Def” से औचित्य दी गई पंक्ति कुछ भी निगमित नहीं करती: वह उसी सूत्र को दूसरे नाम से लिखती है, और टिप्पणी बताती है कि कौन-सा संक्षेपण खोला या समेटा जा रहा है (“Def $\rightarrow$”, “Def $\vee$”)। प्राकृतिक भाषा के औपचारिकीकरण पर पाठ में देखी गई घटना को याद रखना उपयोगी है: एक ही सूत्र के कई नाम हो सकते हैं, जिससे एक संयोजन, प्रतीक-शृंखला के रूप में, एक वियोजन भी है। उदाहरण के लिए, $\neg\varphi$ को $\varphi$ के स्थान पर रखकर सोपाधिक को खोलने पर प्राप्त होता है

और $\varphi$ के आगे आने वाला दोहरा निषेध, जिसे संक्षेपण छिपाता है, वह कारण है जिससे RDN नियम आगे आने वाली हर बात में भाग लेगा।

समता के रूप में निगमनतः तुल्यता

इस पाठ की उपपत्तियाँ, लगभग सभी, तुल्यताओं की शृंखलाएँ हैं: $\varphi_{1} \dashv\vdash \varphi_{2}$, $\varphi_{2} \dashv\vdash \varphi_{3}$, और इसी प्रकार आगे। किसी शृंखला से $\varphi_{1} \dashv\vdash \varphi_{n}$ निष्कर्ष निकालने के लिए निगमनतः तुल्यता को समता की तरह व्यवहार करना चाहिए, और यही बात औपचारिक निगमन प्रणालियों पर पाठ के निगमनतः तुल्यता के गुणों वाले साध्य ने स्थापित की: संबंध स्वतुल्य ($\varphi \dashv\vdash \varphi$), सममित (यदि $\varphi \dashv\vdash \psi$, तो $\psi \dashv\vdash \varphi$) और संक्रामक (यदि $\varphi \dashv\vdash \psi$ और $\psi \dashv\vdash \chi$, तो $\varphi \dashv\vdash \chi$) है, और दो निगमनतः तुल्य सूत्र निष्कर्षों के रूप में परस्पर विनिमेय हैं (यदि $\Gamma \vdash \varphi$ और $\varphi \dashv\vdash \varphi'$, तो $\Gamma \vdash \varphi'$, सूत्रों के प्रत्येक समुच्चय $\Gamma$ के लिए)। यह याद रखना उपयोगी है कि अंतिम दो को कैसे सिद्ध किया गया था, क्योंकि पूरा पाठ उन्हीं पर टिका है: $\{\varphi\} \vdash \varphi'$ से, एकदिष्टता द्वारा, $\Gamma \cup \{\varphi\} \vdash \varphi'$ तक पहुँचते हैं, और इससे तथा $\Gamma \vdash \varphi$ से, कर्तन द्वारा, $\Gamma \vdash \varphi'$ तक; संक्रामकता इसे एक दिशा में $\Gamma = \{\varphi\}$ के साथ और दूसरी में $\Gamma = \{\chi\}$ के साथ लागू करने से प्राप्त होती है।

आगे से, जो चरण तुल्यताओं की किसी शृंखला को एक ही तुल्यता में समेटता है, उसका औचित्य “Cut” से दिया जाता है, जो उस साध्य का उपकरण है। परंतु प्रत्येक कड़ी $\varphi_{i} \dashv\vdash \varphi_{i+1}$ में दोनों निगमन होते हैं, जाने का और लौटने का; अतः तुल्यताओं की शृंखला अपने निष्कर्ष की दोनों दिशाएँ एक साथ सिद्ध करती है, और कुछ भी “अभ्यास के रूप में” शेष नहीं रहता।