हिल्बर्ट प्रणाली

गणितीय भौतिकी में, हिल्बर्ट प्रणाली C*- वर्णित भौतिक प्रणाली के लिए बीजगणित द्वारा कम उपयोग किया जाने वाला शब्द है।

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

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

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

निगमनात्मक तर्क

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

मान लीजिए $\Gamma$ सूत्रों का समूह है, जिसे परिकल्पना माना जाता है। उदाहरण के लिए, $\Gamma$ समूह सिद्धांत या समुच्चय सिद्धांत के लिए अभिगृहीतों का समुच्चय हो सकता है। अंकन $\Gamma \vdash \phi$ इसका मतलब है कि एक निगमन है जो समाप्त होती है $\phi$ अभिगृहीतों के रूप में केवल तार्किक अभिगृहीतों और तत्वों $\Gamma$ का उपयोग करना है। इस प्रकार, अनौपचारिक रूप से, $\Gamma \vdash \phi$ मतलब कि $\phi$ में सभी सूत्रों $\Gamma$ को मानकर सिद्ध होता है।

हिल्बर्ट-शैली की निगमन प्रणालियों को तार्किक अभिगृहीतों की कई स्कीमा के उपयोग की विशेषता है। अभिगृहीत स्कीमा विशिष्ट स्वरूप में किसी रूप के सभी सूत्रों को प्रतिस्थापित करके प्राप्त अभिगृहीतों का अनंत समुच्चय है। तार्किक अभिगृहीतों के समुच्चय में न केवल वे अभिगृहीत सम्मिलित होते हैं जो इस पैटर्न से उत्पन्न होते हैं, बल्कि उनमें से किसी एक अभिगृहीत का सामान्यीकरण भी सम्मिलित होता है। सूत्र पर शून्य या अधिक सार्वभौम परिमाणक लगाकर सूत्र का सामान्यीकरण प्राप्त किया जाता है; उदाहरण के लिए $\forall y(\forall xPxy\to Pty)$ का सामान्यीकरण $\forall xPxy\to Pty$ है।

तार्किक सिद्धांत

विधेय तर्क के कई प्रकार के अभिगृहीत हैं, क्योंकि किसी भी तर्क के लिए अभिगृहीतों और नियमों को चुनने की स्वतंत्रता है जो उस तर्क को चित्रित करते हैं। हम यहां हिल्बर्ट प्रणाली का वर्णन करते हैं जिसमें नौ अभिगृहीत और सिर्फ नियम सरल तर्क हैं, जिसे हम एक-नियम अभिगृहीत कहते हैं और जो चिरसम्मत समीकरण तर्क का वर्णन करता है। हम इस तर्क के लिए न्यूनतम भाषा से संबोधित हैं, जहाँ सूत्र केवल संयोजकों का उपयोग करते हैं $\lnot$ और $\to$ और केवल परिमाणक $\forall$ हैं, बाद में हम दिखाते हैं कि अतिरिक्त तार्किक संयोजकों को सम्मिलित करने के लिए प्रणाली को कैसे बढ़ाया जा सकता है, जैसे $\land$ और $\lor$ निगमन योग्य सूत्रों के वर्ग को बढ़ाए बिना बढ़ाया जा सकता है।

तार्किक संयोजकों के परिचालन के लिए पहली चार तार्किक अभिगृहीत स्कीमा (सरल तर्क के साथ) अनुमति देती हैं।

P1. $\phi \to \phi$

P2. $\phi \to \left(\psi \to \phi \right)$

P3. $\left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)$

P4. $\left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)$

अभिगृहीत P1 अनावश्यक है, क्योंकि यह P3, P2 और सरल तर्क से आता है (देखें) ये अभिगृहीत शास्त्रीय प्रस्तावात्मक तर्क का वर्णन करते हैं; अभिगृहीत P4 के बिना हमें प्रतिज्ञप्तिक कलन मिलता है। न्यूनतम तर्क या तो अभिगृहीत P4m जोड़कर या परिभाषित करके प्राप्त किया जाता है $\lnot \phi$ जैसा $\phi \to \bot$ है।

P4m. $\left(\phi \to \psi \right)\to \left(\left(\phi \to \lnot \psi \right)\to \lnot \phi \right)$

सकारात्मक निहितार्थ तर्क में अभिगृहीत P4i और P5i को जोड़कर, या न्यूनतम तर्क में अभिगृहीत P5i को जोड़कर अंतर्ज्ञानवादी तर्क प्राप्त किया जाता है। P4i और P5i दोनों चिरसम्मत प्रतिज्ञप्तिक कलन के प्रमेय हैं।

P4i. $\left(\phi \to \lnot \phi \right)\to \lnot \phi$

P5i. $\lnot \phi \to \left(\phi \to \psi \right)$

ध्यान दें कि ये अभिगृहीत स्कीमा हैं, जो अभिगृहीतों के असीम रूप से कई विशिष्ट उदाहरणों का प्रतिनिधित्व करती हैं। उदाहरण के लिए, P1 विशेष अभिगृहीत उदाहरण का प्रतिनिधित्व कर सकता है $p\to p$, या यह प्रतिनिधित्व कर सकता है $\left(p\to q\right)\to \left(p\to q\right)$: $\phi$ वह स्थान है जहाँ कोई भी सूत्र रखा जा सकता है। इस तरह के चर जो सूत्रों से अधिक होते हैं उन्हें 'योजनाबद्ध चर' कहा जाता है।

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

माना कि, $\phi (p)$ प्रस्तावात्मक चर के एक या अधिक उदाहरणों के साथ सूत्र बनें $p$, और जाने $\psi$ दूसरा सूत्र हो। फिर से $\phi (p)$, अनुमान $\phi (\psi )$हैं।

अगली तीन तार्किक अभिगृहीत स्कीमा सार्वभौम परिमाणकों को जोड़ने, परिचालन करने और हटाने के तरीके प्रदान करती हैं।

Q5. $\forall x\left(\phi \right)\to \phi [x:=t]$ जहां t को x के लिए $\,\!\phi$ प्रतिस्थापित किया जा सकता है

Q6. $\forall x\left(\phi \to \psi \right)\to \left(\forall x\left(\phi \right)\to \forall x\left(\psi \right)\right)$

Q7. $\phi \to \forall x\left(\phi \right)$ जहाँ x मुक्त नहीं है $\phi$.

ये तीन अतिरिक्त नियम चिरसम्मत विधेय तर्क को अभिगृहीत करने के लिए प्रस्ताव प्रणाली का विस्तार करते हैं। इसी तरह, ये तीन नियम अंतर्ज्ञानवादी साध्यात्मक तर्क (P1-3 और P4i और P5i के साथ) के लिए अंतर्ज्ञानवादी विधेय तर्क के लिए प्रणाली का विस्तार करते हैं।

सामान्यीकरण के अतिरिक्त नियम (मेटाथोरेम्स पर अनुभाग देखें) का उपयोग करते हुए सार्वभौमिक परिमाणीकरण को अधिकांशतः एक वैकल्पिक अभिगृहीतकरण दिया जाता है, इस प्रकरण में नियम Q6 और Q7 अनावश्यक हैं।

मानता प्रतीक वाले सूत्रों के साथ काम करने के लिए अंतिम अभिगृहीत स्कीमा की आवश्यकता होती है।

I8. $x=x$ प्रत्येक चर x के लिए।

I9. $\left(x=y\right)\to \left(\phi [z:=x]\to \phi [z:=y]\right)$

रूढ़िवादी विस्तार

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

अस्तित्वगत परिमाणीकरण

• परिचय

$\forall x(\phi \to \exists y(\phi [x:=y]))$

• उन्मूलन

$\forall x(\phi \to \psi )\to \exists x(\phi )\to \psi$ जहाँ $\psi$, $x$ का मुक्त चर नहीं है

संयोजन और वियोजन

• संयोजन परिचय और उन्मूलन

परिचय: $\alpha \to (\beta \to \alpha \land \beta )$

उन्मूलन बाकी: $\alpha \wedge \beta \to \alpha$

उन्मूलन अधिकार: $\alpha \wedge \beta \to \beta$

• वियोजन परिचय और उन्मूलन

परिचय: $\alpha \to \alpha \vee \beta$

परिचय सही: $\beta \to \alpha \vee \beta$

उन्मूलन: $(\alpha \to \gamma )\to ((\beta \to \gamma )\to \alpha \vee \beta \to \gamma )$

मेटाथोरेम्स

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

इस रूप के कुछ सामान्य रूपक हैं:

• निगमन प्रमेय: $\Gamma ;\phi \vdash \psi$ यदि और केवल यदि $\Gamma \vdash \phi \to \psi$.
• $\Gamma \vdash \phi \leftrightarrow \psi$ यदि और केवल यदि $\Gamma \vdash \phi \to \psi$ और $\Gamma \vdash \psi \to \phi$.
• विपर्यय : यदि $\Gamma ;\phi \vdash \psi$ तब $\Gamma ;\lnot \psi \vdash \lnot \phi$.
• सार्वव्यापकीकरण: यदि $\Gamma \vdash \phi$ और x के किसी भी सूत्र में मुक्त नहीं होता है $\Gamma$ तब $\Gamma \vdash \forall x\phi$.

कुछ उपयोगी प्रमेय और उनकी उपपत्तियाँ

प्रतिज्ञप्तिक कलन में निम्नलिखित कई प्रमेय उनके प्रमाणों के साथ (या अन्य लेखों में इन प्रमाणों के लिंक) हैं। ध्यान दें कि चूँकि (P1) स्वयं अन्य अभिगृहीतों का प्रयोग करके सिद्ध किया जा सकता है, वास्तव में (P2), (P3) और (P4) इन सभी प्रमेयों को सिद्ध करने के लिए पर्याप्त हैं।

(HS1) $(q\to r)\to ((p\to q)\to (p\to r))$ - काल्पनिक न्यायवाक्य, प्रमाण देखें।

(L1) $p\to ((p\to q)\to q)$ - प्रमाण:

(1) $((p\to q)\to (p\to q))\to (((p\to q)\to p)\to ((p\to q)\to q))$ (का उदाहरण (P3))

(2) $(p\to q)\to (p\to q)$ ((P1) का उदाहरण)

(3) $((p\to q)\to p)\to ((p\to q)\to q)$ (से (2) और (1)सरल तर्क द्वारा)

(4) $(((p\to q)\to p)\to ((p\to q)\to q))\to ((p\to ((p\to q)\to p))\to (p\to ((p\to q)\to q)))$ ((HS1) का उदाहरण)

(5) $(p\to ((p\to q)\to p))\to (p\to ((p\to q)\to q))$ (से (3) और (4) सरल तर्क द्वारा)

(6) $p\to ((p\to q)\to p)$ ((P2) का उदाहरण)

(7) $p\to ((p\to q)\to q)$ ((6) और (5) से सरल तर्क द्वारा)

निम्नलिखित दो प्रमेयों को एक साथ दोहरे निषेध के रूप में जाना जाता है:

(DN1)$\neg \neg p\to p$

(DN2) $p\to \neg \neg p$

प्रमाण देखें।

(L2) $(p\to (q\to r))\to (q\to (p\to r))$ - इस प्रमाण के लिए हम काल्पनिक न्यायवाक्य मेटाथोरम की विधि का उपयोग कई प्रमाण चरणों के लिए आशुलिपि के रूप में करते हैं:

(1) $(p\to (q\to r))\to ((p\to q)\to (p\to r))$ (का उदाहरण (P3))

(2) $((p\to q)\to (p\to r))\to ((q\to (p\to q))\to (q\to (p\to r)))$ ((HS1) का उदाहरण)

(3) $(p\to (q\to r))\to ((q\to (p\to q))\to (q\to (p\to r)))$ ((1) और (2) काल्पनिक न्यायवाक्य मेटाथोरम का प्रयोग करके)

(4) $((p\to (q\to r))\to ((q\to (p\to q))\to (q\to (p\to r))))\to (((p\to (q\to r))\to (q\to (p\to q)))\to ((p\to (q\to r))\to (q\to (p\to r))))$ (का उदाहरण (P3))

(5) $((p\to (q\to r))\to (q\to (p\to q)))\to ((p\to (q\to r))\to (q\to (p\to r)))$ ((3) और (4) सरल तर्क का उपयोग करके)

(6) $q\to (p\to q)$ ((P2) का उदाहरण)

(7) $(q\to (p\to q))\to ((p\to (q\to r))\to (q\to (p\to q)))$ ((P2) का उदाहरण)

(8) $(p\to (q\to r))\to (q\to (p\to q))$ ((6) और (7) से सरल तर्क का प्रयोग करके)

(9) $(p\to (q\to r))\to (q\to (p\to r))$ ((8) और (5) से सरल तर्क का उपयोग करके)

(HS2) $(p\to q)\to ((q\to r)\to (p\to r))$ - काल्पनिक न्यायवाक्य का वैकल्पिक रूप। प्रमाण:

(1) $(q\to r)\to ((p\to q)\to (p\to r))$ ((HS1) का उदाहरण)

(2) $((q\to r)\to ((p\to q)\to (p\to r)))\to ((p\to q)\to ((q\to r)\to (p\to r)))$ ((L2) का उदाहरण)

(3) $(p\to q)\to ((q\to r)\to (p\to r))$ ((1) और (2) से सरल तर्क द्वारा)

(TR1) $(p\to q)\to (\neg q\to \neg p)$ - व्युत्क्रमण, प्रमाण देखें (व्युत्क्रमण की दूसरी दिशा (P4) है)।

(TR2) $(\neg p\to q)\to (\neg q\to p)$ - व्युत्क्रमण का दूसरा रूप; प्रमाण:

(1) $(\neg p\to q)\to (\neg q\to \neg \neg p)$ ((TR1) का उदाहरण)

(2) $\neg \neg p\to p$ ((DN1) का उदाहरण)

(3) $(\neg \neg p\to p)\to ((\neg q\to \neg \neg p)\to (\neg q\to p))$ ((HS1) का उदाहरण)

(4) $(\neg q\to \neg \neg p)\to (\neg q\to p)$ ((2) और (3) सरल तर्क से)

(5) $(\neg p\to q)\to (\neg q\to p)$ ((1) और (4) काल्पनिक न्यायवाक्य मेटाथोरम का प्रयोग करके)

(L3) $(\neg p\to p)\to p$ - प्रमाण:

(1) $\neg p\to (\neg \neg (q\to q)\to \neg p)$ ((P2) का उदाहरण)

(2) $(\neg \neg (q\to q)\to \neg p)\to (p\to \neg (q\to q))$ ((P4) का उदाहरण)

(3) $\neg p\to (p\to \neg (q\to q))$ ((1) और (2) काल्पनिक न्यायवाक्य मेटाथोरम का प्रयोग करके)

(4) $(\neg p\to (p\to \neg (q\to q)))\to ((\neg p\to p)\to (\neg p\to \neg (q\to q)))$ (का उदाहरण (P3))

(5) $(\neg p\to p)\to (\neg p\to \neg (q\to q))$ (फॉर्म (3) और (4) सरल तर्क का उपयोग करके)

(6) $(\neg p\to \neg (q\to q))\to ((q\to q)\to p)$ ((P4) का उदाहरण)

(7) $(\neg p\to p)\to ((q\to q)\to p)$ ((5) और (6) काल्पनिक न्यायवाक्य मेटाथोरम का प्रयोग करके)

(8) $q\to q$ ((P1) का उदाहरण)

(9) $(q\to q)\to (((q\to q)\to p)\to p)$ ((L1) का उदाहरण)

(10) $((q\to q)\to p)\to p$ ((8) और (9) सरल तर्क का उपयोग करके)

(11) $(\neg p\to p)\to p$ ((7) और (10) काल्पनिक न्यायवाक्य मेटाथोरम का प्रयोग करके)

वैकल्पिक अभिगृहीतीकरण

Further information: तर्क प्रणालियों की सूची

उपरोक्त अभिगृहीत 3 इसका श्रेय जन लुकासिविक्ज़ को दिया जाता है। गॉटलॉब फ्रेगे की मूल प्रणाली में अभिगृहीत P2 और P3 थे लेकिन अभिगृहीत P4 के अतिरिक्त चार अन्य अभिगृहीत थे (देखें फ्रेगे का प्रस्तावपरक कलन)।, बर्ट्रेंड रसेल और अल्फ्रेड नॉर्थ व्हाइटहेड ने भी पांच प्रस्तावित सिद्धांतों के साथ एक प्रणाली का सुझाव दिया।

आगे के कनेक्शन

अभिगृहीत P1, P2 और P3, निगमनात्मक नियम सरल तर्क (औपचारिक रूप से अंतर्ज्ञानवादी प्रस्ताव तर्क) के साथ, अनुप्रयोग ऑपरेटर के साथ संयोजन तर्क बेस कॉम्बिनेटर I, K और S के अनुरूप हैं। हिल्बर्ट प्रणाली में प्रमाण तब संयोजी तर्क में संयोजी शब्दों के अनुरूप होते हैं। करी-हावर्ड पत्राचार भी देखें।

यह भी देखें

• हिल्बर्ट प्रणाली की सूची
• प्राकृतिक निगमन

संदर्भ

• Curry, Haskell B.; Robert Feys (1958). Combinatory Logic Vol. I. Vol. 1. Amsterdam: North Holland.
• Monk, J. Donald (1976). Mathematical Logic. Graduate Texts in Mathematics. Berlin, New York: Springer-Verlag. ISBN 978-0-387-90170-1.
• Ruzsa, Imre; Máté, András (1997). Bevezetés a modern logikába (in Hungarian). Budapest: Osiris Kiadó.{{cite book}}: CS1 maint: unrecognized language (link)
• Tarski, Alfred (1990). Bizonyítás és igazság (in Hungarian). Budapest: Gondolat.{{cite book}}: CS1 maint: unrecognized language (link) It is a Hungarian translation of Alfred Tarski's selected papers on semantic theory of truth.
• David Hilbert (1927) "The foundations of mathematics", translated by Stephan Bauer-Menglerberg and Dagfinn Føllesdal (pp. 464–479). in:
  • van Heijenoort, Jean (1967). From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931 (3rd printing 1976 ed.). Cambridge MA: Harvard University Press. ISBN 0-674-32449-8.
  • Hilbert's 1927, Based on an earlier 1925 "foundations" lecture (pp. 367–392), presents his 17 axioms -- axioms of implication #1-4, axioms about & and V #5-10, axioms of negation #11-12, his logical ε-axiom #13, axioms of equality #14-15, and axioms of number #16-17 -- along with the other necessary elements of his Formalist "proof theory" -- e.g. induction axioms, recursion axioms, etc; he also offers up a spirited defense against L.E.J. Brouwer's Intuitionism. Also see Hermann Weyl's (1927) comments and rebuttal (pp. 480–484), Paul Bernay's (1927) appendix to Hilbert's lecture (pp. 485–489) and Luitzen Egbertus Jan Brouwer's (1927) response (pp. 490–495)
• Kleene, Stephen Cole (1952). Introduction to Metamathematics (10th impression with 1971 corrections ed.). Amsterdam NY: North Holland Publishing Company. ISBN 0-7204-2103-9.
  • See in particular Chapter IV Formal System (pp. 69–85) wherein Kleene presents subchapters §16 Formal symbols, §17 Formation rules, §18 Free and bound variables (including substitution), §19 Transformation rules (e.g. modus ponens) -- and from these he presents 21 "postulates" -- 18 axioms and 3 "immediate-consequence" relations divided as follows: Postulates for the propostional calculus #1-8, Additional postulates for the predicate calculus #9-12, and Additional postulates for number theory #13-21.

बाहरी संबंध

• Gaifman, Haim. "A Hilbert Type Deductive System for Sentential Logic, Completeness and Compactness" (PDF).
• Farmer, W. M. "Propositional logic" (PDF). It describes (among others) a part of the Hilbert-style deduction system (restricted to propositional calculus).