सामग्री पर जाएँ
Topos Uranos

सारांश

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

अधिगम उद्देश्य

  1. इकाई के परिणामों के तार्किक क्रम का पुनर्निर्माण करना, यह बताते हुए कि प्रत्येक परिणाम किन पूर्ववर्ती परिणामों पर टिका है और किस पाठ में सिद्ध हुआ, और संहतता तथा प्रबल पूर्णता के क्रम का कारण समझाना।
  2. यह समझाना कि भाषा, निगमन और शब्दार्थ ⊢\vdash और ⊨\models के संपात में कैसे मिलते हैं, और पाठ्यक्रम की प्रत्येक इकाई का कौन-सा परिणाम इस संपात के लिए अनिवार्य है।
  3. यह भेद करना कि पाठ्यक्रम ने क्या सिद्ध किया, क्या स्वीकार किया (अभिगृहीत-योजनाएँ, मूल नियम और आगमन) और क्या खुला छोड़ा (संतोषणीयता का निर्णय करने की लागत और परिमाणकों वाला तर्क)।
  4. ऐसी समस्याएँ हल करना जो अंकन, काल्मार प्रमेयिका, समरूप स्थापन, संहतता और विभेदन को जोड़ती हैं, और प्रत्येक स्थिति में संपात की आसान दिशा का लाभ उठाना।

इकाई की उपलब्धियाँ

इकाई का लक्ष्य उन दो संबंधों की तुलना करना था जिन्हें पिछली इकाइयों ने एक ही भाषा पर खड़ा किया था, अर्थात् निगम्यता Γ⊢φ\Gamma \vdash \varphi और शब्दार्थीय परिणाम Γ⊨φ\Gamma \models \varphi, और यह सिद्ध करना कि वे संपाती हैं। कथन के रूप में यह लक्ष्य बिना किसी आरक्षण के प्राप्त हुआ: आधार-वाक्यों के किसी भी समुच्चय के लिए, परिमित हो या अनंत, दोनों एक ही संबंध हैं, और विभेदन परिणाम का निर्णय करने का तीसरा तरीका देता है, जो उतना ही सुदृढ़ और पूर्ण है। आरक्षण विधियों में हैं, और प्रत्येक का उल्लेख अपने स्थान पर किया गया: पहले पाठ की पूर्णता रचनात्मक है, पर व्यावहारिक नहीं, क्योंकि वह जो निगमन उत्पन्न करती है वे सत्यता सारणी जितने लंबे होते हैं; संहतता किसी मान-नियतन के अस्तित्व की गारंटी देती है, पर उसे ढूँढना नहीं सिखाती; विभेदन निर्णय करता है, पर सबसे बुरी स्थिति में उसकी लागत एक खुला प्रश्न है। इन आरक्षणों के साथ, तय किया गया मार्ग चार खंडों वाली निगमन की एक शृंखला के रूप में पढ़ा जा सकता है।

सुदृढ़ता

सुदृढ़ता और पूर्णता वाले पाठ ने पहले शब्दावली तय की: कोई प्रणाली सुदृढ़ है यदि Γ⊢φ⇒Γ⊨φ\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi, और पूर्ण है यदि इसका विलोम लागू हो, और पूर्णता के तीन स्तर हैं (दुर्बल, परिमित समुच्चयों के लिए और प्रबल)। उसने उस चक्रीय युक्ति का पर्दाफ़ाश किया जो पूर्णता को “सुदृढ़ता से” प्राप्त करना चाहती है, और जो ⊬χ\nvdash \chi से ⊭χ\not\models \chi पर जाती है, जबकि यह कदम वास्तव में दुर्बल पूर्णता का प्रतिपरिवर्तित कथन है; और उसने दिखाया कि दोनों गुण एक-दूसरे से स्वतंत्र हैं। फिर उसने सिद्ध किया कि A1, A2 और A3 का प्रत्येक दृष्टांत वैध है, क्योंकि उसे असत्य बनाने वाला मान-नियतन मानने पर सोपाधिक की असत्य पंक्ति से असंभव मान प्राप्त होते हैं; और पंक्तियों की संख्या पर प्रबल आगमन द्वारा सुदृढ़ता सिद्ध की, जिसमें एक स्थिति अभिगृहीतों की है, एक आधार-वाक्यों की, एक शब्दार्थीय मोडस पोनेन्स की, और RDN नियम के लिए तुल्यता θ≡¬¬θ\theta \eqsem \neg\neg\theta तथा शब्दार्थीय प्रतिस्थापन प्रमेय का उपयोग होता है। जो गुण पंक्ति से पंक्ति तक जाता है वह वैधता नहीं है, बल्कि आधार-वाक्यों को संतुष्ट करने वाले एक नियत मान-नियतन द्वारा संतुष्ट होना है, और इसीलिए सुदृढ़ता आधार-वाक्यों के होने पर भी लागू होती है, चाहे वे अनंत हों। इससे प्रत्येक संतोषणीय समुच्चय की संगति निकली, विशेष रूप से स्वयं प्रणाली की संगति, और वह विधि भी जो निगमन की इकाई के पास नहीं थी: एक प्रतिमॉडल यह सिद्ध करता है कि कोई निगमन मौजूद नहीं है।

काल्मार और परिमित पूर्णता

उसी पाठ ने विलोम दो चरणों में सिद्ध किया। पहला चरण काल्मार प्रमेयिका है: यदि φ\varphi के चर u1,…,unu_{1}, \ldots, u_{n} में हैं, तो {u1v,…,unv}⊢φv\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}, प्रत्येक मान-नियतन vv के लिए, जहाँ ψv\psi^{v} या तो ψ\psi है यदि v(ψ)=1v(\psi) = 1, या ¬ψ\neg\psi है अन्यथा; प्रणाली प्रत्येक पंक्ति से वह निगमित करती है जो वह पंक्ति सूत्र के बारे में कहती है। जटिलता पर उसके आगमन में केवल एक संयुक्त स्थिति है, (α↓β)(\alpha \downarrow \beta), क्योंकि संयुक्त निषेध ही एकमात्र मूल संयोजक है, और उसमें तीन उप-स्थितियाँ हैं, जो प्रणाली की दो प्रमेयिकाओं की माँग करती हैं, जिनमें दूसरी दो रूपों में है: ⊢(¬α→(¬β→(α↓β)))\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta))), जो संयोजन के प्रवेश, दोहरे निषेध और RDN नियम के दो अनुप्रयोगों से निगमित होती है, तथा ⊢(α→¬(α↓β))\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta)) और ⊢(β→¬(α↓β))\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta)), जो वियोजन के प्रवेश से निगमित होती हैं। दूसरा चरण आधार-वाक्यों को हटाता है: यदि φ\varphi पुनरुक्ति है, तो वह 2n2^{n} पंक्तियों में से प्रत्येक के आधार-वाक्यों से निगमित होता है, और स्थिति-भेद से उपपत्ति पहले अंतिम चर का लिटरल हटाती है, फिर उपांतिम का, और इसी तरह ⊢φ\vdash \varphi तक पहुँचती है, जो दुर्बल पूर्णता है। शब्दार्थीय निगमन प्रमेय और वाक्यात्मक निगमन प्रमेय के विलोम से पूर्णता का विस्तार आधार-वाक्यों के परिमित समुच्चयों तक हुआ; इसलिए परिमित आधार-वाक्यों के लिए निगमन और परिणाम संपाती हैं, सिद्ध तुल्यता शब्दार्थीय तुल्यता से संपाती है, और निगम्यता निर्णेय है, क्योंकि सारणी उसका उत्तर देती है।

संहतता और प्रबल पूर्णता

संहतता प्रमेय वाले पाठ ने अनंत स्थिति का सामना किया, जहाँ काल्मार प्रमेयिका नहीं पहुँचती, क्योंकि अनंत आधार-वाक्य किसी एक सोपाधिक में नहीं उतारे जा सकते। उसने, किसी भी निगमन का उल्लेख किए बिना, सिद्ध किया कि एक समुच्चय संतोषणीय है यदि और केवल यदि उसका प्रत्येक परिमित उपसमुच्चय संतोषणीय है। v1,…,vnv_{1}, \ldots, v_{n} के लिए मानों का एक अनुक्रम अच्छा कहलाता है यदि समुच्चय का प्रत्येक परिमित उपसमुच्चय उसे विस्तारित करने वाले किसी मान-नियतन से संतुष्ट होता है; दो साक्षियों की प्रमेयिका यह सुनिश्चित करती है कि एक अच्छा अनुक्रम एक अच्छे अनुक्रम में विस्तारित होता है, क्योंकि यदि दोनों में से कोई भी विस्तार अच्छा न हो, तो दो परिमित साक्षियों का सम्मिलन इस बात का खंडन करेगा कि अनुक्रम अच्छा है; और जहाँ संभव हो वहाँ सदा 11 को वरीयता देने से जो मान-नियतन प्राप्त होता है वह प्रत्येक सूत्र को संतुष्ट करता है, संपाती प्रमेयिका से, क्योंकि प्रत्येक सूत्र में परिमित चर होते हैं। इस रचना को चयन अभिगृहीत की आवश्यकता नहीं, क्योंकि चर क्रमांकित हैं और प्रत्येक चरण का एक नियम है। संहतता से उसके तुल्य रूप निकले, असंतोषणीयता का रूप और परिणाम का रूप; इस अंतिम से, परिमित आधार-वाक्यों के लिए पूर्णता से और एकदिष्टता से प्रबल पूर्णता निकली; और उससे तथा सुदृढ़ता से पूर्ण संपात निकला: Γ⊢φ⇔Γ⊨φ\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi, प्रत्येक Γ\Gamma के लिए, और एक समुच्चय संगत है यदि और केवल यदि वह संतोषणीय है। पाठ ने सचेत किया कि यह क्रम रुचि का विषय नहीं है: संहतता को एक ऐसी प्रबल पूर्णता से प्राप्त करना जो अभी उपलब्ध नहीं है, चक्रीय होगा। पाठ गणनीय ग्राफों के रंजन के साथ समाप्त हुआ, जो एक अनंत समस्या को ऐसे सूत्र-समुच्चय में अनूदित करता है जिसके परिमित भाग संतोषणीय हैं, और इस बात की सीमाओं के साथ कि सूत्रों का एक समुच्चय क्या व्यक्त कर सकता है।

विभेदन

विभेदन विधि वाले पाठ ने सूत्रों के समुच्चय के स्थान पर उपवाक्यों के समुच्चय रखे, जहाँ उपवाक्य लिटरलों के परिमित समुच्चय हैं, और इसके दो निरूपण हैं: उपवाक्य रूप, जिसके वही मॉडल हैं, और परिभाषात्मक रूप, जो प्रत्येक संयुक्त उपलेखन के लिए एक नया चर लाता है, केवल संतोषणीयता को सुरक्षित रखता है और दो की घात की तरह नहीं, सूत्र की तरह बढ़ता है। उपवाक्यों पर एक ही नियम काम करता है: CC और DD से, जहाँ ℓ∈C\ell \in C और ℓ∗∈D\ell^{*} \in D, (C∖{ℓ})∪(D∖{ℓ∗})(C \setminus \{\ell\}) \cup (D \setminus \{\ell^{*}\}) प्राप्त होता है; खंडन वह व्युत्पत्ति है जो □\Box तक पहुँचती है। सुदृढ़ता प्रणाली की सुदृढ़ता की तरह व्युत्पत्ति पर आगमन द्वारा सिद्ध हुई, इस बात का उपयोग करके कि विभेदक अपने आधार-वाक्यों का परिणाम है, और खंडन पूर्णता चरों की संख्या पर आगमन द्वारा, एक चर के निरसन के माध्यम से, जो संतोषणीयता को सुरक्षित रखता है और जिसकी उपपत्ति एक मॉडल की रचना करती है; अनंत समुच्चयों के लिए, फिर से संहतता द्वारा। इससे निकलता है कि Γ⊨φ\Gamma \models \varphi यदि और केवल यदि Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} के एक उपवाक्य रूप का खंडन है, और यह कि संतृप्ति परिमित है, क्योंकि nn चरों के साथ 4n4^{n} से अधिक उपवाक्य नहीं होते, और सत्यता सारणी के बिना संतोषणीयता का निर्णय करती है। पाठ ने संतोषणीयता की समस्या प्रस्तुत की, जिसकी सबसे बुरी स्थिति की लागत कोई नहीं जानता, और दो ऐसी स्थितियाँ जिनका निर्णय शीघ्र होता है: हॉर्न उपवाक्य और दो लिटरलों वाले उपवाक्य।

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

शृंखला के आधार

  • Aआगमन और पुनरावर्तन. प्राकृत संख्याओं पर प्रबल आगमन, सूत्र की जटिलता पर आगमन (जिसकी एकमात्र संयुक्त स्थिति (α↓β)(\alpha \downarrow \beta) है) और पुनरावर्तन द्वारा परिभाषाएँ। पहली इकाई में सिद्ध। इस इकाई में बिना प्रमाण के स्वीकार किया गया।
  • Bपाठ्यक्रम की प्रणाली. A1, A2, A3, मोडस पोनेन्स और RDN नियम; स्वतुल्यता, एकदिष्टता, निगमनों के बीच मोडस पोनेन्स, परिमितता और Γ∪{φ}⊢ψ⇔Γ⊢(φ→ψ)\Gamma \cup \{\varphi\} \vdash \psi \Leftrightarrow \Gamma \vdash (\varphi \rightarrow \psi)। दूसरी इकाई में निर्धारित। इस इकाई में बिना प्रमाण के स्वीकार किया गया।
  • Cव्युत्पन्न तकनीकें. दोहरा निषेध, चार निगमन तकनीकों वाले पाठ से; संयोजन का प्रवेश, वियोजन का प्रवेश और स्थिति-भेद से उपपत्ति (यदि Γ∪{ψ}⊢χ\Gamma \cup \{\psi\} \vdash \chi और Γ∪{¬ψ}⊢χ\Gamma \cup \{\neg\psi\} \vdash \chi, तो Γ⊢χ\Gamma \vdash \chi), शास्त्रीय तर्क की तकनीकों वाले पाठ से। दूसरी इकाई में सिद्ध। इस इकाई में बिना प्रमाण के स्वीकार किया गया।
  • Dमान-नियतन और संपात. v((α↓β))=(1−v(α))(1−v(β))v((\alpha \downarrow \beta)) = (1 - v(\alpha))(1 - v(\beta)); यदि दो मान-नियतन V(φ)V(\varphi) पर संपाती हों, तो वे φ\varphi को एक ही मान देते हैं; वैधता का निर्णय 2n2^{n} पंक्तियों से होता है। तीसरी इकाई में सिद्ध। इस इकाई में बिना प्रमाण के स्वीकार किया गया।
  • Eशब्दार्थीय परिणाम. सोपाधिक की असत्य पंक्ति, एकदिष्टता, Γ∪{φ}⊨ψ⇔Γ⊨(φ→ψ)\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi), Γ⊨φ\Gamma \models \varphi यदि और केवल यदि Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} असंतोषणीय है, और शब्दार्थीय प्रतिस्थापन प्रमेय। तीसरी इकाई में सिद्ध। इस इकाई में बिना प्रमाण के स्वीकार किया गया।
  • Fसंयोजक रूप. मान प्रमेयिका; प्रत्येक सूत्र एक संयोजक प्रसामान्य रूप के तुल्य है, जिसके लिए 2n2^{n} उपवाक्यों की आवश्यकता हो सकती है; लिटरलों का एक वियोजन वैध है यदि और केवल यदि उसमें एक पूरक युग्म है। तीसरी इकाई में सिद्ध। इस इकाई में बिना प्रमाण के स्वीकार किया गया।
  • Gसुदृढ़ता. यदि Γ⊢φ\Gamma \vdash \varphi, तो Γ⊨φ\Gamma \models \varphi, प्रत्येक समुच्चय Γ\Gamma के लिए; एक प्रतिमॉडल सिद्ध करता है कि कोई निगमन मौजूद नहीं है। स्थापित होता है: 2. सुदृढ़ता.
  • Hसंहतता. सूत्रों का एक समुच्चय संतोषणीय है यदि और केवल यदि उसका प्रत्येक परिमित उपसमुच्चय संतोषणीय है; इसलिए एक असंतोषणीय समुच्चय किसी परिमित भाग में पहले से ही असंतोषणीय होता है। स्थापित होता है: 11. संहतता प्रमेय.
  1. खंड 1 सुदृढ़ता

    • सारणी बनाए बिना जाँचना कि किसी योजना का प्रत्येक दृष्टांत वैध है।
    • पंक्तियों की संख्या पर प्रबल आगमन द्वारा सुदृढ़ता सिद्ध करना, RDN नियम की स्थिति सहित।
    • प्रतिमॉडल से सिद्ध करना कि कोई सूत्र निगम्य नहीं है, और सुदृढ़ता से संगति प्राप्त करना।
    1. अभिगृहीतों की वैधता. A1, A2 और A3 का प्रत्येक दृष्टांत वैध है: उसे असत्य बनाने वाले मान-नियतन को, सोपाधिक की असत्य पंक्ति के कारण, असंभव मानों की आवश्यकता होगी।

      आधार: E (शब्दार्थीय परिणाम). सिद्ध किया गया: सुदृढ़ता और पूर्णता.

    2. सुदृढ़ता. यदि Γ⊢φ\Gamma \vdash \varphi, तो Γ⊨φ\Gamma \models \varphi, प्रत्येक Γ\Gamma के लिए: पंक्तियों की संख्या पर प्रबल आगमन द्वारा, अभिगृहीतों की एक स्थिति, आधार-वाक्यों की एक, शब्दार्थीय मोडस पोनेन्स, और RDN नियम के लिए θ≡¬¬θ\theta \eqsem \neg\neg\theta तथा शब्दार्थीय प्रतिस्थापन।

      उपयोग करती है: 1. अभिगृहीतों की वैधता. आधार: A (आगमन और पुनरावर्तन), B (पाठ्यक्रम की प्रणाली), E (शब्दार्थीय परिणाम). सिद्ध किया गया: सुदृढ़ता और पूर्णता.

    3. संगति और प्रतिमॉडल. प्रत्येक संतोषणीय समुच्चय संगत है; प्रणाली संगत है और ⊬v1\nvdash v_{1}; यदि कोई मान-नियतन Γ\Gamma को संतुष्ट करता है और φ\varphi को असत्य बनाता है, तो Γ⊬φ\Gamma \nvdash \varphi, और सारणी इसे सिद्ध करती है: जो वैध नहीं वह प्रमेय नहीं है।

      आधार: G (सुदृढ़ता), D (मान-नियतन और संपात). सिद्ध किया गया: सुदृढ़ता और पूर्णता.

  2. खंड 2 काल्मार और परिमित पूर्णता

    • संयुक्त निषेध की दो प्रमेयिकाओं को प्रणाली में निगमित करना, आवश्यकता होने पर RDN नियम के साथ।
    • एक ही संयुक्त स्थिति वाले जटिलता पर आगमन से काल्मार प्रमेयिका सिद्ध करना।
    • स्थिति-भेद से उपपत्ति द्वारा पंक्तियों के आधार-वाक्य हटाना और दोनों निगमन प्रमेयों से परिमित आधार-वाक्य उतारना।
    • परिमित आधार-वाक्यों के साथ निगम्यता, सिद्ध तुल्यता और संगति का सारणी से निर्णय करना।
    1. संयुक्त निषेध का प्रवेश. {¬α,¬β}⊢(α↓β)\{\neg\alpha, \neg\beta\} \vdash (\alpha \downarrow \beta) और ⊢(¬α→(¬β→(α↓β)))\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta))): निषेधों का संयोजन ¬¬(¬¬α↓¬¬β)\neg\neg(\neg\neg\alpha \downarrow \neg\neg\beta) है; दोहरा निषेध बाहरी निषेध हटाता है और RDN नियम दोनों भीतरी निषेध।

      आधार: B (पाठ्यक्रम की प्रणाली), C (व्युत्पन्न तकनीकें). सिद्ध किया गया: सुदृढ़ता और पूर्णता.

    2. संयुक्त निषेध का निषेध. ⊢(α→¬(α↓β))\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta)) और ⊢(β→¬(α↓β))\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta)), क्योंकि ¬(α↓β)\neg(\alpha \downarrow \beta) और कुछ नहीं, (α∨β)(\alpha \vee \beta) ही है, और वियोजन का प्रवेश पर्याप्त है।

      आधार: B (पाठ्यक्रम की प्रणाली), C (व्युत्पन्न तकनीकें). सिद्ध किया गया: सुदृढ़ता और पूर्णता.

    3. काल्मार प्रमेयिका. यदि V(φ)⊆{u1,…,un}V(\varphi) \subseteq \{u_{1}, \ldots, u_{n}\}, तो {u1v,…,unv}⊢φv\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}, प्रत्येक मान-नियतन vv के लिए; आगमनिक चरण में केवल एक स्थिति है, (α↓β)(\alpha \downarrow \beta), जिसकी α\alpha और β\beta के मानों के अनुसार तीन उप-स्थितियाँ हैं।

      उपयोग करती है: 4. संयुक्त निषेध का प्रवेश, 5. संयुक्त निषेध का निषेध. आधार: A (आगमन और पुनरावर्तन), D (मान-नियतन और संपात), B (पाठ्यक्रम की प्रणाली). सिद्ध किया गया: सुदृढ़ता और पूर्णता.

    4. दुर्बल पूर्णता. यदि ⊨φ\models \varphi, तो ⊢φ\vdash \varphi: काल्मार प्रमेयिका प्रत्येक पंक्ति से φ\varphi निगमित करती है, और स्थिति-भेद से उपपत्ति अंतिम चर से पहले चर तक लिटरल हटाती है, जिसमें प्रमेयिका का 2n2^{n} बार और स्थिति-भेद से उपपत्ति का 2n−12^{n} - 1 बार उपयोग होता है।

      उपयोग करती है: 6. काल्मार प्रमेयिका. आधार: C (व्युत्पन्न तकनीकें). सिद्ध किया गया: सुदृढ़ता और पूर्णता.

    5. परिमित आधार-वाक्यों के लिए पूर्णता. {γ1,…,γk}⊨φ⇒{γ1,…,γk}⊢φ\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi \Rightarrow \{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi: शब्दार्थीय निगमन प्रमेय एक पुनरुक्ति तक ले जाता है, दुर्बल पूर्णता उसे निगमित करती है और निगमन प्रमेय का विलोम आधार-वाक्यों को लौटा देता है।

      उपयोग करती है: 7. दुर्बल पूर्णता. आधार: E (शब्दार्थीय परिणाम), B (पाठ्यक्रम की प्रणाली). सिद्ध किया गया: सुदृढ़ता और पूर्णता.

    6. परिमित संपात और निर्णय. परिमित Γ\Gamma के लिए, Γ⊢φ⇔Γ⊨φ\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi और φ⊣⊢ψ⇔φ≡ψ\varphi \dashv\vdash \psi \Leftrightarrow \varphi \eqsem \psi; इसलिए परिमित आधार-वाक्यों से निगम्यता सत्यता सारणी द्वारा निर्णेय है।

      उपयोग करती है: 8. परिमित आधार-वाक्यों के लिए पूर्णता. आधार: G (सुदृढ़ता), D (मान-नियतन और संपात). सिद्ध किया गया: सुदृढ़ता और पूर्णता.

  3. खंड 3 संहतता और प्रबल पूर्णता

    • चरों के मान एक-एक करके नियत करते हुए संहतता सिद्ध करना, अच्छे अनुक्रमों के निश्चर और दो साक्षियों के तर्क के साथ।
    • संतोषणीयता, असंतोषणीयता और परिणाम के रूपों के बीच आना-जाना।
    • बिना चक्रीयता के संहतता से प्रबल पूर्णता प्राप्त करना, और उससे संगति तथा संतोषणीयता का संपात।
    • अनंत वस्तुओं के बारे में समस्याओं को सूत्र-समुच्चयों के रूप में कूटबद्ध करना और उन्हें संहतता से हल करना।
    1. दो साक्षियों की प्रमेयिका. यदि पहले से नियत मानों का अनुक्रम ss अच्छा है (समुच्चय का प्रत्येक परिमित उपसमुच्चय उसे विस्तारित करने वाले किसी मान-नियतन से संतुष्ट होता है), तो (s,1)(s, 1) या (s,0)(s, 0) अच्छा है: यदि दोनों में से कोई न हो, तो दो परिमित साक्षियों का सम्मिलन इस बात का खंडन करेगा कि ss अच्छा है।

      आधार: D (मान-नियतन और संपात). सिद्ध किया गया: संहतता प्रमेय.

    2. संहतता प्रमेय. Γ\Gamma संतोषणीय है यदि और केवल यदि उसका प्रत्येक परिमित उपसमुच्चय संतोषणीय है: vn+1v_{n + 1} को 11 पर नियत करने पर यदि (sn,1)(s_{n}, 1) अच्छा है, और अन्यथा 00 पर, जो मान-नियतन प्राप्त होता है वह संपाती प्रमेयिका से प्रत्येक सूत्र को संतुष्ट करता है। चयन अभिगृहीत की आवश्यकता नहीं, क्योंकि चर क्रमांकित हैं।

      उपयोग करती है: 10. दो साक्षियों की प्रमेयिका. आधार: A (आगमन और पुनरावर्तन), D (मान-नियतन और संपात). सिद्ध किया गया: संहतता प्रमेय.

    3. तुल्य रूप. Γ\Gamma असंतोषणीय है यदि और केवल यदि उसका कोई परिमित भाग असंतोषणीय है; Γ⊨φ\Gamma \models \varphi यदि और केवल यदि Γ0⊨φ\Gamma_{0} \models \varphi, किसी परिमित Γ0⊆Γ\Gamma_{0} \subseteq \Gamma के लिए; और यह अंतिम रूप, बदले में, प्रमेय का निहितार्थ देता है।

      उपयोग करती है: 11. संहतता प्रमेय. आधार: E (शब्दार्थीय परिणाम). सिद्ध किया गया: संहतता प्रमेय.

    4. प्रबल पूर्णता. यदि Γ⊨φ\Gamma \models \varphi, तो Γ⊢φ\Gamma \vdash \varphi, प्रत्येक Γ\Gamma के लिए: परिणाम का रूप एक परिमित Γ0\Gamma_{0} देता है, परिमित आधार-वाक्यों के लिए पूर्णता Γ0⊢φ\Gamma_{0} \vdash \varphi देती है, और एकदिष्टता Γ⊢φ\Gamma \vdash \varphi देती है।

      उपयोग करती है: 8. परिमित आधार-वाक्यों के लिए पूर्णता, 12. तुल्य रूप. आधार: B (पाठ्यक्रम की प्रणाली). सिद्ध किया गया: संहतता प्रमेय.

    5. निगमन ही परिणाम है. Γ⊢φ⇔Γ⊨φ\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi, प्रत्येक Γ\Gamma के लिए; प्रमेय ठीक-ठीक पुनरुक्तियाँ हैं, और एक समुच्चय संगत है यदि और केवल यदि वह संतोषणीय है।

      उपयोग करती है: 13. प्रबल पूर्णता. आधार: G (सुदृढ़ता). सिद्ध किया गया: संहतता प्रमेय.

    6. गणनीय ग्राफों का रंजन. प्रत्येक शीर्ष और प्रत्येक रंग के लिए एक चर xi,cx_{i,c} लेकर, और ऐसे सूत्र लेकर जो कहते हैं कि प्रत्येक शीर्ष का ठीक एक रंग है और आसन्न शीर्षों के रंग भिन्न हैं, एक गणनीय ग्राफ kk रंगों से रंजनीय है यदि उसका प्रत्येक परिमित उपग्राफ रंजनीय है।

      आधार: H (संहतता), F (संयोजक रूप). सिद्ध किया गया: संहतता प्रमेय.

  4. खंड 4 विभेदन

    • सूत्रों के एक समुच्चय को संयोजक रूप या परिभाषात्मक रूप द्वारा उपवाक्यों के समुच्चय के रूप में व्यक्त करना।
    • एक ही चरण में दो पूरक युग्मों को हटाए बिना खंडन बनाना।
    • विभेदन की सुदृढ़ता और खंडन पूर्णता सिद्ध करना, पहले परिमित समुच्चयों के लिए और फिर संहतता से किसी भी समुच्चय के लिए।
    • संतृप्ति से परिणाम का निर्णय करना और उन स्थितियों को पहचानना जिनका निर्णय शीघ्र होता है।
    1. उपवाक्य रूप. एक उपवाक्य लिटरलों का परिमित समुच्चय है, जो तब संतुष्ट होता है जब उसका कोई लिटरल 11 मान लेता है, और □\Box असंतोषणीय है; Γ\Gamma के एक उपवाक्य रूप के वही मॉडल हैं, और Γ⊨φ\Gamma \models \varphi यदि और केवल यदि Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} का एक उपवाक्य रूप असंतोषणीय है।

      आधार: F (संयोजक रूप), E (शब्दार्थीय परिणाम). सिद्ध किया गया: विभेदन विधि.

    2. परिभाषात्मक उपवाक्य रूप. प्रत्येक उपलेखन के लिए एक नया चर और उसके परिभाषात्मक उपवाक्य लेने पर, T(φ)T(\varphi) और φ\varphi समसंतोषणीय हैं, और अधिक से अधिक 4k+14k + 1 उपवाक्य हैं, प्रत्येक में अधिक से अधिक तीन लिटरल; परिभाषात्मक रूप परिमित आधार-वाक्यों के साथ परिणाम का निर्णय करता है।

      उपयोग करती है: 16. उपवाक्य रूप. आधार: A (आगमन और पुनरावर्तन), D (मान-नियतन और संपात). सिद्ध किया गया: विभेदन विधि.

    3. विभेदन की सुदृढ़ता. {C,D}⊨Rℓ(C,D)\{C, D\} \models R_{\ell}(C, D), ℓ\ell के मान पर स्थिति-भेद से; व्युत्पत्ति पर प्रबल आगमन द्वारा, S⊨CS \models C, प्रत्येक उपवाक्य CC के लिए जो SS से व्युत्पन्न हो, और यदि SS का खंडन है, तो वह असंतोषणीय है।

      उपयोग करती है: 16. उपवाक्य रूप. आधार: A (आगमन और पुनरावर्तन). सिद्ध किया गया: विभेदन विधि.

    4. एक चर का निरसन. Ep(S)E_{p}(S), जो उन उपवाक्यों को रखता है जिनमें न pp है न ¬p\neg p और pp पर विभेदक जोड़ता है, उसमें pp नहीं है और वह SS के साथ समसंतोषणीय है; उसके एक मॉडल से SS का एक मॉडल प्राप्त होता है, pp का मान चुनकर।

      उपयोग करती है: 18. विभेदन की सुदृढ़ता. आधार: D (मान-नियतन और संपात). सिद्ध किया गया: विभेदन विधि.

    5. परिमित खंडन पूर्णता. उपवाक्यों के प्रत्येक परिमित और असंतोषणीय समुच्चय का खंडन होता है, चरों की संख्या पर आगमन से: अंतिम चर का निरसन करके और प्रत्येक विभेदक के आधार-वाक्य बीच में डालकर।

      उपयोग करती है: 19. एक चर का निरसन. आधार: A (आगमन और पुनरावर्तन). सिद्ध किया गया: विभेदन विधि.

    6. खंडन पूर्णता. उपवाक्यों का एक समुच्चय, परिमित हो या अनंत, असंतोषणीय है यदि और केवल यदि उसका खंडन है; इसलिए Γ⊨φ\Gamma \models \varphi यदि और केवल यदि Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} के एक उपवाक्य रूप का खंडन है।

      उपयोग करती है: 16. उपवाक्य रूप, 18. विभेदन की सुदृढ़ता, 20. परिमित खंडन पूर्णता. आधार: H (संहतता). सिद्ध किया गया: विभेदन विधि.

    7. संतृप्ति निर्णय करती है. nn चरों के साथ व्युत्पन्न उपवाक्यों के समुच्चय में अधिक से अधिक 4n4^{n} अवयव होते हैं; संतृप्ति रुकती है और सत्यता सारणी के बिना संतोषणीयता का निर्णय करती है, यद्यपि सदा उससे अधिक तेज़ नहीं।

      उपयोग करती है: 18. विभेदन की सुदृढ़ता, 20. परिमित खंडन पूर्णता. सिद्ध किया गया: विभेदन विधि.

पाठ्यक्रम कहाँ पहुँचता है. शृंखला वहाँ समाप्त होती है जहाँ पाठ्यक्रम के दोनों पक्ष एक ही संबंध के रूप में पहचाने जाते हैं और उसका निर्णय करने की विधियाँ उपलब्ध होती हैं। जो खुला रहता है वह अब प्रस्तावात्मक तर्क के बारे में प्रश्न नहीं है, बल्कि उसकी लागत और परिमाणकों तक उसके विस्तार के बारे में है।