Q0 (mathematical logic)
क्यू0 पीटर एंड्रयूज द्वारा सरल-टाइप किए गए लैम्ब्डा कलन का सूत्रीकरण है, और प्रथम-क्रम तर्क और सेट सिद्धांत के साथ तुलनीय गणित के लिए एक आधार प्रदान करता है। यह उच्च-क्रम तर्क का एक रूप है और एचओएल प्रमेय कहावत परिवार के तर्क से निकटता से संबंधित है। सिद्धांत साबित करने वाली प्रणालियाँ टी. पी. एस. और ई. टी. पी. एस. क्यू0 पर आधारित हैं। अगस्त 2009 में, टी. पी. एस. ने उच्च-क्रम प्रमेय साबित करने वाली प्रणालियों के बीच पहली बार प्रतियोगिता जीती। इस प्रणाली में केवल पाँच स्वयंसिद्ध हैं, जिन्हें इस प्रकार कहा जा सकता हैः (स्वयंसिद्ध 2,3 और 4 स्वयंसिद्ध योजनाएँ हैं-समान स्वयंसिद्धों के परिवार। स्वयंसिद्ध 2 और स्वयंसिद्ध 3 के उदाहरण केवल चर और स्थिरांक के प्रकार से भिन्न होते हैं, लेकिन स्वयंसिद्ध 4 के उदाहरणों में ए और बी की जगह कोई भी अभिव्यक्ति हो सकती है।) अभिलिखित "ओ" बूलियन मूल्यों के लिए प्रकार प्रतीक है, और अभिलिखित "आई" व्यक्तिगत (गैर-बूलियन) मूल्यों के लिए प्रकार प्रतीक है। इनके अनुक्रम प्रकार के कार्यों का प्रतिनिधित्व करते हैं, और विभिन्न प्रकार के कार्यों को अलग करने के लिए कोष्ठक शामिल कर सकते हैं। अभिलिखित यूनानी अक्षर जैसे कि α और β प्रकार प्रतीकों के लिए वाक्य रचना चर हैं। बोल्ड कैपिटल अक्षर जैसे,, और डब्ल्यू. एफ. एफ. के लिए वाक्यात्मक चर हैं, और बोल्ड लोअर केस अक्षर जैसे, चर के लिए वाक्यात्मक चर हैं। सभी मुक्त घटनाओं पर वाक्यात्मक प्रतिस्थापन को इंगित करता है। केवल आदिम स्थिरांक हैं, जो प्रत्येक प्रकार α के सदस्यों की समानता को दर्शाते हैं, और, व्यक्तियों के लिए एक विवरण प्रचालक को दर्शाते हैं, एक समूह का अद्वितीय तत्व जिसमें बिल्कुल एक व्यक्ति होता है। प्रतीक λ और कोष्ठक ("[" और "]") भाषा के वाक्यविन्यास हैं। अन्य सभी प्रतीक इनमें शामिल शब्दों के लिए संक्षिप्त नाम हैं, जिनमें परिमापक τ और HE शामिल हैं। स्वयंसिद्ध 4 में, इन के लिए मुक्त होना चाहिए, जिसका अर्थ है कि प्रतिस्थापन के परिणामस्वरूप मुक्त चर की कोई भी घटना बाध्य नहीं होती है। स्वयंसिद्धियों के बारे में स्वयंसिद्ध 1 इस विचार को व्यक्त करता है कि और केवल बूलियन मूल्य हैं। स्वयंसिद्ध योजना 2α और 3αβ कार्यों के मौलिक गुणों को व्यक्त करते हैं। स्वयंसिद्ध योजना 4 λ संकेतन की प्रकृति को परिभाषित करती है। स्वयंसिद्ध 5 का कहना है कि चयन प्रचालक व्यक्तियों पर समानता फलन का व्युत्क्रम है। (एक तर्क को देखते हुए, उस व्यक्ति को व्यक्ति वाले सेट/विधेय के साथ मैप करें। क्यू0 में, के लिए एक संक्षिप्त नाम है, जो के लिए एक संक्षिप्त नाम है)। इस प्रचालक को निश्चित विवरण प्रचालक के रूप में भी जाना जाता है। में, स्वयंसिद्ध 4 को पाँच उपभागों में विकसित किया गया है जो प्रतिस्थापन की प्रक्रिया को तोड़ते हैं। जैसा कि यहाँ दिया गया है, स्वयंसिद्ध को एक विकल्प के रूप में चर्चा की गई है और उपभागों से साबित किया गया है। लॉजिकल कोर एंड्रयूज के विस्तार सभी प्रकार के संग्रहों के लिए चयन प्रचालक की परिभाषाओं के साथ इस तर्क का विस्तार करते हैं, ताकि एक प्रमेय (संख्या 5309) हो। दूसरे शब्दों में, सभी प्रकारों का एक निश्चित विवरण प्रचालक होता है। यह एक रूढ़िवादी विस्तार है, इसलिए विस्तारित प्रणाली सुसंगत है यदि कोर सुसंगत है। वह एक अतिरिक्त स्वयंसिद्ध 6 भी प्रस्तुत करते हैं, जिसमें कहा गया है कि अनंत के समकक्ष वैकल्पिक स्वयंसिद्धियों के साथ अनंत रूप से कई व्यक्ति हैं। प्रकार सिद्धांत पर आधारित प्रकार सिद्धांत और प्रमाण सहायकों के कई अन्य सूत्रीकरणों के विपरीत, क्यू0 ओ और आई के अलावा अन्य आधार प्रकारों के लिए प्रदान नहीं करता है, इसलिए उदाहरण के लिए परिमित कार्डिनल संख्याओं का निर्माण सरल प्रकार सिद्धांत के अर्थ में एक प्रकार के बजाय सामान्य पीनो अभिधारणाओं का पालन करने वाले व्यक्तियों के संग्रह के रूप में किया जाता है। क्यू0 क्यू0 में अनुमान का एक ही नियम है। नियम आर. इन की एक घटना को एक घटना द्वारा प्रतिस्थापित करने के परिणाम से और उसका अनुमान लगाने के लिए, बशर्ते कि इन की घटना तुरंत पहले (एक चर की घटना) न हो। अनुमान R′ का व्युत्पन्न नियम परिकल्पनाओं के एक समूह H. नियम R′ से तर्क को सक्षम बनाता है। यदि, और, और की एक घटना को एक घटना द्वारा प्रतिस्थापित करके प्राप्त किया जाता है, तो, बशर्ते किः इन की घटना तुरंत पहले एक चर की घटना नहीं है, और कोई भी चर मुक्त नहीं है और एक सदस्य की प्रतिस्थापित घटना पर बाध्य है। नोटः इन द्वारा प्रतिस्थापन पर प्रतिबंध यह सुनिश्चित करता है कि कोई भी चर दोनों परिकल्पनाओं में मुक्त है और प्रतिस्थापन के बाद दोनों में समान मूल्य रखने के लिए विवश है। क्यू0 के लिए कटौती प्रमेय से पता चलता है कि नियम आर′ का उपयोग करके परिकल्पनाओं के प्रमाणों को परिकल्पनाओं के बिना और नियम आर का उपयोग करके प्रमाणों में परिवर्तित किया जा सकता है। कुछ समान प्रणालियों के विपरीत, क्यू0 में अनुमान एक समान अभिव्यक्ति के साथ डब्ल्यू. एफ. एफ. के भीतर किसी भी गहराई पर एक उप-अभिव्यक्ति को प्रतिस्थापित करता है। तो उदाहरण के लिए दिए गए स्वयंसिद्धः 1. 2. और तथ्य यह है कि, हम परिमापक को हटाए बिना आगे बढ़ सकते हैंः 3. ए और बी 4 के लिए तत्काल. नियम आर पंक्ति 3 का उपयोग करके पंक्ति 1 में प्रतिस्थापित। अधिक गहराई में क्यू0 का एक विवरण; स्टैनफोर्ड एनसाइक्लोपीडिया ऑफ फिलॉसफी में चर्च के प्रकार सिद्धांत पर एक लेख का हिस्सा। गणितीय तर्कशास्त्र पर एक अवलोकन (क्यू0 के विभिन्न उत्तराधिकारियों सहित): गणित की नींव। वंशावली और अवलोकन दोईः 10.4444/100.111। कंप्यूटर विज्ञान में तर्क