प्रथम-क्रम तर्क

प्रथम-क्रम तर्क - जिसे विधेय तर्क, मात्रात्मक तर्क और प्रथम-क्रम विधेय कलन के रूप में भी जाना जाता है - गणित, दर्शन, भाषा विज्ञान और कंप्यूटर विज्ञान में उपयोग की जाने वाली औपचारिक प्रणालियों का एक संग्रह है। प्रथम-क्रम तर्क गैर-तार्किक वस्तुओं पर परिमाणीकरण (तर्क) का उपयोग करता है, और उन वाक्यों के उपयोग की अनुमति देता है जिनमें चर होते हैं, ताकि सुकरात एक आदमी है जैसे प्रस्तावों के बजाय, किसी के पास एक्स के रूप में अभिव्यक्ति हो सकती है जैसे कि एक्स सुकरात है और x एक आदमी है, जहां मौजूद है एक परिमाणक है, जबकि x एक चर है।^[1] यह इसे प्रस्तावात्मक तर्क से अलग करता है, जो क्वांटिफायर या अंतिम संबंधों का उपयोग नहीं करता है;^[2] इस अर्थ में, प्रस्तावात्मक तर्क प्रथम-क्रम तर्क की नींव है।

किसी विषय के बारे में एक सिद्धांत, जैसे सेट सिद्धांत, समूहों के लिए एक सिद्धांत,^[3] या अंकगणित का एक औपचारिक सिद्धांत, आम तौर पर प्रवचन के एक निर्दिष्ट डोमेन (जिस पर मात्रात्मक चर सीमा होती है) के साथ एक प्रथम-क्रम तर्क होता है, उस डोमेन से स्वयं तक सीमित रूप से कई फ़ंक्शन, उस डोमेन पर परिभाषित कई परिमित विधेय (गणितीय तर्क) , और उनके बारे में सिद्धांतों का एक समूह माना जाता है। सिद्धांत को कभी-कभी अधिक औपचारिक अर्थ में प्रथम-क्रम तर्क में वाक्यों के एक सेट के रूप में समझा जाता है।

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

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

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

प्रथम-क्रम तर्क की नींव भगवान का शुक्र है फ्रीज और चार्ल्स सैंडर्स पीयर्स द्वारा स्वतंत्र रूप से विकसित की गई थी।^[5] प्रथम-क्रम तर्क के इतिहास और यह औपचारिक तर्क पर कैसे हावी हुआ, इसके लिए जोस फेरेइरोस (2001) देखें।

परिचय

जबकि प्रस्तावात्मक तर्क सरल घोषणात्मक प्रस्तावों से संबंधित है, प्रथम-क्रम तर्क अतिरिक्त रूप से Predicate_(mathematical_logic)s और परिमाणीकरण (तर्क) को भी कवर करता है।

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

क्वांटिफ़ायर को किसी सूत्र में चर पर लागू किया जा सकता है। पिछले सूत्र में चर x को सार्वभौमिक रूप से परिमाणित किया जा सकता है, उदाहरण के लिए, प्रत्येक x के लिए प्रथम-क्रम वाक्य के साथ, यदि x एक दार्शनिक है, तो x एक विद्वान है। इस वाक्य में प्रत्येक के लिए सार्वभौमिक परिमाणक इस विचार को व्यक्त करता है कि यदि x एक दार्शनिक है, तो x एक विद्वान है, यह दावा x के सभी विकल्पों के लिए मान्य है।

प्रत्येक x के लिए वाक्य का निषेध, यदि x एक दार्शनिक है, तो x एक विद्वान है, तार्किक रूप से इस वाक्य के समतुल्य है कि x का अस्तित्व इस प्रकार है कि x एक दार्शनिक है और x एक विद्वान नहीं है। वहां मौजूद अस्तित्व संबंधी परिमाणक इस विचार को व्यक्त करता है कि दावा x एक दार्शनिक है और x एक विद्वान नहीं है जो x के कुछ विकल्प के लिए है।

विधेय एक दार्शनिक है और एक विद्वान है, प्रत्येक एक एकल चर लेता है। सामान्य तौर पर, विधेय कई चर ले सकते हैं। पहले क्रम के वाक्य में सुकरात प्लेटो का शिक्षक है, विधेय दो चर लेता है।

प्रथम-क्रम सूत्र की व्याख्या (या मॉडल) निर्दिष्ट करती है कि प्रत्येक विधेय का क्या अर्थ है, और वे इकाइयाँ जो चर को त्वरित कर सकती हैं। ये संस्थाएँ प्रवचन या ब्रह्मांड का क्षेत्र बनाती हैं, जिसके लिए आमतौर पर एक गैर-रिक्त सेट होना आवश्यक होता है। उदाहरण के लिए, सभी मनुष्यों से युक्त प्रवचन के क्षेत्र के साथ एक व्याख्या में और विधेय एक दार्शनिक है जिसे गणतंत्र (प्लेटो) के लेखक के रूप में समझा जाता है, वाक्य वहाँ x मौजूद है जैसे कि x एक दार्शनिक है जिसे सत्य के रूप में देखा जाता है , जैसा कि प्लेटो ने देखा था।^{[clarification needed]}

प्रथम-क्रम तर्क के दो प्रमुख भाग हैं। वाक्यविन्यास यह निर्धारित करता है कि प्रतीकों का कौन सा परिमित क्रम प्रथम-क्रम तर्क में अच्छी तरह से गठित अभिव्यक्ति है, जबकि शब्दार्थ इन अभिव्यक्तियों के पीछे के अर्थ को निर्धारित करता है।

वाक्यविन्यास

वर्णमाला

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

वर्णमाला के प्रतीकों को तार्किक प्रतीकों में विभाजित करना आम बात है, जिनका हमेशा एक ही अर्थ होता है, और गैर-तार्किक प्रतीकों में, जिनका अर्थ व्याख्या के अनुसार बदलता रहता है।^{[citation needed]} उदाहरण के लिए, तार्किक प्रतीक $\land$ हमेशा प्रतिनिधित्व करता है तथा ; इसकी कभी भी या के रूप में व्याख्या नहीं की जाती है, जिसे तार्किक प्रतीक द्वारा दर्शाया जाता है $\lor$ . हालाँकि, एक गैर-तार्किक विधेय प्रतीक जैसे कि फिल (x) की व्याख्या इस अर्थ में की जा सकती है कि x एक दार्शनिक है, x फिलिप नाम का एक व्यक्ति है, या हाथ में व्याख्या के आधार पर कोई अन्य एकात्मक विधेय है।

तार्किक प्रतीक

तार्किक प्रतीक वर्णों का एक समूह है जो लेखक के अनुसार अलग-अलग होता है, लेकिन आमतौर पर इसमें निम्नलिखित शामिल होते हैं:^[7]

परिमाणक (तर्क)तर्क) प्रतीक: $\forall$ सार्वभौमिक परिमाणीकरण के लिए, और $\exists$ अस्तित्वगत परिमाणीकरण के लिए
तार्किक संयोजक: $\land$ तार्किक संयोजन के लिए, $\lor$ विच्छेद के लिए, $\to$ सामग्री सशर्त के लिए, $\leftrightarrow$ तार्किक द्विशर्तीय के लिए, $\neg$ निषेध के लिए. कुछ लेखक^[8] इसके स्थान पर Cpq का उपयोग करें $\to$ और Epq के बजाय $\leftrightarrow$ , विशेष रूप से उन संदर्भों में जहां → का उपयोग अन्य उद्देश्यों के लिए किया जाता है। इसके अलावा, घोड़े की नाल $\supset$ प्रतिस्थापित कर सकता है $\to$ ; ट्रिपल-बार $\equiv$ प्रतिस्थापित कर सकता है $\leftrightarrow$ ; टिल्ड ( $~$ ), एनपी, या एफपी प्रतिस्थापित कर सकता है $\neg$ ; एक डबल बार $\|$ , $+$ , $\bigwedge pq$ ,^[9] या एपीक्यू प्रतिस्थापित कर सकता है $\lor$ ; और एक एम्परसेंड $&$ , Kpq, या मध्य बिंदु $\cdot$ प्रतिस्थापित कर सकता है $\land$ , विशेषकर यदि ये प्रतीक तकनीकी कारणों से उपलब्ध नहीं हैं। (उपरोक्त प्रतीक Cpq, Epq, Np, Apq, और Kpq पोलिश संकेतन में उपयोग किए जाते हैं।)
कोष्ठक, कोष्ठक और अन्य विराम चिह्न। ऐसे प्रतीकों का चुनाव संदर्भ के आधार पर भिन्न-भिन्न होता है।
चरों का एक अनंत सेट, जिसे अक्सर वर्णमाला x, y, z, ... के अंत में छोटे अक्षरों द्वारा दर्शाया जाता है। सबस्क्रिप्ट का उपयोग अक्सर वेरिएबल को अलग करने के लिए किया जाता है: $x 0, x 1, x 2, ... .$
एक समानता प्रतीक (कभी-कभी, पहचान प्रतीक) $=$ (देखना § Equality and its axioms नीचे)।

प्रथम-क्रम तर्क में इन सभी प्रतीकों की आवश्यकता नहीं है। निषेध, संयोजन (या वियोजन), चर, कोष्ठक और समानता के साथ कोई भी परिमाणक पर्याप्त है।

अन्य तार्किक प्रतीकों में निम्नलिखित शामिल हैं:

सत्य स्थिरांक: टी, वी, या $⊤$ सत्य और एफ, ओ, या के लिए $⊥$ असत्य के लिए (V और O पोलिश संकेतन से हैं)। वैलेंस 0 के ऐसे किसी भी तार्किक ऑपरेटर के बिना, इन दो स्थिरांकों को केवल क्वांटिफायर का उपयोग करके व्यक्त किया जा सकता है।
अतिरिक्त तार्किक संयोजक जैसे शेफ़र लाइन, डीपीक्यू (एनएएनडी), और एकमात्र, जेपीक्यू।

गैर-तार्किक प्रतीक

गैर-तार्किक प्रतीक विधेय (संबंध), फ़ंक्शन और स्थिरांक का प्रतिनिधित्व करते हैं। सभी उद्देश्यों के लिए गैर-तार्किक प्रतीकों के एक निश्चित, अनंत सेट का उपयोग करना मानक अभ्यास हुआ करता था:

प्रत्येक पूर्णांक n ≥ 0 के लिए, arity|n-ary, या n-स्थान, विधेय प्रतीकों का एक संग्रह होता है। चूँकि वे n तत्वों के बीच परिमित संबंध का प्रतिनिधित्व करते हैं, इसलिए उन्हें संबंध प्रतीक भी कहा जाता है। प्रत्येक arity n के लिए, उनकी अनंत आपूर्ति है:
पीⁿ₀, पीⁿ₁, पीⁿ₂, पीⁿ₃, ...
प्रत्येक पूर्णांक n ≥ 0 के लिए, अनंत रूप से कई n-ary फ़ंक्शन प्रतीक हैं:
एफⁿ₀, एफⁿ₁, एफⁿ₂, एफⁿ₃, ...

जब किसी विधेय प्रतीक या फ़ंक्शन प्रतीक की योग्यता संदर्भ से स्पष्ट होती है, तो सुपरस्क्रिप्ट n को अक्सर छोड़ दिया जाता है।

इस पारंपरिक दृष्टिकोण में, प्रथम-क्रम तर्क की केवल एक ही भाषा है।^[10] यह दृष्टिकोण अभी भी आम है, विशेषकर दार्शनिक रूप से उन्मुख पुस्तकों में।

एक हालिया अभ्यास यह है कि किसी व्यक्ति के मन में जो अनुप्रयोग होता है उसके अनुसार विभिन्न गैर-तार्किक प्रतीकों का उपयोग किया जाता है। इसलिए, किसी विशेष एप्लिकेशन में उपयोग किए जाने वाले सभी गैर-तार्किक प्रतीकों के सेट को नाम देना आवश्यक हो गया है। यह चुनाव एक हस्ताक्षर (तर्क) के माध्यम से किया जाता है।^[11] गणित में विशिष्ट हस्ताक्षर समूह (गणित) के लिए {1, ×} या सिर्फ {×} हैं,^[3]या ऑर्डर किए गए फ़ील्ड के लिए {0, 1, +, ×, <}। गैर-तार्किक प्रतीकों की संख्या पर कोई प्रतिबंध नहीं है। हस्ताक्षर खाली सेट, परिमित या अनंत, यहां तक कि बेशुमार भी हो सकते हैं। उदाहरण के लिए, लोवेनहेम-स्कोलेम प्रमेय के आधुनिक प्रमाणों में अनगिनत हस्ताक्षर पाए जाते हैं।

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

इस दृष्टिकोण में, प्रत्येक गैर-तार्किक प्रतीक निम्नलिखित प्रकारों में से एक होता है:

एक विधेय प्रतीक (या संबंध प्रतीक) जिसकी कुछ संयोजकता (या तर्कों की संख्या) 0 से अधिक या उसके बराबर है। इन्हें अक्सर बड़े अक्षरों जैसे पी, क्यू और आर द्वारा दर्शाया जाता है। उदाहरण:
- P(x) में, P संयोजकता 1 का एक विधेय प्रतीक है। एक संभावित व्याख्या यह है कि x एक आदमी है।
- Q(x,y) में, Q संयोजकता 2 का एक विधेय प्रतीक है। संभावित व्याख्याओं में शामिल है कि x, y से बड़ा है और x, y का पिता है।
- वैलेंस 0 के संबंधों को प्रस्तावात्मक चर के साथ पहचाना जा सकता है, जो किसी भी कथन के लिए खड़ा हो सकता है। आर की एक संभावित व्याख्या यह है कि सुकरात एक आदमी है।
एक फ़ंक्शन प्रतीक, जिसकी कुछ संयोजकता 0 से अधिक या उसके बराबर होती है। इन्हें अक्सर लोअरकेस लैटिन लिपि जैसे f, g और h द्वारा दर्शाया जाता है। उदाहरण:
- f(x) की व्याख्या x के पिता के रूप में की जा सकती है। अंकगणित में, इसका मतलब -x हो सकता है। सेट सिद्धांत में, यह x के सत्ता स्थापित के लिए खड़ा हो सकता है।
- अंकगणित में, g(x,y) का अर्थ x+y हो सकता है। सेट सिद्धांत में, यह x और y के मिलन का प्रतीक हो सकता है।
- वैलेंस 0 के फ़ंक्शन प्रतीकों को स्थिर प्रतीक कहा जाता है, और अक्सर वर्णमाला की शुरुआत में छोटे अक्षरों जैसे ए, बी और सी द्वारा दर्शाया जाता है। प्रतीक 'ए' का अर्थ सुकरात हो सकता है। अंकगणित में, यह 0 के लिए खड़ा हो सकता है। सेट सिद्धांत में, यह खाली सेट के लिए खड़ा हो सकता है।

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

निर्माण नियम

BNF grammar

<index>             ::= "" 
                      | <index> "'"
<variable>          ::= "x" <index>
<constant>          ::= "c" <index>
<unary function>    ::= "f1" <index>
<binary function>   ::= "f2" <index>
<ternary function>  ::= "f3" <index>
<unary predicate>   ::= "p1" <index>
<binary predicate>  ::= "p2" <index>
<ternary predicate> ::= "p3" <index>
<term>              ::= <variable> 
                      | <constant> 
                      | <unary function> "(" <term> ")" 
                      | <binary function> "(" <term> "," <term> ")" 
                      | <ternary function> "(" <term> "," <term> "," <term> ")"
<atomic formula>    ::= "TRUE" 
                      | "FALSE"
                      | <term> "=" <term>
                      | <unary predicate> "(" <term> ")" 
                      | <binary predicate> "(" <term> "," <term> ")" 
                      | <ternary predicate> "(" <term> "," <term> "," <term> ")"
<formula>           ::= <atomic formula> 
                      | "¬" <formula>
                      | <formula> "∧" <formula>
                      | <formula> "∨" <formula>
                      | <formula> "⇒" <formula>
                      | <formula> "⇔" <formula>
                      | "(" <formula> ")"
                      | "∀" <variable> <formula>
                      | "∃" <variable> <formula>

The above context-free grammar in Backus-Naur form defines the language of syntactically valid first-order formulas with function symbols and predicate symbols up to arity 3. For higher arities, it needs to be adapted accordingly.^[12]^{[citation needed]}

The example formula ∀x ∃x' (¬x=c) ⇒ f2(x,x')=c' describes multiplicative inverses when f2', c, and c' are interpreted as multiplication, zero, and one, respectively.

गठन नियम प्रथम-क्रम तर्क के नियमों और सूत्रों को परिभाषित करते हैं।^[13] जब शब्दों और सूत्रों को प्रतीकों की श्रृंखला के रूप में दर्शाया जाता है, तो इन नियमों का उपयोग शब्दों और सूत्रों के लिए औपचारिक व्याकरण लिखने के लिए किया जा सकता है। ये नियम आम तौर पर संदर्भ-मुक्त व्याकरण हैं|संदर्भ-मुक्त (प्रत्येक उत्पादन में बाईं ओर एक ही प्रतीक होता है), सिवाय इसके कि प्रतीकों के सेट को अनंत होने की अनुमति दी जा सकती है और कई प्रारंभ प्रतीक हो सकते हैं, उदाहरण के लिए चर #शर्तों का मामला.

शर्तें

टर्म (तर्क) का सेट निम्नलिखित नियमों द्वारा आगमनात्मक परिभाषा है:^[14]

चर। कोई भी परिवर्तनशील प्रतीक एक पद है।
कार्य. यदि f एक n-ary फ़ंक्शन प्रतीक है, और t₁, ..., टी_n पद हैं, तो f(t₁,...,टी_n) एक शब्द है. विशेष रूप से, व्यक्तिगत स्थिरांक को दर्शाने वाले प्रतीक अशक्त कार्य प्रतीक हैं, और इस प्रकार पद हैं।

केवल वे अभिव्यक्तियाँ जो नियम 1 और 2 के बहुत से अनुप्रयोगों द्वारा प्राप्त की जा सकती हैं, पद हैं। उदाहरण के लिए, विधेय चिह्न से युक्त कोई भी अभिव्यक्ति शब्द नहीं है।

सूत्र

सूत्र का सेट (गणितीय तर्क) (जिसे अच्छी तरह से गठित सूत्र भी कहा जाता है | अच्छी तरह से गठित सूत्र^[15] या WFFs) को निम्नलिखित नियमों द्वारा आगमनात्मक रूप से परिभाषित किया गया है:

विधेय चिह्न. यदि P एक n-ary विधेय प्रतीक है और t₁, ..., टी_n पद हैं तो P(t₁,...,टी_n) एक सूत्र है.
तार्किक समानता. यदि समानता प्रतीक को तर्क का हिस्सा माना जाता है, और टी₁ और टी₂ पद हैं, तो t₁ = टी₂ एक सूत्र है.
निषेध. अगर $\varphi$ तो फिर यह एक सूत्र है $\lnot \varphi$ एक सूत्र है.
बाइनरी संयोजक। अगर $\varphi$ और $\psi$ सूत्र हैं, तो ( $\varphi \rightarrow \psi$ ) एक सूत्र है. इसी तरह के नियम अन्य बाइनरी तार्किक संयोजकों पर भी लागू होते हैं।
परिमाणक. अगर $\varphi$ तो फिर, एक सूत्र है और x एक चर है $\forall x\varphi$ (सभी एक्स के लिए, $\varphi$ धारण करता है) और $\exists x\varphi$ (वहाँ x ऐसा मौजूद है $\varphi$ ) सूत्र हैं.

केवल वे अभिव्यक्तियाँ जो नियम 1-5 के सीमित रूप से कई अनुप्रयोगों द्वारा प्राप्त की जा सकती हैं, सूत्र हैं। प्रथम दो नियमों से प्राप्त सूत्र परमाणु सूत्र कहलाते हैं।

उदाहरण के लिए,

\forall x\forall y(P(f(x))\rightarrow \neg (P(x)\rightarrow Q(f(y),x,z)))

एक सूत्र है, यदि f एक यूनरी फ़ंक्शन प्रतीक है, P एक यूनरी विधेय प्रतीक है, और Q एक टर्नरी विधेय प्रतीक है। हालाँकि, $\forall x\,x\rightarrow$ यह कोई सूत्र नहीं है, हालाँकि यह वर्णमाला के प्रतीकों की एक श्रृंखला है।

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

सूत्र की यह परिभाषा यदि-तब-अन्यथा फ़ंक्शन को परिभाषित करने का समर्थन नहीं करती है ite(c, a, b), जहां c एक सूत्र के रूप में व्यक्त की गई शर्त है, यदि c सत्य है तो a लौटाएगा, और यदि गलत है तो b लौटाएगा। ऐसा इसलिए है क्योंकि विधेय और फ़ंक्शन दोनों केवल शब्दों को पैरामीटर के रूप में स्वीकार कर सकते हैं, लेकिन पहला पैरामीटर एक सूत्र है। प्रथम-क्रम तर्क पर बनी कुछ भाषाएँ, जैसे SMT-LIB 2.0, इसे जोड़ती हैं।^[16]

नोटेशनल कन्वेंशन

सुविधा के लिए, कुछ मामलों में कोष्ठक लिखने की आवश्यकता से बचने के लिए, तार्किक ऑपरेटरों की प्राथमिकता के बारे में परंपराएँ विकसित की गई हैं। ये नियम अंकगणित में संक्रियाओं के क्रम के समान हैं। एक सामान्य सम्मेलन है:

$\lnot$ पहले मूल्यांकन किया जाता है
$\land$ और $\lor$ अगले का मूल्यांकन किया जाता है
क्वांटिफायर का मूल्यांकन आगे किया जाता है
$\to$ अंतिम मूल्यांकन किया जाता है।

इसके अलावा, सूत्रों को पढ़ने में आसान बनाने के लिए परिभाषा के लिए आवश्यक अतिरिक्त विराम चिह्न भी शामिल किया जा सकता है। इस प्रकार सूत्र

\lnot \forall xP(x)\to \exists x\lnot P(x)

के रूप में लिखा जा सकता है

(\lnot [\forall xP(x)])\to \exists x[\lnot P(x)].

कुछ क्षेत्रों में, ऊपर परिभाषित उपसर्ग नोटेशन के बजाय, बाइनरी संबंधों और कार्यों के लिए इनफ़िक्स नोटेशन का उपयोग करना आम है। उदाहरण के लिए, अंकगणित में, आमतौर पर कोई =(+(2,2),4) के बजाय 2 + 2 = 4 लिखता है। इनफ़िक्स नोटेशन में सूत्रों को उपसर्ग नोटेशन, सीएफ में संबंधित सूत्रों के संक्षिप्त रूप के रूप में मानना आम बात है। टर्म (तर्क)#शब्द संरचना बनाम प्रतिनिधित्व|शब्द संरचना बनाम प्रतिनिधित्व भी।

उपरोक्त परिभाषाएँ बाइनरी संयोजकों के लिए इन्फ़िक्स नोटेशन का उपयोग करती हैं जैसे कि $\to$ . एक कम आम परंपरा पोलिश संकेतन है, जिसमें कोई लिखता है $\rightarrow$ , $\wedge$ और इसी तरह उनके बीच के बजाय उनके तर्कों के सामने। यह परिपाटी इस दृष्टि से लाभप्रद है कि यह सभी विराम चिन्हों को त्यागने की अनुमति देती है। वैसे तो, पोलिश नोटेशन कॉम्पैक्ट और सुरुचिपूर्ण है, लेकिन व्यवहार में इसका उपयोग शायद ही कभी किया जाता है क्योंकि इसे पढ़ना मनुष्यों के लिए कठिन है। पोलिश संकेतन में, सूत्र

\forall x\forall y(P(f(x))\rightarrow \neg (P(x)\rightarrow Q(f(y),x,z)))

बन जाता है "∀x∀y→Pfx¬→ PxQfyxz".

मुक्त और बाध्य चर

किसी सूत्र में, एक चर मुक्त या बाध्य (या दोनों) हो सकता है। इस धारणा का एक औपचारिकीकरण क्विन के कारण होता है, पहले एक परिवर्तनीय घटना की अवधारणा को परिभाषित किया जाता है, फिर क्या एक परिवर्तनीय घटना स्वतंत्र या बाध्य है, फिर क्या एक चर प्रतीक समग्र रूप से मुक्त या बाध्य है। समान प्रतीक x की विभिन्न घटनाओं को अलग करने के लिए, सूत्र φ में एक चर प्रतीक x की प्रत्येक घटना को φ के प्रारंभिक उपस्ट्रिंग के साथ उस बिंदु तक पहचाना जाता है जिस पर प्रतीक x का उदाहरण प्रकट होता है।^[17]^{पृष्ठ 297} फिर, x की घटना को बाध्य कहा जाता है यदि x की घटना इनमें से कम से कम एक के दायरे में आती है $\exists x$ या $\forall x$ . अंततः, यदि φ में x की सभी घटनाएँ बाध्य हैं, तो x φ में परिबद्ध है।^[17]^{पृ.142--143}

सहज रूप से, एक चर प्रतीक किसी सूत्र में मुफ़्त है यदि किसी भी बिंदु पर इसकी मात्रा निर्धारित नहीं की गई है:^[17]^{पृ.142--143}में $\forall y P (x, y)$ , चर x की एकमात्र घटना मुफ़्त है जबकि y की घटना बाध्य है। किसी सूत्र में मुक्त और बाध्य चर घटनाओं को आगमनात्मक रूप से निम्नानुसार परिभाषित किया गया है।

परमाणु सूत्र: यदि φ एक परमाणु सूत्र है, तो x φ में मुक्त होता है यदि और केवल यदि x φ में होता है। इसके अलावा, किसी भी परमाणु सूत्र में कोई बाध्य चर नहीं हैं।
निषेध: ¬φ में x मुक्त होता है यदि और केवल यदि x φ में मुक्त होता है। x ¬φ में बंधा हुआ होता है यदि और केवल यदि x φ में बंधा हुआ होता है
द्विआधारी संयोजक: x (φ → ψ) में मुक्त होता है यदि और केवल यदि x या तो φ या ψ में मुक्त होता है। x (φ → ψ) में बाउंड होता है यदि और केवल यदि x या तो φ या ψ में बाउंड होता है। यही नियम → के स्थान पर किसी अन्य बाइनरी संयोजक पर भी लागू होता है।
परिमाणक: x मुफ़्त में होता है $\forall y φ$ , यदि और केवल यदि x φ में मुक्त होता है और x, y से भिन्न प्रतीक है। इसके अलावा, x बाउंड इन होता है $\forall y φ$ , यदि और केवल यदि x, y है या x φ में बंधा हुआ है। यही नियम लागू होता है $\exists$ की जगह $\forall$ .

उदाहरण के लिए, में $\forall x \forall y (P (x) \to Q (x, f (x), z))$ , x और y केवल बंधे हुए होते हैं,^[18] z केवल मुफ़्त होता है, और w न तो होता है क्योंकि यह सूत्र में नहीं होता है।

किसी सूत्र के मुक्त और बाध्य चर को असंयुक्त सेट होने की आवश्यकता नहीं है: सूत्र में $P (x) \to \forall x Q (x)$ , x की पहली घटना, P के तर्क के रूप में, मुफ़्त है जबकि दूसरी, Q के तर्क के रूप में, बाध्य है।

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

उदाहरण: आदेशित एबेलियन समूह

गणित में, क्रमबद्ध एबेलियन समूहों की भाषा में एक स्थिर प्रतीक 0, एक यूनरी फ़ंक्शन प्रतीक -, एक बाइनरी फ़ंक्शन प्रतीक +, और एक बाइनरी संबंध प्रतीक ≤ होता है। तब:

अभिव्यक्ति +(x, y) और +(x, +(y, −(z))) पद हैं। इन्हें आमतौर पर x + y और x + y − z के रूप में लिखा जाता है।
अभिव्यक्ति +(x, y) = 0 और ≤(+(x, +(y, −(z))), +(x, y)) परमाणु सूत्र हैं। इन्हें आमतौर पर x + y = 0 और x + y − z ≤ x + y के रूप में लिखा जाता है।
इजहार $(\forall x\forall y\,[\mathop {\leq } (\mathop {+} (x,y),z)\to \forall x\,\forall y\,\mathop {+} (x,y)=0)]$ एक सूत्र है, जिसे सामान्यतः इस प्रकार लिखा जाता है $\forall x\forall y(x+y\leq z)\to \forall x\forall y(x+y=0).$ इस सूत्र में एक मुक्त चर, z है।

आदेशित एबेलियन समूहों के लिए स्वयंसिद्धों को भाषा में वाक्यों के एक सेट के रूप में व्यक्त किया जा सकता है। उदाहरण के लिए, यह स्वयंसिद्ध कथन कि समूह क्रमविनिमेय है, आमतौर पर लिखा जाता है $(\forall x)(\forall y)[x+y=y+x].$

शब्दार्थ

प्रथम-क्रम भाषा की व्याख्या (तर्क) उस भाषा में प्रत्येक गैर-तार्किक प्रतीक (विधेय प्रतीक, फ़ंक्शन प्रतीक, या स्थिर प्रतीक) को एक संकेत प्रदान करती है। यह प्रवचन का एक क्षेत्र भी निर्धारित करता है जो परिमाणकों की सीमा निर्दिष्ट करता है। इसका परिणाम यह होता है कि प्रत्येक पद को एक वस्तु सौंपी जाती है जिसका वह प्रतिनिधित्व करता है, प्रत्येक विधेय को वस्तुओं का एक गुण सौंपा जाता है, और प्रत्येक वाक्य को एक सत्य मान दिया जाता है। इस प्रकार, एक व्याख्या भाषा के शब्दों, विधेय और सूत्रों को अर्थपूर्ण अर्थ प्रदान करती है। औपचारिक भाषाओं की व्याख्याओं के अध्ययन को औपचारिक शब्दार्थ (तर्क) कहा जाता है। प्रथम-क्रम तर्क के लिए मानक या सत्य परिभाषा#टार्स्की.27 के सिद्धांत शब्दार्थ का विवरण इस प्रकार है। (गेम सेमेन्टिक्स#क्लासिकल लॉजिक|गेम सेमेन्टिक्स को प्रथम-क्रम तर्क के लिए परिभाषित करना भी संभव है, लेकिन पसंद के स्वयंसिद्ध की आवश्यकता के अलावा, गेम सेमेन्टिक्स प्रथम-क्रम तर्क के लिए टार्स्कियन सेमेन्टिक्स से सहमत है, इसलिए गेम सेमेन्टिक्स को यहां विस्तृत नहीं किया जाएगा। .)

प्रथम-क्रम संरचनाएं

किसी व्याख्या को निर्दिष्ट करने का सबसे आम तरीका (विशेषकर गणित में) एक संरचना निर्दिष्ट करना है (जिसे मॉडल भी कहा जाता है; नीचे देखें)। संरचना में प्रवचन डी का एक डोमेन और एक व्याख्या फ़ंक्शन शामिल है $I$ गैर-तार्किक प्रतीकों को विधेय, कार्यों और स्थिरांकों में मैप करना।

प्रवचन डी का क्षेत्र किसी प्रकार की वस्तुओं का एक गैर-रिक्त सेट है। सहज रूप से, एक व्याख्या को देखते हुए, प्रथम-क्रम सूत्र इन वस्तुओं के बारे में एक बयान बन जाता है; उदाहरण के लिए, $\exists xP(x)$ डी में कुछ वस्तु के अस्तित्व को बताता है जिसके लिए विधेय पी सत्य है (या, अधिक सटीक रूप से, जिसके लिए व्याख्या द्वारा विधेय प्रतीक पी को सौंपा गया विधेय सत्य है)। उदाहरण के लिए, कोई D को पूर्णांक का समुच्चय मान सकता है।

गैर-तार्किक प्रतीकों की व्याख्या इस प्रकार की जाती है:

एन-एरी फ़ंक्शन प्रतीक की व्याख्या डी से एक फ़ंक्शन हैⁿसे D. उदाहरण के लिए, यदि प्रवचन का क्षेत्र पूर्णांकों का समूह है, तो arity 2 के फ़ंक्शन प्रतीक f को उस फ़ंक्शन के रूप में व्याख्या किया जा सकता है जो इसके तर्कों का योग देता है। दूसरे शब्दों में, प्रतीक f फ़ंक्शन से संबद्ध है $I(f)$ जो, इस व्याख्या में, जोड़ है।

एक स्थिर प्रतीक की व्याख्या (arity 0 का एक फ़ंक्शन प्रतीक) डी से एक फ़ंक्शन है⁰ (एक सेट जिसका एकमात्र सदस्य खाली टुपल है) से डी, जिसे डी में किसी ऑब्जेक्ट के साथ आसानी से पहचाना जा सकता है। उदाहरण के लिए, एक व्याख्या मान निर्दिष्ट कर सकती है $I(c)=10$ निरंतर प्रतीक के लिए $c$ .

एन-एरी विधेय प्रतीक की व्याख्या डी के तत्वों के एन-टुपल्स का एक सेट है, जो तर्क देता है जिसके लिए विधेय सत्य है। उदाहरण के लिए, एक व्याख्या $I(P)$ एक द्विआधारी विधेय प्रतीक P पूर्णांकों के युग्मों का समूह हो सकता है जैसे कि पहला दूसरे से छोटा हो। इस व्याख्या के अनुसार, विधेय P सत्य होगा यदि इसका पहला तर्क इसके दूसरे तर्क से कम है। समान रूप से, विधेय प्रतीकों को बूलियन-मूल्यवान फ़ंक्शन सौंपा जा सकता है|डी से बूलियन-मूल्यवान फ़ंक्शनⁿको $\{\mathrm {true,false} \}$ .

सत्यमूल्यों का मूल्यांकन

एक सूत्र एक व्याख्या और एक चर असाइनमेंट μ को देखते हुए सही या गलत का मूल्यांकन करता है जो प्रत्येक चर के साथ प्रवचन के क्षेत्र के एक तत्व को जोड़ता है। एक वेरिएबल असाइनमेंट की आवश्यकता का कारण मुक्त वेरिएबल वाले सूत्रों को अर्थ देना है, जैसे $y=x$ . इस सूत्र का सत्य मान इस पर निर्भर करता है कि क्या x और y एक ही व्यक्ति को दर्शाते हैं।

सबसे पहले, परिवर्तनीय असाइनमेंट μ को भाषा के सभी शब्दों तक बढ़ाया जा सकता है, जिसके परिणामस्वरूप प्रत्येक शब्द प्रवचन के क्षेत्र के एक ही तत्व पर मैप होता है। इस असाइनमेंट को बनाने के लिए निम्नलिखित नियमों का उपयोग किया जाता है:

चर। प्रत्येक चर x μ(x) का मूल्यांकन करता है
कार्य. दी गई शर्तें $t_{1},\ldots ,t_{n}$ जिनका मूल्यांकन तत्वों से किया गया है $d_{1},\ldots ,d_{n}$ प्रवचन के क्षेत्र का, और एक एन-एरी फ़ंक्शन प्रतीक एफ, शब्द $f(t_{1},\ldots ,t_{n})$ का मूल्यांकन करता है $(I(f))(d_{1},\ldots ,d_{n})$ .

इसके बाद, प्रत्येक सूत्र को एक सत्य मान दिया गया है। इस असाइनमेंट को बनाने के लिए उपयोग की जाने वाली आगमनात्मक परिभाषा को टी-स्कीमा कहा जाता है।

परमाणु सूत्र (1). एक सूत्र $P(t_{1},\ldots ,t_{n})$ यह इस बात पर निर्भर करता है कि मान सही है या गलत $\langle v_{1},\ldots ,v_{n}\rangle \in I(P)$ , कहाँ $v_{1},\ldots ,v_{n}$ शर्तों का मूल्यांकन हैं $t_{1},\ldots ,t_{n}$ और $I(P)$ की व्याख्या है $P$ , जो अनुमान के अनुसार इसका एक उपसमुच्चय है $D^{n}$ .
परमाणु सूत्र (2). एक सूत्र $t_{1}=t_{2}$ यदि सत्य असाइन किया गया है $t_{1}$ और $t_{2}$ प्रवचन के क्षेत्र की एक ही वस्तु का मूल्यांकन करें (नीचे समानता पर अनुभाग देखें)।
तार्किक संयोजक। प्रपत्र में एक सूत्र $\neg \varphi$ , $\varphi \rightarrow \psi$ , आदि का मूल्यांकन प्रश्न में संयोजक के लिए सत्य तालिका के अनुसार किया जाता है, जैसा कि प्रस्तावात्मक तर्क में होता है।
अस्तित्वगत परिमाणक। एक सूत्र $\exists x\varphi (x)$ एम और के अनुसार सत्य है $\mu$ यदि कोई मूल्यांकन मौजूद है $\mu '$ उन चरों में से जो केवल भिन्न हैं $\mu$ x के मूल्यांकन के संबंध में और ऐसा कि φ व्याख्या M और चर असाइनमेंट के अनुसार सत्य है $\mu '$ . यह औपचारिक परिभाषा इस विचार को दर्शाती है कि $\exists x\varphi (x)$ सत्य है यदि और केवल यदि x के लिए मान चुनने का कोई तरीका है जैसे कि φ(x) संतुष्ट हो।
सार्वभौमिक परिमाणक। एक सूत्र $\forall x\varphi (x)$ एम और के अनुसार सत्य है $\mu$ यदि φ(x) व्याख्या एम और कुछ चर असाइनमेंट द्वारा रचित प्रत्येक जोड़ी के लिए सत्य है $\mu '$ जो इससे भिन्न है $\mu$ केवल x के मान पर. यह इस विचार को दर्शाता है कि $\forall x\varphi (x)$ सत्य है यदि x के मान का प्रत्येक संभावित विकल्प φ(x) को सत्य बनाता है।

यदि किसी सूत्र में मुक्त चर नहीं हैं, और एक वाक्य भी है, तो प्रारंभिक चर असाइनमेंट उसके सत्य मान को प्रभावित नहीं करता है। दूसरे शब्दों में, एम और के अनुसार एक वाक्य सत्य है $\mu$ यदि और केवल यदि यह एम और प्रत्येक अन्य चर असाइनमेंट के अनुसार सत्य है $\mu '$ .

सत्य मूल्यों को परिभाषित करने के लिए एक दूसरा सामान्य दृष्टिकोण है जो परिवर्तनीय असाइनमेंट फ़ंक्शंस पर निर्भर नहीं करता है। इसके बजाय, एक व्याख्या एम को देखते हुए, पहले हस्ताक्षर में निरंतर प्रतीकों का एक संग्रह जोड़ा जाता है, एम में प्रवचन के क्षेत्र के प्रत्येक तत्व के लिए एक; मान लें कि डोमेन में प्रत्येक d के लिए स्थिर प्रतीक c है_d निश्चित है। व्याख्या को विस्तारित किया गया है ताकि प्रत्येक नए स्थिर प्रतीक को डोमेन के संबंधित तत्व को सौंपा जा सके। अब परिमाणित सूत्रों के लिए वाक्यात्मक रूप से सत्य को इस प्रकार परिभाषित किया जाता है:

अस्तित्वगत परिमाणक (वैकल्पिक)। एक सूत्र $\exists x\varphi (x)$ एम के अनुसार सत्य है यदि प्रवचन के क्षेत्र में कुछ डी ऐसा है $\varphi (c_{d})$ धारण करता है. यहाँ $\varphi (c_{d})$ c को प्रतिस्थापित करने का परिणाम है_d φ में x की प्रत्येक मुक्त घटना के लिए।
सार्वभौमिक परिमाणक (वैकल्पिक)। एक सूत्र $\forall x\varphi (x)$ एम के अनुसार सत्य है यदि, प्रवचन के क्षेत्र में प्रत्येक डी के लिए, $\varphi (c_{d})$ एम के अनुसार सत्य है।

यह वैकल्पिक दृष्टिकोण सभी वाक्यों को वैरिएबल असाइनमेंट के माध्यम से दृष्टिकोण के समान सत्य मान देता है।

वैधता, संतुष्टि, और तार्किक परिणाम

यदि एक वाक्य φ किसी दी गई व्याख्या एम के तहत सत्य का मूल्यांकन करता है, तो कोई कहता है कि एम φ को संतुष्ट करता है; यह दर्शाया गया है^[19] $M\vDash \varphi$ . एक वाक्य संतोषजनक है यदि ऐसी कोई व्याख्या हो जिसके अंतर्गत वह सत्य हो। ये सिंबल से थोड़ा अलग है $\vDash$ मॉडल सिद्धांत से, कहाँ $M\vDash \phi$ एक मॉडल में संतुष्टि को दर्शाता है, यानी इसमें मूल्यों का एक उपयुक्त असाइनमेंट है $M$ के डोमेन के चर प्रतीकों के लिए $\phi$ .^[20] मुक्त चर वाले सूत्रों की संतुष्टि अधिक जटिल है, क्योंकि एक व्याख्या अपने आप में ऐसे सूत्र का सत्य मूल्य निर्धारित नहीं करती है। सबसे आम परंपरा यह है कि मुक्त चर वाला एक सूत्र φ है $x_{1}$ , ..., $x_{n}$ कहा जाता है कि यदि सूत्र φ सत्य रहता है तो व्याख्या से संतुष्ट हो जाते हैं, भले ही प्रवचन के क्षेत्र से कौन से व्यक्तियों को इसके मुक्त चर को सौंपा गया हो $x_{1}$ , ..., $x_{n}$ . इसका प्रभाव यह कहने जैसा ही है कि एक सूत्र φ तभी संतुष्ट होता है जब उसका सार्वभौमिक समापन होता है $\forall x_{1}\dots \forall x_{n}\phi (x_{1},\dots ,x_{n})$ संतुष्ट है।

एक सूत्र तार्किक रूप से मान्य (या बस मान्य) है यदि यह प्रत्येक व्याख्या में सत्य है।^[21] ये सूत्र प्रस्तावात्मक तर्क में टॉटोलॉजी (तर्क) के समान भूमिका निभाते हैं।

एक सूत्र φ, सूत्र ψ का एक तार्किक परिणाम है यदि प्रत्येक व्याख्या जो ψ को सत्य बनाती है, वह भी φ को सत्य बनाती है। इस मामले में कोई कहता है कि φ तर्कसंगत रूप से ψ द्वारा निहित है।

बीजगणितीकरण

प्रथम-क्रम तर्क के शब्दार्थ के लिए एक वैकल्पिक दृष्टिकोण अमूर्त बीजगणित के माध्यम से आगे बढ़ता है। यह दृष्टिकोण प्रस्तावित तर्क के लिंडेनबाम-टार्स्की बीजगणित को सामान्यीकृत करता है। प्रथम-क्रम तर्क से परिमाणित चर को हटाने के तीन तरीके हैं जिनमें परिमाणकों को अन्य चर बाइंडिंग टर्म ऑपरेटरों के साथ प्रतिस्थापित करना शामिल नहीं है:

बेलनाकार बीजगणित, अल्फ्रेड टार्स्की और उनके सहयोगियों द्वारा;
पॉलीडिक बीजगणित, पॉल हेल्मोस द्वारा;
विधेय फ़ैक्टर तर्क, मुख्य रूप से विलार्ड वान ऑरमैन क्विन के कारण।

ये बीजगणित सभी जाली (क्रम) हैं जो दो-तत्व बूलियन बीजगणित को उचित रूप से विस्तारित करते हैं।

टार्स्की और गिवंत (1987) ने दिखाया कि प्रथम-क्रम तर्क का टुकड़ा जिसमें तीन से अधिक क्वांटिफायर के दायरे में कोई परमाणु वाक्य नहीं है, संबंध बीजगणित के समान ही अभिव्यंजक शक्ति है।^[22]^: 32–33 यह टुकड़ा बहुत रुचि का है क्योंकि यह पीनो अंकगणित और अधिकांश स्वयंसिद्ध सेट सिद्धांत के लिए पर्याप्त है, जिसमें कैनोनिकल ज़र्मेलो-फ्रेंकेल सेट सिद्धांत भी शामिल है। वे यह भी सिद्ध करते हैं कि आदिम क्रमित युग्म के साथ प्रथम-क्रम तर्क दो क्रमित युग्म प्रक्षेपण कार्यों के साथ संबंध बीजगणित के बराबर है।^[23]^: 803

प्रथम-क्रम सिद्धांत, मॉडल और प्रारंभिक कक्षाएं

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

एक प्रथम-क्रम संरचना जो किसी दिए गए सिद्धांत के सभी वाक्यों को संतुष्ट करती है, उसे सिद्धांत का एक मॉडल कहा जाता है। प्रारंभिक वर्ग किसी विशेष सिद्धांत को संतुष्ट करने वाली सभी संरचनाओं का समूह है। ये कक्षाएं मॉडल सिद्धांत में अध्ययन का एक मुख्य विषय हैं।

कई सिद्धांतों की एक इच्छित व्याख्या होती है, एक निश्चित मॉडल जिसे सिद्धांत का अध्ययन करते समय ध्यान में रखा जाता है। उदाहरण के लिए, पीनो अंकगणित की इच्छित व्याख्या में उनके सामान्य संचालन के साथ सामान्य प्राकृतिक संख्याएँ शामिल होती हैं। हालाँकि, लोवेनहेम-स्कोलेम प्रमेय से पता चलता है कि अधिकांश प्रथम-क्रम सिद्धांतों में अन्य, गैर-मानक मॉडल भी होंगे।

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

खाली डोमेन

उपरोक्त परिभाषा के लिए आवश्यक है कि किसी भी व्याख्या के प्रवचन का क्षेत्र खाली न हो। ऐसी सेटिंग्स हैं, जैसे समावेशी तर्क, जहां खाली डोमेन की अनुमति है। इसके अलावा, यदि बीजगणितीय संरचनाओं के एक वर्ग में एक खाली संरचना शामिल है (उदाहरण के लिए, एक खाली पोसेट है), तो वह वर्ग केवल प्रथम-क्रम तर्क में एक प्राथमिक वर्ग हो सकता है यदि खाली डोमेन की अनुमति है या खाली संरचना को वर्ग से हटा दिया गया है .

हालाँकि, खाली डोमेन के साथ कई कठिनाइयाँ हैं:

अनुमान के कई सामान्य नियम केवल तभी मान्य होते हैं जब प्रवचन का क्षेत्र गैर-रिक्त होना आवश्यक होता है। एक उदाहरण यह बताने वाला नियम है $\varphi \lor \exists x\psi$ तात्पर्य $\exists x(\varphi \lor \psi )$ जब x एक स्वतंत्र चर नहीं है $\varphi$ . यह नियम, जिसका उपयोग सूत्रों को प्रीनेक्स सामान्य रूप में रखने के लिए किया जाता है, गैर-रिक्त डोमेन में सही है, लेकिन यदि खाली डोमेन की अनुमति है तो यह गलत है।
एक व्याख्या में सत्य की परिभाषा जो एक वैरिएबल असाइनमेंट फ़ंक्शन का उपयोग करती है वह खाली डोमेन के साथ काम नहीं कर सकती है, क्योंकि ऐसे कोई वैरिएबल असाइनमेंट फ़ंक्शन नहीं हैं जिनकी सीमा खाली है। (इसी प्रकार, कोई भी स्थिर प्रतीकों को व्याख्याएं निर्दिष्ट नहीं कर सकता है।) इस सत्य परिभाषा के लिए आवश्यक है कि किसी को परमाणु सूत्रों के लिए सत्य मान परिभाषित करने से पहले एक चर असाइनमेंट फ़ंक्शन (ऊपर μ) का चयन करना होगा। फिर किसी वाक्य के सत्य मान को किसी भी परिवर्तनीय असाइनमेंट के तहत उसके सत्य मान के रूप में परिभाषित किया जाता है, और यह साबित होता है कि यह सत्य मान इस बात पर निर्भर नहीं करता है कि कौन सा असाइनमेंट चुना गया है। यदि कोई असाइनमेंट फ़ंक्शन नहीं है तो यह तकनीक काम नहीं करती है; खाली डोमेन को समायोजित करने के लिए इसे बदला जाना चाहिए।

इस प्रकार, जब खाली डोमेन की अनुमति दी जाती है, तो इसे अक्सर एक विशेष मामले के रूप में माना जाना चाहिए। हालाँकि, अधिकांश लेखक परिभाषा के अनुसार खाली डोमेन को बाहर कर देते हैं।

निगमनात्मक प्रणालियाँ

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

यदि कोई भी सूत्र जो प्रणाली में प्राप्त किया जा सकता है वह तार्किक रूप से मान्य है तो एक निगमनात्मक प्रणाली सही है। इसके विपरीत, यदि प्रत्येक तार्किक रूप से मान्य सूत्र व्युत्पन्न है तो एक निगमनात्मक प्रणाली पूर्ण हो जाती है। इस आलेख में चर्चा की गई सभी प्रणालियाँ सुदृढ़ और पूर्ण दोनों हैं। वे इस संपत्ति को भी साझा करते हैं कि यह प्रभावी ढंग से सत्यापित करना संभव है कि कथित रूप से वैध कटौती वास्तव में कटौती है; ऐसी कटौती प्रणालियाँ प्रभावी कहलाती हैं।

निगमनात्मक प्रणालियों की एक प्रमुख संपत्ति यह है कि वे पूरी तरह से वाक्यात्मक हैं, ताकि किसी भी व्याख्या पर विचार किए बिना व्युत्पत्तियों को सत्यापित किया जा सके। इस प्रकार एक ठोस तर्क भाषा की हर संभव व्याख्या में सही होता है, भले ही वह व्याख्या गणित, अर्थशास्त्र या किसी अन्य क्षेत्र के बारे में हो।

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

अनुमान के नियम

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

उदाहरण के लिए, अनुमान का एक सामान्य नियम प्रतिस्थापन का नियम है। यदि t एक पद है और φ एक सूत्र है जिसमें संभवतः चर x शामिल है, तो φ[t/x] φ में x के सभी मुक्त उदाहरणों को t द्वारा प्रतिस्थापित करने का परिणाम है। प्रतिस्थापन नियम में कहा गया है कि किसी भी φ और किसी भी पद t के लिए, कोई φ से φ[t/x] का निष्कर्ष निकाल सकता है, बशर्ते कि प्रतिस्थापन प्रक्रिया के दौरान t का कोई भी मुक्त चर बाध्य न हो। (यदि t का कुछ मुक्त चर बाध्य हो जाता है, तो x के स्थान पर t को प्रतिस्थापित करने के लिए सबसे पहले φ के बाध्य चर को t के मुक्त चर से भिन्न करने के लिए बदलना आवश्यक है।)

यह देखने के लिए कि बाध्य चरों पर प्रतिबंध क्यों आवश्यक है, दिए गए तार्किक रूप से मान्य सूत्र φ पर विचार करें $\exists x(x=y)$ , अंकगणित के (0,1,+,×,=) के हस्ताक्षर में। यदि t शब्द x + 1 है, तो सूत्र φ[t/y] है $\exists x(x=x+1)$ , जो कई व्याख्याओं में गलत होगा। समस्या यह है कि प्रतिस्थापन के दौरान t का मुक्त चर x बाध्य हो गया। इच्छित प्रतिस्थापन को φ के बाध्य चर x का नाम बदलकर किसी और चीज़, मान लीजिए z, द्वारा प्राप्त किया जा सकता है, ताकि प्रतिस्थापन के बाद सूत्र हो $\exists z(z=x+1)$ , जो फिर से तार्किक रूप से मान्य है।

प्रतिस्थापन नियम अनुमान के नियमों के कई सामान्य पहलुओं को प्रदर्शित करता है। यह पूर्णतः वाक्यात्मक है; कोई भी यह बता सकता है कि क्या इसे बिना किसी व्याख्या की अपील के सही ढंग से लागू किया गया था। इसे कब लागू किया जा सकता है, इसकी (वाक्यविन्यास रूप से परिभाषित) सीमाएँ हैं, जिनका व्युत्पत्ति की शुद्धता को बनाए रखने के लिए सम्मान किया जाना चाहिए। इसके अलावा, जैसा कि अक्सर होता है, ये सीमाएँ स्वतंत्र और बाध्य चर के बीच की बातचीत के कारण आवश्यक हैं जो कि अनुमान नियम में शामिल सूत्रों के वाक्यात्मक हेरफेर के दौरान होती हैं।

हिल्बर्ट-शैली प्रणाली और प्राकृतिक कटौती

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

प्राकृतिक कटौती प्रणालियाँ हिल्बर्ट-शैली प्रणालियों से मिलती-जुलती हैं, जिसमें कटौती सूत्रों की एक सीमित सूची होती है। हालाँकि, प्राकृतिक कटौती प्रणालियों में कोई तार्किक सिद्धांत नहीं हैं; वे अनुमान के अतिरिक्त नियम जोड़कर क्षतिपूर्ति करते हैं जिनका उपयोग प्रमाण में सूत्रों में तार्किक संयोजकों में हेरफेर करने के लिए किया जा सकता है।

गणना अनुसरण करती है

प्राकृतिक कटौती प्रणालियों के गुणों का अध्ययन करने के लिए अनुक्रमिक कैलकुलस विकसित किया गया था।^[24] एक समय में एक सूत्र के साथ काम करने के बजाय, यह अनुक्रमों का उपयोग करता है, जो कि रूप की अभिव्यक्ति हैं

A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k},

जहाँ एक₁, ..., ए_n, बी₁, ..., बी_k सूत्र और टर्नस्टाइल प्रतीक हैं $\vdash$ दो हिस्सों को अलग करने के लिए विराम चिह्न के रूप में उपयोग किया जाता है। सहज रूप से, एक अनुक्रम इस विचार को व्यक्त करता है $(A_{1}\land \cdots \land A_{n})$ तात्पर्य $(B_{1}\lor \cdots \lor B_{k})$ .

झांकी विधि

प्रस्तावात्मक तर्क सूत्र के लिए एक झांकी प्रमाण ((a ∨ ¬b) ∧ b) → a

अभी वर्णित विधियों के विपरीत, झांकी विधि में व्युत्पत्तियाँ सूत्रों की सूची नहीं हैं। इसके बजाय, व्युत्पत्ति सूत्रों का एक वृक्ष है। यह दिखाने के लिए कि सूत्र A सिद्ध करने योग्य है, झांकी विधि यह प्रदर्शित करने का प्रयास करती है कि A का निषेध असंतोषजनक है। व्युत्पत्ति का वृक्ष है $\lnot A$ इसके मूल में; पेड़ की शाखाएं इस तरह से लगाएं कि सूत्र की संरचना प्रतिबिंबित हो। उदाहरण के लिए, यह दिखाने के लिए $C\lor D$ असंतोषजनक है, यह दिखाने की आवश्यकता है कि C और D प्रत्येक असंतोषजनक हैं; यह पेरेंट के साथ पेड़ में शाखा बिंदु से मेल खाता है $C\lor D$ और बच्चे सी और डी.

संकल्प

संकल्प (तर्क) अनुमान का एक एकल नियम है, जो प्रथम-क्रम तर्क के लिए एकीकरण (कंप्यूटिंग) # एकीकरण की परिभाषा के साथ, प्रथम-क्रम तर्क के लिए ध्वनि और पूर्ण है। झांकी विधि की तरह, एक सूत्र को यह दिखाकर सिद्ध किया जाता है कि सूत्र का निषेधन असंतोषजनक है। रिज़ॉल्यूशन का उपयोग आमतौर पर स्वचालित प्रमेय सिद्ध करने में किया जाता है।

रिज़ॉल्यूशन विधि केवल उन सूत्रों के साथ काम करती है जो परमाणु सूत्रों के विच्छेदन हैं; मनमाने फ़ार्मुलों को पहले शोलेमाइजेशन के माध्यम से इस रूप में परिवर्तित किया जाना चाहिए। संकल्प नियम कहता है कि परिकल्पनाओं से $A_{1}\lor \cdots \lor A_{k}\lor C$ और $B_{1}\lor \cdots \lor B_{l}\lor \lnot C$ , निष्कर्ष $A_{1}\lor \cdots \lor A_{k}\lor B_{1}\lor \cdots \lor B_{l}$ प्राप्त किया जा सकता है।

सिद्ध पहचान

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

\lnot \forall x\,P(x)\Leftrightarrow \exists x\,\lnot P(x)

\lnot \exists x\,P(x)\Leftrightarrow \forall x\,\lnot P(x)

\forall x\,\forall y\,P(x,y)\Leftrightarrow \forall y\,\forall x\,P(x,y)

\exists x\,\exists y\,P(x,y)\Leftrightarrow \exists y\,\exists x\,P(x,y)

\forall x\,P(x)\land \forall x\,Q(x)\Leftrightarrow \forall x\,(P(x)\land Q(x))

\exists x\,P(x)\lor \exists x\,Q(x)\Leftrightarrow \exists x\,(P(x)\lor Q(x))

P\land \exists x\,Q(x)\Leftrightarrow \exists x\,(P\land Q(x))

(कहाँ

x

मुक्त में नहीं होना चाहिए

P

)

P\lor \forall x\,Q(x)\Leftrightarrow \forall x\,(P\lor Q(x))

(कहाँ

x

मुक्त में नहीं होना चाहिए

P

)

समानता और उसके सिद्धांत

प्रथम-क्रम तर्क में समानता (या पहचान) का उपयोग करने के लिए कई अलग-अलग परंपराएँ हैं। सबसे आम सम्मेलन, जिसे समानता के साथ प्रथम-क्रम तर्क के रूप में जाना जाता है, में समानता प्रतीक को एक आदिम तार्किक प्रतीक के रूप में शामिल किया जाता है, जिसे हमेशा प्रवचन के क्षेत्र के सदस्यों के बीच वास्तविक समानता संबंध के रूप में व्याख्या किया जाता है, जैसे कि दिए गए दो सदस्य एक ही सदस्य हैं . यह दृष्टिकोण नियोजित निगमनात्मक प्रणाली में समानता के बारे में कुछ सिद्धांत भी जोड़ता है। ये समानता सिद्धांत हैं:^[25]^{: 198–200}

रिफ्लेक्सिविटी। प्रत्येक चर x के लिए, x = x.
कार्यों के लिए प्रतिस्थापन. सभी वेरिएबल्स x और y, और किसी भी फ़ंक्शन प्रतीक f के लिए,
x = y → f(..., x, ...) = f(..., y, ...).
सूत्रों के लिए प्रतिस्थापन. किसी भी चर x और y और किसी भी सूत्र φ(x) के लिए, यदि φ' को φ में x की किसी भी संख्या में मुक्त घटनाओं को y के साथ प्रतिस्थापित करके प्राप्त किया जाता है, जैसे कि ये y की मुक्त घटनाएं बनी रहें, तो
x = y → (φ → φ').

ये स्वयंसिद्ध स्कीमा हैं, जिनमें से प्रत्येक स्वयंसिद्धों के अनंत सेट को निर्दिष्ट करता है। तीसरे स्कीमा को अविभाज्य की पहचान#समरूपताओं की अविभाज्यता|लीबनिज़ का नियम, प्रतिस्थापन का सिद्धांत, समरूपताओं की अविवेकशीलता, या प्रतिस्थापन संपत्ति के रूप में जाना जाता है। दूसरा स्कीमा, जिसमें फ़ंक्शन प्रतीक एफ शामिल है, सूत्र का उपयोग करके तीसरे स्कीमा का एक विशेष मामला है (समकक्ष)

x = y → (f(..., x, ...) = z → f(..., y, ...) = z).

समानता के कई अन्य गुण उपरोक्त सिद्धांतों के परिणाम हैं, उदाहरण के लिए:

समरूपता. यदि x = y तो y = x.^[26]
परिवर्तनशीलता. यदि x = y और y = z तो x = z.^[27]

समानता के बिना प्रथम-क्रम तर्क

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

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

समानता के बिना प्रथम-क्रम तर्क को अक्सर दूसरे-क्रम अंकगणित और अंकगणित के अन्य उच्च-क्रम सिद्धांतों के संदर्भ में नियोजित किया जाता है, जहां प्राकृतिक संख्याओं के सेट के बीच समानता संबंध आमतौर पर छोड़ दिया जाता है।

एक सिद्धांत के भीतर समानता को परिभाषित करना

यदि किसी सिद्धांत में एक द्विआधारी सूत्र A(x,y) है जो रिफ्लेक्सिविटी और लाइबनिज के नियम को संतुष्ट करता है, तो सिद्धांत को समानता वाला या समानता वाला सिद्धांत कहा जाता है। सिद्धांत में उपरोक्त स्कीमा के सभी उदाहरण स्वयंसिद्ध के रूप में नहीं, बल्कि व्युत्पन्न प्रमेय के रूप में हो सकते हैं। उदाहरण के लिए, बिना फ़ंक्शन प्रतीकों और संबंधों की एक सीमित संख्या वाले सिद्धांतों में, दो शब्दों s और t को बराबर परिभाषित करके, यदि कोई संबंध अपरिवर्तित है, तो s को t में बदलकर, संबंधों के संदर्भ में समानता का विस्तार करना संभव है। किसी भी तर्क में.

कुछ सिद्धांत समानता की अन्य तदर्थ परिभाषाओं की अनुमति देते हैं:

एक संबंध प्रतीक ≤ के साथ आंशिक आदेशों के सिद्धांत में, कोई s = t को s ≤ t ∧ t ≤ s के संक्षिप्त रूप के रूप में परिभाषित कर सकता है।
एक संबंध ∈ के साथ सेट सिद्धांत में, कोई s = t को संक्षिप्त नाम के रूप में परिभाषित कर सकता है $\forall x (s \in x \leftrightarrow t \in x) \land \forall x (x \in s \leftrightarrow x \in t)$ . समानता की यह परिभाषा तब स्वचालित रूप से समानता के सिद्धांतों को संतुष्ट करती है। इस मामले में, किसी को विस्तारशीलता के सामान्य सिद्धांत को प्रतिस्थापित करना चाहिए, जिसे इस प्रकार कहा जा सकता है $\forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow x=y]$ , एक वैकल्पिक सूत्रीकरण के साथ $\forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow \forall z(x\in z\Leftrightarrow y\in z)]$ , जो कहता है कि यदि समुच्चय x और y में समान अवयव हैं, तो वे भी समान समुच्चय से संबंधित हैं।

धात्विक गुण

उच्च-क्रम तर्क के बजाय प्रथम-क्रम तर्क के उपयोग के लिए एक प्रेरणा यह है कि प्रथम-क्रम तर्क में कई धातु संबंधी गुण होते हैं जो मजबूत तर्क में नहीं होते हैं। ये परिणाम व्यक्तिगत सिद्धांतों के गुणों के बजाय प्रथम-क्रम तर्क के सामान्य गुणों से संबंधित हैं। वे प्रथम-क्रम सिद्धांतों के मॉडल के निर्माण के लिए मौलिक उपकरण प्रदान करते हैं।

पूर्णता और अनिर्णयता

1929 में कर्ट गोडेल द्वारा सिद्ध गोडेल की पूर्णता प्रमेय, यह स्थापित करती है कि प्रथम-क्रम तर्क के लिए ध्वनि, पूर्ण, प्रभावी निगमनात्मक प्रणालियाँ हैं, और इस प्रकार प्रथम-क्रम तार्किक परिणाम संबंध को परिमित सिद्धता द्वारा पकड़ लिया जाता है। सहजता से, यह कथन कि एक सूत्र φ तार्किक रूप से एक सूत्र ψ का तात्पर्य करता है, φ के प्रत्येक मॉडल पर निर्भर करता है; ये मॉडल आम तौर पर मनमाने ढंग से बड़ी कार्डिनैलिटी के होंगे, और इसलिए हर मॉडल की जांच करके तार्किक परिणाम को प्रभावी ढंग से सत्यापित नहीं किया जा सकता है। हालाँकि, सभी परिमित व्युत्पत्तियों की गणना करना और φ से ψ की व्युत्पत्ति की खोज करना संभव है। यदि ψ तार्किक रूप से φ द्वारा निहित है, तो ऐसी व्युत्पत्ति अंततः मिल जाएगी। इस प्रकार प्रथम-क्रम तार्किक परिणाम अर्धनिर्णायक है: वाक्यों के सभी युग्मों (φ,ψ) की प्रभावी गणना करना संभव है, जैसे कि ψ, φ का तार्किक परिणाम है।

प्रस्तावात्मक तर्क के विपरीत, प्रथम-क्रम तर्क निर्णायकता (तर्क) है (यद्यपि अर्धनिर्णायक), बशर्ते कि भाषा में कम से कम 2 (समानता के अलावा) का कम से कम एक विधेय हो। इसका मतलब यह है कि ऐसी कोई निर्णय प्रक्रिया नहीं है जो यह निर्धारित करती हो कि मनमाने सूत्र तार्किक रूप से मान्य हैं या नहीं। यह परिणाम क्रमशः 1936 और 1937 में अलोंजो चर्च और एलन ट्यूरिंग द्वारा स्वतंत्र रूप से स्थापित किया गया था, जो 1928 में डेविड हिल्बर्ट और विल्हेम एकरमैन द्वारा प्रस्तुत एंट्सचीडुंग्सप्रॉब्लम का नकारात्मक उत्तर देता है। उनके प्रमाण पहले के लिए निर्णय समस्या की अघुलनशीलता के बीच एक संबंध प्रदर्शित करते हैं- आदेश तर्क और रुकने की समस्या का समाधान न होना।

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

लोवेनहेम-स्कोलेम प्रमेय

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

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

संहतता प्रमेय

कॉम्पैक्टनेस प्रमेय बताता है कि प्रथम-क्रम वाक्यों के एक सेट में एक मॉडल होता है यदि और केवल तभी जब इसके प्रत्येक परिमित उपसमुच्चय में एक मॉडल हो।^[28] इसका तात्पर्य यह है कि यदि कोई सूत्र प्रथम-क्रम वाले स्वयंसिद्धों के अनंत सेट का तार्किक परिणाम है, तो यह उन स्वयंसिद्धों की कुछ सीमित संख्या का तार्किक परिणाम है। पूर्णता प्रमेय के परिणामस्वरूप इस प्रमेय को सबसे पहले कर्ट गोडेल द्वारा सिद्ध किया गया था, लेकिन समय के साथ कई अतिरिक्त प्रमाण प्राप्त हुए हैं। यह मॉडल सिद्धांत में एक केंद्रीय उपकरण है, जो मॉडल के निर्माण के लिए एक मौलिक विधि प्रदान करता है।

कॉम्पैक्टनेस प्रमेय का एक सीमित प्रभाव होता है जिस पर प्रथम-क्रम संरचनाओं का संग्रह प्राथमिक वर्ग होता है। उदाहरण के लिए, कॉम्पैक्टनेस प्रमेय का तात्पर्य है कि कोई भी सिद्धांत जिसमें मनमाने ढंग से बड़े परिमित मॉडल होते हैं, उसका एक अनंत मॉडल होता है। इस प्रकार सभी परिमित ग्राफ़ (असतत गणित) का वर्ग एक प्रारंभिक वर्ग नहीं है (यही बात कई अन्य बीजगणितीय संरचनाओं के लिए भी लागू होती है)।

प्रथम-क्रम तर्क की अधिक सूक्ष्म सीमाएँ भी हैं जो कॉम्पैक्टनेस प्रमेय द्वारा निहित हैं। उदाहरण के लिए, कंप्यूटर विज्ञान में, कई स्थितियों को राज्यों (नोड्स) और कनेक्शन (निर्देशित किनारों) के निर्देशित ग्राफ के रूप में तैयार किया जा सकता है। ऐसी प्रणाली को मान्य करने के लिए यह दिखाने की आवश्यकता हो सकती है कि किसी भी अच्छे राज्य से किसी बुरे राज्य तक नहीं पहुंचा जा सकता है। इस प्रकार कोई यह निर्धारित करना चाहता है कि क्या अच्छी और बुरी स्थितियाँ ग्राफ़ के अलग-अलग जुड़े घटकों (ग्राफ़ सिद्धांत) में हैं। हालाँकि, कॉम्पैक्टनेस प्रमेय का उपयोग यह दिखाने के लिए किया जा सकता है कि कनेक्टेड ग्राफ़ प्रथम-क्रम तर्क में प्राथमिक वर्ग नहीं हैं, और ग्राफ़ के तर्क में, प्रथम-क्रम तर्क का कोई सूत्र φ(x,y) नहीं है, जो व्यक्त करता है विचार करें कि x से y तक एक पथ है। हालाँकि, जुड़ाव को दूसरे क्रम के तर्क में व्यक्त किया जा सकता है, लेकिन केवल अस्तित्वगत सेट क्वांटिफायर के साथ नहीं, जैसा कि $\Sigma _{1}^{1}$ कॉम्पैक्टनेस का भी आनंद लेता है।

लिंडस्ट्रॉम का प्रमेय

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

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

सीमाएँ

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

उदाहरण के लिए, प्रथम-क्रम तर्क अनिर्णीत है, जिसका अर्थ है कि सिद्धता के लिए एक ठोस, पूर्ण और अंतिम निर्णय एल्गोरिदम असंभव है। इससे सी जैसे दिलचस्प निर्णायक अंशों के अध्ययन को बढ़ावा मिला है₂: दो चर और गिनती परिमाणकों के साथ प्रथम-क्रम तर्क $\exists ^{\geq n}$ और $\exists ^{\leq n}$ .^[29]

अभिव्यंजना

लोवेनहेम-स्कोलेम प्रमेय से पता चलता है कि यदि प्रथम-क्रम सिद्धांत में कोई अनंत मॉडल है, तो इसमें प्रत्येक कार्डिनैलिटी के अनंत मॉडल हैं। विशेष रूप से, अनंत मॉडल वाला कोई भी प्रथम-क्रम सिद्धांत मॉर्ले की श्रेणीबद्धता प्रमेय नहीं हो सकता है। इस प्रकार ऐसा कोई प्रथम-क्रम सिद्धांत नहीं है जिसके एकमात्र मॉडल में उसके डोमेन के रूप में प्राकृतिक संख्याओं का सेट हो, या जिसके एकमात्र मॉडल में उसके डोमेन के रूप में वास्तविक संख्याओं का सेट हो। प्रथम-क्रम तर्क के कई विस्तार, जिनमें अनंत तर्क और उच्च-क्रम तर्क शामिल हैं, इस अर्थ में अधिक अभिव्यंजक हैं कि वे प्राकृतिक संख्याओं या वास्तविक संख्याओं के श्रेणीबद्ध स्वयंसिद्धीकरण की अनुमति देते हैं।^{[clarification needed]}. हालाँकि, यह अभिव्यंजना एक धातु संबंधी लागत पर आती है: लिंडस्ट्रॉम के प्रमेय के अनुसार, कॉम्पैक्टनेस प्रमेय और नीचे की ओर लोवेनहेम-स्कोलेम प्रमेय किसी भी तर्क को प्रथम-क्रम से अधिक मजबूत नहीं रख सकता है।

प्राकृतिक भाषाओं को औपचारिक बनाना

प्रथम-क्रम तर्क प्राकृतिक भाषा में कई सरल क्वांटिफायर निर्माणों को औपचारिक रूप देने में सक्षम है, जैसे कि पर्थ में रहने वाला प्रत्येक व्यक्ति ऑस्ट्रेलिया में रहता है। इसलिए, प्रथम-क्रम तर्क का उपयोग ज्ञान प्रतिनिधित्व भाषाओं, जैसे एफओ (.) के लिए आधार के रूप में किया जाता है।

फिर भी, प्राकृतिक भाषा की जटिल विशेषताएं हैं जिन्हें प्रथम-क्रम तर्क में व्यक्त नहीं किया जा सकता है। कोई भी तार्किक प्रणाली जो प्राकृतिक भाषा के विश्लेषण के लिए एक उपकरण के रूप में उपयुक्त है, उसे प्रथम-क्रम विधेय तर्क की तुलना में अधिक समृद्ध संरचना की आवश्यकता होती है।^[30]

Type	Example	Comment
Quantification over properties	If John is self-satisfied, then there is at least one thing he has in common with Peter.	Example requires a quantifier over predicates, which cannot be implemented in single-sorted first-order logic: Zj → ∃X(Xj∧Xp).
Quantification over properties	Santa Claus has all the attributes of a sadist.	Example requires quantifiers over predicates, which cannot be implemented in single-sorted first-order logic: ∀X(∀x(Sx → Xx) → Xs).
Predicate adverbial	John is walking quickly.	Example cannot be analysed as Wj ∧ Qj; predicate adverbials are not the same kind of thing as second-order predicates such as colour.
Relative adjective	Jumbo is a small elephant.	Example cannot be analysed as Sj ∧ Ej; predicate adjectives are not the same kind of thing as second-order predicates such as colour.
Predicate adverbial modifier	John is walking very quickly.	—
Relative adjective modifier	Jumbo is terribly small.	An expression such as "terribly", when applied to a relative adjective such as "small", results in a new composite relative adjective "terribly small".
Prepositions	Mary is sitting next to John.	The preposition "next to" when applied to "John" results in the predicate adverbial "next to John".

प्रतिबंध, विस्तार और विविधताएँ

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

प्रतिबंधित भाषाएँ

प्रथम-क्रम तर्क का अध्ययन ऊपर वर्णित की तुलना में कम तार्किक प्रतीकों वाली भाषाओं में किया जा सकता है।

क्योंकि $\exists x\varphi (x)$ के रूप में व्यक्त किया जा सकता है $\neg \forall x\neg \varphi (x)$ , और $\forall x\varphi (x)$ के रूप में व्यक्त किया जा सकता है $\neg \exists x\neg \varphi (x)$ , दो परिमाणकों में से कोई एक $\exists$ और $\forall$ गिराया जा सकता है.
तब से $\varphi \lor \psi$ के रूप में व्यक्त किया जा सकता है $\lnot (\lnot \varphi \land \lnot \psi )$ और $\varphi \land \psi$ के रूप में व्यक्त किया जा सकता है $\lnot (\lnot \varphi \lor \lnot \psi )$ , दोनों में से एक $\vee$ या $\wedge$ गिराया जा सकता है. दूसरे शब्दों में, यह होना ही पर्याप्त है $\neg$ और $\vee$ , या $\neg$ और $\wedge$ , एकमात्र तार्किक संयोजक के रूप में।
इसी प्रकार, केवल होना ही पर्याप्त है $\neg$ और $\rightarrow$ तार्किक संयोजकों के रूप में, या केवल शेफ़र स्ट्रोक (NAND) या पियर्स तीर (NOR) ऑपरेटर के रूप में।
फ़ंक्शन प्रतीकों और निरंतर प्रतीकों से पूरी तरह से बचना संभव है, उन्हें उचित तरीके से विधेय प्रतीकों के माध्यम से फिर से लिखना। उदाहरण के लिए, एक स्थिर चिह्न का उपयोग करने के बजाय $\;0$ कोई विधेय का उपयोग कर सकता है $\;0(x)$ (इस प्रकार व्याख्या की गई $\;x=0$ ), और प्रत्येक विधेय को प्रतिस्थापित करें जैसे कि $\;P(0,y)$ साथ $\forall x\;(0(x)\rightarrow P(x,y))$ . एक फ़ंक्शन जैसे $f(x_{1},x_{2},...,x_{n})$ इसी तरह एक विधेय द्वारा प्रतिस्थापित किया जाएगा $F(x_{1},x_{2},...,x_{n},y)$ के रूप में व्याख्या की गई $y=f(x_{1},x_{2},...,x_{n})$ . इस परिवर्तन के लिए मौजूदा सिद्धांत में अतिरिक्त स्वयंसिद्ध जोड़ने की आवश्यकता है, ताकि उपयोग किए गए विधेय प्रतीकों की व्याख्याओं में सही शब्दार्थ हो।^[31]

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

पर्याप्त रूप से अभिव्यंजक सिद्धांतों में फ़ंक्शन प्रतीकों और विधेय प्रतीकों की विशेषताओं को प्रतिबंधित करना भी संभव है। सिद्धांत रूप में कोई भी उन सिद्धांतों में 2 से अधिक योग्यता के कार्यों और 1 से अधिक की योग्यता की भविष्यवाणी से पूरी तरह से छुटकारा पा सकता है जिसमें एक युग्मन फ़ंक्शन शामिल है। यह एरीटी 2 का एक फ़ंक्शन है जो डोमेन के तत्वों के जोड़े लेता है और उनसे युक्त एक ऑर्डर किया हुआ जोड़ा लौटाता है। एरिटी 2 के दो विधेय प्रतीकों का होना भी पर्याप्त है जो एक क्रमित जोड़ी से उसके घटकों तक प्रक्षेपण कार्यों को परिभाषित करते हैं। किसी भी मामले में यह आवश्यक है कि युग्म फलन और उसके प्रक्षेपणों के लिए प्राकृतिक सिद्धांत संतुष्ट हों।

बहु-क्रमबद्ध तर्क

सामान्य प्रथम-क्रम व्याख्याओं में प्रवचन का एक ही क्षेत्र होता है, जिस पर सभी परिमाणकों का दायरा होता है। अनेक-क्रमबद्ध प्रथम-क्रम तर्क वेरिएबल्स को विभिन्न प्रकार के होने की अनुमति देता है, जिनके अलग-अलग डोमेन होते हैं। इसे टाइप किया गया प्रथम-क्रम तर्क भी कहा जाता है, और सॉर्ट को प्रकार भी कहा जाता है (जैसा कि डेटा प्रकार में होता है), लेकिन यह प्रथम-क्रम प्रकार सिद्धांत के समान नहीं है। बहु-क्रमबद्ध प्रथम-क्रम तर्क का उपयोग अक्सर दूसरे-क्रम अंकगणित के अध्ययन में किया जाता है।^[32] जब किसी सिद्धांत में केवल सीमित रूप से कई प्रकार होते हैं, तो कई-क्रमबद्ध प्रथम-क्रम तर्क को एकल-क्रमबद्ध प्रथम-क्रम तर्क में घटाया जा सकता है।^[33]^{: 296–299} एक एकल-क्रमबद्ध सिद्धांत में कई-क्रमबद्ध सिद्धांत में प्रत्येक प्रकार के लिए एक यूनरी विधेय प्रतीक का परिचय देता है, और यह कहते हुए एक स्वयंसिद्ध जोड़ता है कि ये यूनरी विधेय प्रवचन के क्षेत्र को विभाजित करता है। उदाहरण के लिए, यदि दो प्रकार हैं, तो एक विधेय प्रतीक जोड़ता है $P_{1}(x)$ और $P_{2}(x)$ और स्वयंसिद्ध

\forall x(P_{1}(x)\lor P_{2}(x))\land \lnot \exists x(P_{1}(x)\land P_{2}(x))

.

फिर तत्त्व तृप्त करनेवाले $P_{1}$ पहले प्रकार के तत्वों और संतोषजनक तत्वों के रूप में सोचा जाता है $P_{2}$ दूसरे प्रकार के तत्वों के रूप में। परिमाणीकरण की सीमा को सीमित करने के लिए संबंधित विधेय प्रतीक का उपयोग करके कोई भी प्रत्येक प्रकार का परिमाण निर्धारित कर सकता है। उदाहरण के लिए, यह कहने के लिए कि पहले प्रकार का एक तत्व संतोषजनक सूत्र φ(x) है, कोई लिखता है

\exists x(P_{1}(x)\land \varphi (x))

.

अतिरिक्त परिमाणक

अतिरिक्त क्वांटिफायर को प्रथम-क्रम तर्क में जोड़ा जा सकता है।

कभी-कभी ऐसा कहना उपयोगी होता है $P (x)$ बिल्कुल एक x के लिए है, जिसे इस प्रकार व्यक्त किया जा सकता है $\exists! x P (x)$ . यह अंकन, जिसे विशिष्टता परिमाणीकरण कहा जाता है, को किसी सूत्र को संक्षिप्त करने के लिए लिया जा सकता है जैसे $\exists x (P (x) \land\forall y (P (y) \to (x = y)))$ .
अतिरिक्त क्वांटिफायर के साथ प्रथम-क्रम तर्क में परिबद्ध परिमाणक Qx,... हैं, जैसे कि कई x ऐसे हैं जो...। जॉर्ज बूलोस और अन्य के शाखा परिमाणक और बहुवचन क्वांटिफ़िकेशन भी देखें।
परिबद्ध क्वांटिफायर का उपयोग अक्सर सेट सिद्धांत या अंकगणित के अध्ययन में किया जाता है।

असीम तर्क

अनंत तर्क अनंत लंबे वाक्यों की अनुमति देता है। उदाहरण के लिए, कोई अनंत सूत्रों के संयोजन या विच्छेदन, या अनंत अनेक चरों पर परिमाणीकरण की अनुमति दे सकता है। टोपोलॉजी और मॉडल सिद्धांत सहित गणित के क्षेत्रों में असीमित लंबे वाक्य उत्पन्न होते हैं।

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

सबसे अधिक अध्ययन किए जाने वाले इनफ़िनिटरी लॉजिक्स को एल से दर्शाया जाता है_αβ, जहां α और β प्रत्येक या तो कार्डिनल संख्याएं हैं या प्रतीक ∞ हैं। इस अंकन में, सामान्य प्रथम-क्रम तर्क एल है_ωω. तर्क में एल_∞ω, सूत्रों का निर्माण करते समय मनमाने संयोजन या विच्छेदन की अनुमति होती है, और चर की असीमित आपूर्ति होती है। अधिक सामान्यतः, वह तर्क जो κ से कम घटकों के साथ संयोजन या वियोजन की अनुमति देता है उसे एल के रूप में जाना जाता है_κω. उदाहरण के लिए, एल_ω₁ω गणनीय सेट संयोजन और वियोजन की अनुमति देता है।

L के सूत्र में मुक्त चरों का समुच्चय उप>κω में कोई भी कार्डिनैलिटी सख्ती से κ से कम हो सकती है, फिर भी जब एक सूत्र दूसरे के उपसूत्र के रूप में प्रकट होता है, तो उनमें से केवल सीमित संख्या में ही किसी क्वांटिफायर के दायरे में हो सकते हैं।^[34] अन्य अनंत तर्कशास्त्रों में, एक उपसूत्र अनंत रूप से कई परिमाणकों के दायरे में हो सकता है। उदाहरण के लिए, एल में_κ∞, एक एकल सार्वभौमिक या अस्तित्वगत परिमाणक मनमाने ढंग से कई चर को एक साथ बांध सकता है। इसी प्रकार, तर्क एल_κλ λ से कम चरों पर एक साथ मात्रा निर्धारण की अनुमति देता है, साथ ही κ से कम आकार के संयोजन और विच्छेदन की भी अनुमति देता है।

गैर-शास्त्रीय और मोडल तर्कशास्त्र

अंतर्ज्ञानवादी तर्क|अंतर्ज्ञानवादी प्रथम-क्रम तर्क शास्त्रीय तर्क के बजाय अंतर्ज्ञानवादी तर्क का उपयोग करता है; उदाहरण के लिए, ¬¬φ को φ के समतुल्य होने की आवश्यकता नहीं है और ¬ ∀x.φ सामान्यतः ∃ x.¬φ के समतुल्य नहीं है।
प्रथम-क्रम मोडल तर्क किसी को अन्य संभावित दुनिया के साथ-साथ इस आकस्मिक रूप से सच्ची दुनिया का वर्णन करने की अनुमति देता है जिसमें हम रहते हैं। कुछ संस्करणों में, संभावित दुनिया का सेट इस पर निर्भर करता है कि कौन सी संभावित दुनिया में निवास करता है। मोडल लॉजिक में अर्थों के साथ अतिरिक्त मोडल ऑपरेटर होते हैं जिन्हें अनौपचारिक रूप से वर्णित किया जा सकता है, उदाहरण के लिए यह आवश्यक है कि φ (सभी संभावित दुनिया में सत्य) और यह संभव है कि φ (कुछ संभावित दुनिया में सत्य)। मानक प्रथम-क्रम तर्क के साथ हमारे पास एक ही डोमेन है और प्रत्येक विधेय को एक एक्सटेंशन सौंपा गया है। प्रथम-क्रम मोडल लॉजिक के साथ हमारे पास एक डोमेन फ़ंक्शन होता है जो प्रत्येक संभावित दुनिया को अपना स्वयं का डोमेन निर्दिष्ट करता है, ताकि प्रत्येक विधेय को केवल इन संभावित दुनिया के सापेक्ष एक विस्तार मिल सके। यह हमें ऐसे मामलों का मॉडल तैयार करने की अनुमति देता है जहां, उदाहरण के लिए, एलेक्स एक दार्शनिक है, लेकिन एक गणितज्ञ रहा होगा, और हो सकता है कि उसका अस्तित्व ही न हो। पहली संभावित दुनिया में P(a) सत्य है, दूसरे में P(a) गलत है, और तीसरी संभावित दुनिया में डोमेन में कोई a ही नहीं है।
टी-मानदंड फ़ज़ी लॉजिक|फर्स्ट-ऑर्डर फ़ज़ी लॉजिक्स क्लासिकल प्रपोजल कैलकुलस के बजाय प्रपोजल फ़ज़ी लॉजिक्स के प्रथम-क्रम एक्सटेंशन हैं।

फिक्सपॉइंट तर्क

फिक्सपॉइंट लॉजिक सकारात्मक ऑपरेटरों के सबसे कम निश्चित बिंदुओं के तहत क्लोजर जोड़कर प्रथम-क्रम तर्क का विस्तार करता है।^[35]

उच्च-क्रम तर्क

प्रथम-क्रम तर्क की विशेषता यह है कि व्यक्तियों को परिमाणित किया जा सकता है, लेकिन विधेय नहीं। इस प्रकार

\exists a({\text{Phil}}(a))

एक कानूनी प्रथम-क्रम फॉर्मूला है, लेकिन

\exists {\text{Phil}}({\text{Phil}}(a))

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

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

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

स्वचालित प्रमेय सिद्ध करने और औपचारिक विधियाँ

स्वचालित प्रमेय सिद्ध करना कंप्यूटर प्रोग्रामों के विकास को संदर्भित करता है जो गणितीय प्रमेयों की व्युत्पत्ति (औपचारिक प्रमाण) खोजते हैं।^[36] व्युत्पत्तियाँ ढूँढना एक कठिन कार्य है क्योंकि खोज एल्गोरिथ्म बहुत बड़ा हो सकता है; हर संभावित व्युत्पत्ति की विस्तृत खोज सैद्धांतिक रूप से संभव है लेकिन गणित में रुचि की कई प्रणालियों के लिए कम्प्यूटेशनल जटिलता सिद्धांत। इस प्रकार एक अंधी खोज की तुलना में कम समय में व्युत्पत्ति खोजने का प्रयास करने के लिए जटिल अनुमानी कार्य विकसित किए जाते हैं।^{[citation needed]}

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

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

कंप्यूटर विज्ञान में औपचारिक सत्यापन लागू करने के लिए स्वचालित प्रमेय कहावतों का भी उपयोग किया जाता है। इस सेटिंग में, औपचारिक विनिर्देश के संबंध में प्रोग्राम और CPU जैसे हार्डवेयर की शुद्धता को सत्यापित करने के लिए प्रमेय प्रोवर्स का उपयोग किया जाता है। चूँकि इस तरह का विश्लेषण समय लेने वाला और महंगा होता है, इसलिए यह आमतौर पर उन परियोजनाओं के लिए आरक्षित होता है जिनमें खराबी के गंभीर मानवीय या वित्तीय परिणाम हो सकते हैं।

मॉडल जाँच की समस्या के लिए, कुशल कलन विधि को समस्या का निर्णय करने के लिए जाना जाता है कि क्या एक इनपुट परिमित संरचना कम्प्यूटेशनल जटिलता सीमाओं के अलावा, प्रथम-क्रम सूत्र को संतुष्ट करती है: देखें Model checking § First-order logic.

यह भी देखें

ACL2 - एप्लिकेटिव कॉमन लिस्प के लिए एक कम्प्यूटेशनल तर्क
अरिस्टोटेलियन तर्क
समसंगति

एहरनफ्यूच्ट फ्रैसे खेल खेल

लोज में
लोवेनहेम संख्या
नॉनफर्स्टऑर्डरिज़ेबिलिटी
प्रीनेक्स सामान्य रूप
पूर्व विश्लेषिकी
प्रोलॉग
संबंधपरक बीजगणित
संबंधपरक मॉडल
स्कोलेम सामान्य रूप
टार्स्की की दुनिया
ट्रुथ टेबल
प्रकार (मॉडल सिद्धांत)

↑ Hodgson, Dr. J. P. E., "First Order Logic" (archive.org), Saint Joseph's University, Philadelphia, 1995.
↑ Hughes, G. E., & Cresswell, M. J., A New Introduction to Modal Logic (London: Routledge, 1996), p.161.
↑ ^3.0 ^3.1 A. Tarski, Undecidable Theories (1953), p.77. Studies in Logic and the Foundation of Mathematics, North-Holland
↑ Mendelson, Elliott (1964). गणितीय तर्क का परिचय. Van Nostrand Reinhold. p. 56.
↑ Eric M. Hammer: Semantics for Existential Graphs, Journal of Philosophical Logic, Volume 27, Issue 5 (October 1998), page 489: "Development of first-order logic independently of Frege, anticipating prenex and Skolem normal forms"
↑ Goertzel, B., Geisweiller, N., Coelho, L., Janičić, P., & Pennachin, C., Real-World Reasoning: Toward Scalable, Uncertain Spatiotemporal, Contextual and Causal Inference (Amsterdam & Paris: Atlantis Press, 2011), p. 29.
↑ "Predicate Logic | Brilliant Math & Science Wiki". brilliant.org. Retrieved 2020-08-20.
↑ "Introduction to Symbolic Logic: Lecture 2". cstl-cla.semo.edu. Retrieved 2021-01-04.
↑ Hans Hermes (1973). गणितीय तर्क का परिचय. Hochschultext (Springer-Verlag). London: Springer. ISBN 3540058192. ISSN 1431-4657.
↑ More precisely, there is only one language of each variant of one-sorted first-order logic: with or without equality, with or without functions, with or without propositional variables, ....
↑ The word language is sometimes used as a synonym for signature, but this can be confusing because "language" can also refer to the set of formulas.
↑ Eberhard Bergmann and Helga Noll (1977). Mathematische Logik mit Informatik-Anwendungen. Heidelberger Taschenbücher, Sammlung Informatik (in Deutsch). Vol. 187. Heidelberg: Springer. pp. 300–302.
↑ Smullyan, R. M., First-order Logic (New York: Dover Publications, 1968), p. 5.
↑ G. Takeuti, 'Proof Theory' (1989, p.6)
↑ Some authors who use the term "well-formed formula" use "formula" to mean any string of symbols from the alphabet. However, most authors in mathematical logic use "formula" to mean "well-formed formula" and have no term for non-well-formed formulas. In every context, it is only the well-formed formulas that are of interest.
↑ Clark Barrett; Aaron Stump; Cesare Tinelli. "The SMT-LIB Standard: Version 2.0". SMT-LIB. Retrieved 2019-06-15.
↑ ^17.0 ^17.1 ^17.2 W. V. O. Quine, Mathematical Logic (1981). Harvard University Press, 0-674-55451-5.
↑ y occurs bound by rule 4, although it doesn't appear in any atomic subformula
↑ It seems that symbol $\vDash$ was introduced by Kleene, see footnote 30 in Dover's 2002 reprint of his book Mathematical Logic, John Wiley and Sons, 1967.
↑ F. R. Drake, Set theory: An introduction to large cardinals (1974)
↑ Rogers, R. L., Mathematical Logic and Formalized Theories: A Survey of Basic Concepts and Results (Amsterdam/London: North-Holland Publishing Company, 1971), p. 39.
↑ Brink, C., Kahl, W., & Schmidt, G., eds., Relational Methods in Computer Science (Berlin / Heidelberg: Springer, 1997), pp. 32–33.
↑ Anon., Mathematical Reviews (Providence: American Mathematical Society, 2006), p. 803.
↑ Shankar, N., Owre, S., Rushby, J. M., & Stringer-Calvert, D. W. J., PVS Prover Guide 2.4 (Menlo Park: SRI International, November 2001).
↑ Fitting, M., First-Order Logic and Automated Theorem Proving (Berlin/Heidelberg: Springer, 1990), pp. 198–200.
↑ Use formula substitution with φ being x=x and φ' being y=x, then use reflexivity.
↑ Use formula substitution with φ being y=z and φ' being x=z to obtain y=x → (y=z → x=z), then use symmetry and uncurrying.
↑ Hodel, R. E., An Introduction to Mathematical Logic (Mineola NY: Dover, 1995), p. 199.
↑ Horrocks, Ian (2010). "Description Logic: A Formal Foundation for Languages and Tools" (PDF). Slide 22. Archived (PDF) from the original on 2015-09-06.
↑ Gamut 1991, p. 75.
↑ Left-totality can be expressed by an axiom $\forall x_{1},...,x_{n}.\exists y.F(x_{1},...,x_{n},y)$ ; right-uniqueness by $\forall x_{1},...,x_{n},y,y'.$ $F(x_{1},...,x_{n},y)\land F(x_{1},...,x_{n},y')\rightarrow y=y'$ , provided the equality symbol is admitted. Both also apply to constant replacements (for $n=0$ ).
↑ Uzquiano, Gabriel (October 17, 2018). "परिमाणक और परिमाणीकरण". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy (Winter 2018 ed.). See in particular section 3.2, Many-Sorted Quantification.
↑ Enderton, H. A Mathematical Introduction to Logic, second edition. Academic Press, 2001, pp.296–299.
↑ Some authors only admit formulas with finitely many free variables in L_κω, and more generally only formulas with < λ free variables in L_κλ.
↑ Bosse, Uwe (1993). "An Ehrenfeucht–Fraïssé game for fixpoint logic and stratified fixpoint logic". In Börger, Egon (ed.). Computer Science Logic: 6th Workshop, CSL'92, San Miniato, Italy, September 28 - October 2, 1992. Selected Papers. Lecture Notes in Computer Science. Vol. 702. Springer-Verlag. pp. 100–114. ISBN 3-540-56992-8. Zbl 0808.03024.
↑ Melvin Fitting (6 December 2012). प्रथम-क्रम तर्क और स्वचालित प्रमेय सिद्ध करना. Springer Science & Business Media. ISBN 978-1-4612-2360-3.
↑ Avigad, et al. (2007) discuss the process of formally verifying a proof of the prime number theorem. The formalized proof required approximately 30,000 lines of input to the Isabelle proof verifier.

संदर्भ

Rautenberg, Wolfgang (2010), A Concise Introduction to Mathematical Logic (3rd ed.), New York, NY: Springer Science+Business Media, doi:10.1007/978-1-4419-1221-3, ISBN 978-1-4419-1220-6
Andrews, Peter B. (2002); An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed., Berlin: Kluwer Academic Publishers. Available from Springer.
Avigad, Jeremy; Donnelly, Kevin; Gray, David; and Raff, Paul (2007); "A formally verified proof of the prime number theorem", ACM Transactions on Computational Logic, vol. 9 no. 1 doi:10.1145/1297658.1297660
Barwise, Jon (1977). "An Introduction to First-Order Logic". In Barwise, Jon (ed.). Handbook of Mathematical Logic. Studies in Logic and the Foundations of Mathematics. Amsterdam, NL: North-Holland (published 1982). ISBN 978-0-444-86388-1.
Monk, J. Donald (1976). Mathematical Logic. New York, NY: Springer New York. doi:10.1007/978-1-4684-9452-5. ISBN 978-1-4684-9454-9.
Barwise, Jon; and Etchemendy, John (2000); Language Proof and Logic, Stanford, CA: CSLI Publications (Distributed by the University of Chicago Press)
Bocheński, Józef Maria (2007); A Précis of Mathematical Logic, Dordrecht, NL: D. Reidel, translated from the French and German editions by Otto Bird
Ferreirós, José (2001); The Road to Modern Logic — An Interpretation, Bulletin of Symbolic Logic, Volume 7, Issue 4, 2001, pp. 441–484, doi:10.2307/2687794, JSTOR 2687794
Gamut, L. T. F. (1991), Logic, Language, and Meaning, Volume 2: Intensional Logic and Logical Grammar, Chicago, Illinois: University of Chicago Press, ISBN 0-226-28088-8
Hilbert, David; and Ackermann, Wilhelm (1950); Principles of Mathematical Logic, Chelsea (English translation of Grundzüge der theoretischen Logik, 1928 German first edition)
Hodges, Wilfrid (2001); "Classical Logic I: First-Order Logic", in Goble, Lou (ed.); The Blackwell Guide to Philosophical Logic, Blackwell
Ebbinghaus, Heinz-Dieter; Flum, Jörg; and Thomas, Wolfgang (1994); Mathematical Logic, Undergraduate Texts in Mathematics, Berlin, DE/New York, NY: Springer-Verlag, Second Edition, ISBN 978-0-387-94258-2
Tarski, Alfred and Givant, Steven (1987); A Formalization of Set Theory without Variables. Vol.41 of American Mathematical Society colloquium publications, Providence RI: American Mathematical Society, ISBN 978-0821810415

बाहरी संबंध

"Predicate calculus", Encyclopedia of Mathematics, EMS Press, 2001 [1994]
Stanford Encyclopedia of Philosophy: Shapiro, Stewart; "Classical Logic". Covers syntax, model theory, and metatheory for first-order logic in the natural deduction style.
Magnus, P. D.; forall x: an introduction to formal logic. Covers formal semantics and proof theory for first-order logic.
Metamath: an ongoing online project to reconstruct mathematics as a huge first-order theory, using first-order logic and the axiomatic set theory ZFC. Principia Mathematica modernized.
Podnieks, Karl; Introduction to mathematical logic
Cambridge Mathematical Tripos notes (typeset by John Fremlin). These notes cover part of a past Cambridge Mathematical Tripos course taught to undergraduate students (usually) within their third year. The course is entitled "Logic, Computation and Set Theory" and covers Ordinals and cardinals, Posets and Zorn's Lemma, Propositional logic, Predicate logic, Set theory and Consistency issues related to ZFC and other set theories.
Tree Proof Generator can validate or invalidate formulas of first-order logic through the semantic tableaux method.

[1] Hodgson, Dr. J. P. E., "First Order Logic" (archive.org), Saint Joseph's University, Philadelphia, 1995.

[2] Hughes, G. E., & Cresswell, M. J., A New Introduction to Modal Logic (London: Routledge, 1996), p.161.

[Tarski53-3] 3.0 ^3.1 A. Tarski, Undecidable Theories (1953), p.77. Studies in Logic and the Foundation of Mathematics, North-Holland

[4] Mendelson, Elliott (1964). गणितीय तर्क का परिचय. Van Nostrand Reinhold. p. 56.

[5] Eric M. Hammer: Semantics for Existential Graphs, Journal of Philosophical Logic, Volume 27, Issue 5 (October 1998), page 489: "Development of first-order logic independently of Frege, anticipating prenex and Skolem normal forms"

[6] Goertzel, B., Geisweiller, N., Coelho, L., Janičić, P., & Pennachin, C., Real-World Reasoning: Toward Scalable, Uncertain Spatiotemporal, Contextual and Causal Inference (Amsterdam & Paris: Atlantis Press, 2011), p. 29.

[7] "Predicate Logic | Brilliant Math & Science Wiki". brilliant.org. Retrieved 2020-08-20.

[8] "Introduction to Symbolic Logic: Lecture 2". cstl-cla.semo.edu. Retrieved 2021-01-04.

[9] Hans Hermes (1973). गणितीय तर्क का परिचय. Hochschultext (Springer-Verlag). London: Springer. ISBN 3540058192. ISSN 1431-4657.

[10] More precisely, there is only one language of each variant of one-sorted first-order logic: with or without equality, with or without functions, with or without propositional variables, ....

[11] The word language is sometimes used as a synonym for signature, but this can be confusing because "language" can also refer to the set of formulas.

[12] Eberhard Bergmann and Helga Noll (1977). Mathematische Logik mit Informatik-Anwendungen. Heidelberger Taschenbücher, Sammlung Informatik (in Deutsch). Vol. 187. Heidelberg: Springer. pp. 300–302.

[13] Smullyan, R. M., First-order Logic (New York: Dover Publications, 1968), p. 5.

[14] G. Takeuti, 'Proof Theory' (1989, p.6)

[15] Some authors who use the term "well-formed formula" use "formula" to mean any string of symbols from the alphabet. However, most authors in mathematical logic use "formula" to mean "well-formed formula" and have no term for non-well-formed formulas. In every context, it is only the well-formed formulas that are of interest.

[16] Clark Barrett; Aaron Stump; Cesare Tinelli. "The SMT-LIB Standard: Version 2.0". SMT-LIB. Retrieved 2019-06-15.

[Quine81-17] 17.0 ^17.1 ^17.2 W. V. O. Quine, Mathematical Logic (1981). Harvard University Press, 0-674-55451-5.

[18] y occurs bound by rule 4, although it doesn't appear in any atomic subformula

[19] It seems that symbol $\vDash$ was introduced by Kleene, see footnote 30 in Dover's 2002 reprint of his book Mathematical Logic, John Wiley and Sons, 1967.

[20] F. R. Drake, Set theory: An introduction to large cardinals (1974)

[21] Rogers, R. L., Mathematical Logic and Formalized Theories: A Survey of Basic Concepts and Results (Amsterdam/London: North-Holland Publishing Company, 1971), p. 39.

[22] Brink, C., Kahl, W., & Schmidt, G., eds., Relational Methods in Computer Science (Berlin / Heidelberg: Springer, 1997), pp. 32–33.

[23] Anon., Mathematical Reviews (Providence: American Mathematical Society, 2006), p. 803.

[24] Shankar, N., Owre, S., Rushby, J. M., & Stringer-Calvert, D. W. J., PVS Prover Guide 2.4 (Menlo Park: SRI International, November 2001).

[25] Fitting, M., First-Order Logic and Automated Theorem Proving (Berlin/Heidelberg: Springer, 1990), pp. 198–200.

[26] Use formula substitution with φ being x=x and φ' being y=x, then use reflexivity.

[27] Use formula substitution with φ being y=z and φ' being x=z to obtain y=x → (y=z → x=z), then use symmetry and uncurrying.

[28] Hodel, R. E., An Introduction to Mathematical Logic (Mineola NY: Dover, 1995), p. 199.

[29] Horrocks, Ian (2010). "Description Logic: A Formal Foundation for Languages and Tools" (PDF). Slide 22. Archived (PDF) from the original on 2015-09-06.

[FOOTNOTEGamut199175-30] Gamut 1991, p. 75.

[31] Left-totality can be expressed by an axiom $\forall x_{1},...,x_{n}.\exists y.F(x_{1},...,x_{n},y)$ ; right-uniqueness by $\forall x_{1},...,x_{n},y,y'.$ $F(x_{1},...,x_{n},y)\land F(x_{1},...,x_{n},y')\rightarrow y=y'$ , provided the equality symbol is admitted. Both also apply to constant replacements (for $n=0$ ).

[32] Uzquiano, Gabriel (October 17, 2018). "परिमाणक और परिमाणीकरण". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy (Winter 2018 ed.). See in particular section 3.2, Many-Sorted Quantification.

[33] Enderton, H. A Mathematical Introduction to Logic, second edition. Academic Press, 2001, pp.296–299.

[34] Some authors only admit formulas with finitely many free variables in L_κω, and more generally only formulas with < λ free variables in L_κλ.

[35] Bosse, Uwe (1993). "An Ehrenfeucht–Fraïssé game for fixpoint logic and stratified fixpoint logic". In Börger, Egon (ed.). Computer Science Logic: 6th Workshop, CSL'92, San Miniato, Italy, September 28 - October 2, 1992. Selected Papers. Lecture Notes in Computer Science. Vol. 702. Springer-Verlag. pp. 100–114. ISBN 3-540-56992-8. Zbl 0808.03024.

[Fitting2012-36] Melvin Fitting (6 December 2012). प्रथम-क्रम तर्क और स्वचालित प्रमेय सिद्ध करना. Springer Science & Business Media. ISBN 978-1-4612-2360-3.

[37] Avigad, et al. (2007) discuss the process of formally verifying a proof of the prime number theorem. The formalized proof required approximately 30,000 lines of input to the Isabelle proof verifier.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

[28]

[29]

[30]

[31]

[32]

[33]

[34]

[35]

[36]

[37]