Geometric logic
गणितीय तर्क में, ज्यामितीय तर्क सुसंगत तर्क का एक अनंत सामान्यीकरण है, जो स्कोलेम के कारण प्रथम-क्रम तर्क का एक प्रतिबंध है जो प्रमाण-सैद्धांतिक रूप से ट्रैक्टेबल है। ज्यामितीय तर्क कई गणितीय सिद्धांतों को व्यक्त करने में सक्षम है और इसका टोपोस सिद्धांत के साथ घनिष्ठ संबंध है। परिभाषा प्रथम-क्रम तर्क का एक सिद्धांत ज्यामितीय है यदि इसे केवल उस रूप के स्वयंसिद्धों का उपयोग करके स्वयंसिद्ध किया जा सकता है जहां I और J सूत्र सूचकांकों के असंबद्ध संग्रह हैं कि प्रत्येक अनंत हो सकता है और सूत्र φ या तो परमाणु हैं या परमाणुओं के निषेध हैं। यदि सभी स्वयंसिद्ध परिमित हैं (अर्थात, प्रत्येक स्वयंसिद्ध के लिए, I और J दोनों सीमित हैं), तो सिद्धांत सुसंगत है। प्रमेय प्रत्येक प्रथम-क्रम सिद्धांत का एक सुसंगत रूढ़िवादी विस्तार होता है। महत्व सूची में उपरोक्त प्रमेय के आठ परिणाम हैं जो इसके महत्व की व्याख्या करते हैं (फुटनोट्स और अधिकांश संदर्भों को छोड़कर): जी3सी जैसे क्रमिक कलन के संदर्भ में, स्वयंसिद्ध के रूप में विशेष सुसंगत निहितार्थ को संरचनात्मक नियमों (कमजोरी, संकुचन और कटौती) की स्वीकार्यता को प्रभावित किए बिना सीधे अनुमान नियमों में परिवर्तित किया जा सकता है; इसी तरह के शब्दों में, सुसंगत सिद्धांत "एक निश्चित सरल रूप में प्राकृतिक कटौती नियमों द्वारा व्यक्त किए जाने वाले सिद्धांत हैं जिसमें केवल परमाणु सूत्र एक महत्वपूर्ण भूमिका निभाते हैं"; सुसंगत निहितार्थ अनुक्रम बनाते हैं जो एक ग्लिवेंको वर्ग देते हैं। इस मामले में, परिणाम, जिसे प्रथम-क्रम बार के प्रमेय के रूप में जाना जाता है, बताता है कि यदि प्रत्येक Ii: 0 ≤ i ≤ n एक सुसंगत निहितार्थ है और अनुक्रमिक I1, है। .. .. , में I0 शास्त्रीय रूप से सिद्ध करने योग्य है तो यह अंतर्ज्ञानी रूप से सिद्ध करने योग्य है; सुसंगत/ज्यामितीय सिद्धांतों के कई उदाहरण हैंः सभी बीजगणितीय सिद्धांत, जैसे कि समूह सिद्धांत और रिंग सिद्धांत, सभी अनिवार्य रूप से बीजगणितीय सिद्धांत, जैसे कि श्रेणी सिद्धांत, क्षेत्रों का सिद्धांत, स्थानीय रिंगों का सिद्धांत, जाली सिद्धांत, प्रोजेक्टिव ज्यामिति, अलग-अलग बंद स्थानीय रिंगों का सिद्धांत (उर्फ "सख्ती से हेन्सेलियन स्थानीय रिंग") और मरोड़ एबेलियन समूहों का अनंत सिद्धांत; सुसंगत/ज्यामितीय सिद्धांतों को टोपोई (मैक्लेन और मोर्डिक 1992, अध्याय X) के बीच ज्यामितीय रूपात्मकता के साथ पुलबैक द्वारा संरक्षित किया जाता है। सी डी तर्क प्रोग्रामिंग से हॉर्न खंडों को सामान्यीकृत करता है, जहां डी को एक परमाणु होने की आवश्यकता होती है; वास्तव में, वे विखंडनीय तर्क कार्यक्रमों के "खंडों" को सामान्यीकृत करते हैं, जहां डी को परमाणुओं का विच्छेदन होने की अनुमति है। सुसंगत सिद्धांतों के लिए प्रभावी प्रमेय-प्रमाण, (संकल्प के संबंध में) सापेक्ष आसानी और स्पष्टता के साथ, स्वचालित हो सकता है। जैसा कि बेज़ेम और अन्य लोगों ने उल्लेख किया है कि स्कोलेमाइजेशन (नए कार्य प्रतीकों की शुरुआत) की अनुपस्थिति कोई वास्तविक कठिनाई नहीं है, और क्लॉज़ल रूप में गैर-रूपांतरण सामान्य गणितीय तर्कों की संरचना को बेहतर बनाए रखने की अनुमति देता है। नोट्स बिब्लियोग्राफी (दो खंड, ऑक्सफोर्ड लॉजिक गाइड 43 और 44, तैयारी में तीसरा खंड) आगे पढ़ने के लिए ज्यामिति लॉजिक