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

गणितीय भौतिकी में, हिल्बर्ट प्रणाली 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$

पा. $\phi \to \left(\psi \to \phi \right)$

बेचना। $\left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)$

पी 4 $\left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)$ अभिगृहीत P1 बेमानी है, क्योंकि यह P3, P2 और विधानात्मक हेतुफलानुमान से आता है (देखें Propositional_calculus#Example_of_a_proof_in_a_classical_propositional_calculus_system)। ये स्वयंसिद्ध शास्त्रीय प्रस्तावात्मक तर्क का वर्णन करते हैं; अभिगृहीत P4 के बिना हमें इम्प्लीकेशनल साध्यात्मक कलन मिलता है। न्यूनतम तर्क या तो स्वयंसिद्ध P4m जोड़कर या परिभाषित करके प्राप्त किया जाता है $\lnot \phi$ जैसा $\phi \to \bot$.

पी4एम. $\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$

ठीक है। $\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 )$.

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

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

6 $\forall x\left(\phi \to \psi \right)\to \left(\forall x\left(\phi \right)\to \forall x\left(\psi \right)\right)$ 7 $\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$ कहाँ $x$ का मुक्त चर नहीं है $\psi$.

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

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

परिचय: $\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) इन सभी प्रमेयों को सिद्ध करने के लिए पर्याप्त हैं।

(एचएस1) $(q\to r)\to ((p\to q)\to (p\to r))$ - Hypothetical_syllogism#Alternative_form, Hypothetical_syllogism#Proof_2 देखें।

(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) से मॉडस पोनेंस द्वारा)

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

(डीएन1)$\neg \neg p\to p$

(डीएनए) $p\to \neg \neg p$

Double_negation#In_classical_propositional_calculus_system देखें।

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

(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) से मॉडस पोनेंस का उपयोग करके)

(एचएस2) $(p\to q)\to ((q\to r)\to (p\to r))$ - Hypothetical_syllogism#Alternative_form का एक वैकल्पिक रूप। सबूत:

(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) से मॉडस पोनेंस द्वारा)

(टीआर1) $(p\to q)\to (\neg q\to \neg p)$ - ट्रांसपोजिशन, ट्रांसपोजिशन_ (तर्क) # इन_क्लासिकल_प्रोपोजिशनल_कैलकुलस_सिस्टम देखें (ट्रांसपोजिशन की दूसरी दिशा (पी 4) है)।

(टीआर2) $(\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: List of logic systems

उपरोक्त स्वयंसिद्ध 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).