अनुमेय नियम

This article is about rules of inference in logic systems. For the concept in decision theory, see admissible decision rule.

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

सभी प्रतिस्थापनों के लिए σ को 'संरचनात्मक' कहा जाता है। (ध्यान दें कि संरचनात्मक शब्द जैसा कि यहां और नीचे प्रयोग किया गया है, क्रमिक कलन में संरचनात्मक नियमों की धारणा से संबंधित नहीं है।) एक संरचनात्मक परिणाम संबंध को 'प्रस्तावात्मक तर्क' कहा जाता है। एक सूत्र A एक तर्क का प्रमेय है $\vdash$ अगर $\varnothing \vdash A$.

परिभाषाएँ

प्रस्तावपरक तर्क गैर-शास्त्रीय तर्क में केवल संरचनात्मक (अर्थात् प्रतिस्थापन (तर्क) -बंद) नियमों के मामले में स्वीकार्यता का व्यवस्थित रूप से अध्ययन किया गया है, जिसका वर्णन हम आगे करेंगे।

बुनियादी तार्किक संयोजकों का एक सेट तय होने दें (उदाहरण के लिए, $\{\to ,\land ,\lor ,\bot \}$ सुपरिंट्यूशनिस्टिक लॉजिक्स के मामले में, या $\{\to ,\bot ,\Box \}$ मॉडल तर्क के मामले में)। प्रस्तावित चर p के एक गणनीय सेट सेट से इन संयोजकों का उपयोग करके अच्छी तरह से बनाए गए सूत्र मुक्त रूप से बनाए गए हैं₀, पी₁, .... एक प्रतिस्थापन (तर्क) σ सूत्र से सूत्र तक का एक कार्य है जो संयोजकों के अनुप्रयोगों के साथ संचार करता है, अर्थात,

$\sigma f(A_{1},\dots ,A_{n})=f(\sigma A_{1},\dots ,\sigma A_{n})$

प्रत्येक संयोजक एफ और सूत्र ए के लिए₁, ... , ए_n. (हम सूत्रों के सेट Γ के लिए प्रतिस्थापन भी लागू कर सकते हैं, बना सकते हैं σΓ = {σA: A ∈ Γ}.) एक टार्स्की-शैली का परिणाम संबंध एक रिश्ता है $\vdash$ सूत्रों के सेट और सूत्रों के बीच, जैसे कि

1. $A\vdash A,$
2. if $\Gamma \vdash A$ then $\Gamma ,\Delta \vdash A,$ ("weakening")
3. if $\Gamma \vdash A$ and $\Delta ,A\vdash B$ then $\Gamma ,\Delta \vdash B,$ ("composition")

सभी फ़ार्मुलों A, B और फ़ार्मुलों के सेट Γ, Δ के लिए। एक परिणामी संबंध ऐसा है

4. if $\Gamma \vdash A$ then $\sigma \Gamma \vdash \sigma A$

सभी प्रतिस्थापनों के लिए σ को 'संरचनात्मक' कहा जाता है। (ध्यान दें कि संरचनात्मक शब्द जैसा कि यहां और नीचे प्रयोग किया गया है, क्रमिक कलन में संरचनात्मक नियमों की धारणा से संबंधित नहीं है।) एक संरचनात्मक परिणाम संबंध को 'प्रस्तावात्मक तर्क' कहा जाता है। एक सूत्र A एक तर्क का प्रमेय है $\vdash$ अगर $\varnothing \vdash A$.

उदाहरण के लिए, हम एक सुपरिंट्यूशनिस्टिक लॉजिक एल को उसके मानक परिणाम संबंध के साथ पहचानते हैं $\vdash _{L}$ मूड सेट करना और स्वयंसिद्धों द्वारा उत्पन्न, और हम इसके वैश्विक परिणाम संबंध के साथ एक सामान्य मोडल तर्क की पहचान करते हैं $\vdash _{L}$ मॉडस पोनेंस, आवश्यकता, और (सिद्धांतों के रूप में) तर्क के प्रमेयों द्वारा उत्पन्न।

एक संरचनात्मक निष्कर्ष नियम (या केवल संक्षेप के लिए नियम) एक जोड़ी (Γ, बी) द्वारा दिया जाता है, जिसे आमतौर पर लिखा जाता है

${\frac {A_{1},\dots ,A_{n}}{B}}\qquad {\text{or}}\qquad A_{1},\dots ,A_{n}/B,$

जहां Γ = {ए₁, ... , ए_n} सूत्रों का एक परिमित सेट है, और B एक सूत्र है। नियम का एक 'उदाहरण' है

$\sigma A_{1},\dots ,\sigma A_{n}/\sigma B$

एक प्रतिस्थापन के लिए σ। नियम Γ/B 'व्युत्पन्न' है $\vdash$, अगर $\Gamma \vdash B$. यह स्वीकार्य है अगर नियम के प्रत्येक उदाहरण के लिए, σB एक प्रमेय है जब भी σΓ से सभी सूत्र प्रमेय हैं। दूसरे शब्दों में, एक नियम स्वीकार्य है यदि वह तर्क में जोड़े जाने पर, नए प्रमेयों को जन्म नहीं देता है। हम भी लिखते हैं $\Gamma \mathrel {|\!\!\!\sim } B$ यदि Γ/B स्वीकार्य है। (ध्यान दें कि ${\phantom {.}}\!{|\!\!\!\sim }$ अपने आप में एक संरचनात्मक परिणाम संबंध है।)

प्रत्येक व्युत्पन्न नियम स्वीकार्य है, लेकिन सामान्य तौर पर इसके विपरीत नहीं। एक तर्क संरचनात्मक रूप से पूर्ण है यदि प्रत्येक स्वीकार्य नियम व्युत्पन्न है, अर्थात, ${\vdash }={\,|\!\!\!\sim }$. एक अच्छी तरह से व्यवहार तार्किक संयुग्मन संयोजी (जैसे अधीक्षणवादी या मोडल लॉजिक्स) के साथ तर्कशास्त्र में, एक नियम $A_{1},\dots ,A_{n}/B$ के बराबर है $A_{1}\land \dots \land A_{n}/B$ स्वीकार्यता और व्युत्पन्नता के संबंध में। इसलिए यह केवल एकात्मक संचालन नियम A/B से निपटने के लिए प्रथागत है।

उदाहरण

• शास्त्रीय तर्क (सीपीसी) संरचनात्मक रूप से पूर्ण है। वास्तव में, मान लें कि ए/बी एक गैर-व्युत्पन्न नियम है, और एक असाइनमेंट वी तय करें जैसे वी (ए) = 1, और वी (बी) = 0। एक प्रतिस्थापन σ परिभाषित करें जैसे कि प्रत्येक चर पी के लिए, σp = $\top$ अगर वी (पी) = 1, और σp = $\bot$ अगर v(p) = 0. तो σA एक प्रमेय है, लेकिन σB नहीं है (वास्तव में, ¬σB एक प्रमेय है)। इस प्रकार नियम ए/बी भी स्वीकार्य नहीं है। (वही तर्क किसी भी बहु-मूल्यवान तर्क एल पर लागू होता है जो तार्किक मैट्रिक्स के संबंध में पूरा होता है, जिनके सभी तत्वों का नाम एल की भाषा में होता है।)
• जॉर्ज क्रेज़ेल-हिलेरी पटनम नियम (जिसे रोनाल्ड हैरोप के नियम या आधार नियम की स्वतंत्रता के रूप में भी जाना जाता है)

$({\mathit {KPR}})\qquad {\frac {\neg p\to q\lor r}{(\neg p\to q)\lor (\neg p\to r)}}$

अंतर्ज्ञानवादी तर्क (आईपीसी) में स्वीकार्य है। वास्तव में, यह प्रत्येक अंधज्ञानवादी तर्क में स्वीकार्य है। दूसरी ओर सूत्र है

$(\neg p\to q\lor r)\to ((\neg p\to q)\lor (\neg p\to r))$

एक अंतर्ज्ञानवादी प्रमेय नहीं है; इसलिए केपीआर आईपीसी में व्युत्पन्न नहीं है। विशेष रूप से, IPC संरचनात्मक रूप से पूर्ण नहीं है।

• नियम

${\frac {\Box p}{p}}$

K, D, K4, S4, GL जैसे कई मोडल लॉजिक्स में स्वीकार्य है (कृपके सिमेंटिक्स#कॉरस्पोंडेंस एंड कंप्लीटनेस फॉर नेम्स ऑफ मोडल लॉजिक्स देखें)। यह S4 में व्युत्पन्न है, लेकिन यह K, D, K4, या GL में व्युत्पन्न नहीं है।

• नियम

${\frac {\Diamond p\land \Diamond \neg p}{\bot }}$

हर सामान्य मोडल लॉजिक में स्वीकार्य है। यह GL और S4.1 में व्युत्पन्न है, लेकिन यह K, D, K4, S4, या S5 में व्युत्पन्न नहीं है।

• लोब का प्रमेय|लोब का नियम

$({\mathit {LR}})\qquad {\frac {\Box p\to p}{p}}$

मूल मोडल लॉजिक K में स्वीकार्य (लेकिन व्युत्पन्न नहीं) है, और यह GL में व्युत्पन्न है। हालांकि, K4 में LR स्वीकार्य नहीं है। विशेष रूप से, यह सामान्य रूप से सत्य नहीं है कि तर्क L में स्वीकार्य नियम इसके विस्तार में स्वीकार्य होना चाहिए।

• मध्यवर्ती लॉजिक | गोडेल-डमेट लॉजिक (LC), और मॉडल लॉजिक Grz.3 संरचनात्मक रूप से पूर्ण हैं। टी-नॉर्म फ़ज़ी लॉजिक भी संरचनात्मक रूप से पूर्ण है।

निर्णायकता और घटे हुए नियम

किसी दिए गए तर्क के स्वीकार्य नियमों के बारे में मूल प्रश्न यह है कि क्या सभी स्वीकार्य नियमों का सेट निर्णायक सेट है। ध्यान दें कि समस्या गैर-तुच्छ है, भले ही तर्क स्वयं (अर्थात, इसके प्रमेयों का सेट) निर्णायकता (तर्क) है: नियम ए/बी की स्वीकार्यता की परिभाषा में सभी प्रस्तावित प्रतिस्थापनों पर एक असीमित सार्वभौमिक क्वांटिफायर शामिल है। इसलिए एक प्राथमिकता हम केवल यह जानते हैं कि एक निर्णायक तर्क में नियम की स्वीकार्यता है $\Pi _{1}^{0}$ (यानी, इसका पूरक पुनरावर्ती गणना योग्य है)। उदाहरण के लिए, यह ज्ञात है कि बिमॉडल लॉजिक्स में स्वीकार्यता K_u और के 4_u (सार्वभौमिक साधन के साथ K या K4 का विस्तार) अनिर्णीत है। उल्लेखनीय रूप से, बुनियादी मोडल लॉजिक K में स्वीकार्यता की निर्णायकता एक बड़ी खुली समस्या है।

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

${\frac {\bigvee _{i=0}^{n}{\bigl (}\bigwedge _{j=0}^{k}\neg _{i,j}^{0}p_{j}\land \bigwedge _{j=0}^{k}\neg _{i,j}^{1}\Box p_{j}{\bigr )}}{p_{0}}},$

जहां प्रत्येक $\neg _{i,j}^{u}$ या तो रिक्त है, या तार्किक निषेध है $\neg$. प्रत्येक नियम r के लिए, हम प्रभावी रूप से एक कम नियम s (जिसे r का घटा हुआ रूप कहा जाता है) का निर्माण कर सकते हैं, जैसे कि कोई भी तर्क स्वीकार करता है (या प्राप्त करता है) r यदि और केवल अगर यह स्वीकार करता है (या प्राप्त करता है), सभी उपसूत्रों के लिए विस्तार चर प्रस्तुत करके ए में, और परिणाम को पूर्ण वियोगात्मक सामान्य रूप में व्यक्त करना। इस प्रकार कम नियमों की स्वीकार्यता के लिए एक निर्णय एल्गोरिथम का निर्माण करना पर्याप्त है।

होने देना $\textstyle \bigvee _{i=0}^{n}\varphi _{i}/p_{0}$ ऊपर के रूप में एक कम नियम बनें। हम हर संयोजन की पहचान करते हैं $\varphi _{i}$ सेट के साथ $\{\neg _{i,j}^{0}p_{j},\neg _{i,j}^{1}\Box p_{j}\mid j\leq k\}$ इसके जोड़ों का। सेट के किसी भी उपसमुच्चय W के लिए $\{\varphi _{i}\mid i\leq n\}$ सभी संयोजनों में से, आइए हम एक क्रिपके मॉडल को परिभाषित करें $M=\langle W,R,{\Vdash }\rangle$ द्वारा

$\varphi _{i}\Vdash p_{j}\iff p_{j}\in \varphi _{i},$

$\varphi _{i}\,R\,\varphi _{i'}\iff \forall j\leq k\,(\Box p_{j}\in \varphi _{i}\Rightarrow \{p_{j},\Box p_{j}\}\subseteq \varphi _{i'}).$

फिर निम्नलिखित K4 में स्वीकार्यता के लिए एल्गोरिथम मानदंड प्रदान करता है: प्रमेय। नियम $\textstyle \bigvee _{i=0}^{n}\varphi _{i}/p_{0}$ K4 में स्वीकार्य नहीं है अगर और केवल अगर कोई सेट मौजूद है $W\subseteq \{\varphi _{i}\mid i\leq n\}$ ऐसा है कि

1. $\varphi _{i}\nVdash p_{0}$ कुछ के लिए $i\leq n,$
2. $\varphi _{i}\Vdash \varphi _{i}$ हरएक के लिए $i\leq n,$
3. W के प्रत्येक उपसमुच्चय D के लिए तत्व मौजूद हैं $\alpha ,\beta \in W$ जैसे कि समानताएं

$\alpha \Vdash \Box p_{j}$ अगर और केवल अगर $\varphi \Vdash p_{j}\land \Box p_{j}$ हरएक के लिए $\varphi \in D$

$\alpha \Vdash \Box p_{j}$ अगर और केवल अगर $\alpha \Vdash p_{j}$ और $\varphi \Vdash p_{j}\land \Box p_{j}$ हरएक के लिए $\varphi \in D$

सभी जे के लिए पकड़ो।

लॉजिक्स S4, GL, और Grz के लिए भी इसी तरह के मापदंड पाए जा सकते हैं। इसके अलावा, अंतर्ज्ञानवादी तर्क में स्वीकार्यता को मोडल साथी का उपयोग करके Grz में स्वीकार्यता तक कम किया जा सकता है। गोडेल-मैकिन्से-टार्स्की अनुवाद:

$A\,|\!\!\!\sim _{IPC}B$ अगर और केवल अगर $T(A)\,|\!\!\!\sim _{Grz}T(B).$

रयबाकोव (1997) ने स्वीकार्यता की निर्णायकता दिखाने के लिए बहुत अधिक परिष्कृत तकनीकों का विकास किया, जो सकर्मक (यानी, K4 या IPC का विस्तार) मोडल और सुपरिंट्यूशनिस्टिक लॉजिक्स के एक मजबूत (अनंत) वर्ग पर लागू होता है, जिसमें उदा। एस4.1, एस4.2, एस4.3, केसी, टी_k (साथ ही उपर्युक्त लॉजिक्स IPC, K4, S4, GL, Grz)। निर्णायक होने के बावजूद, स्वीकार्यता समस्या में अपेक्षाकृत उच्च कम्प्यूटेशनल जटिलता सिद्धांत है, यहां तक ​​​​कि सरल लॉजिक्स में भी: बुनियादी सकर्मक लॉजिक्स IPC, K4, S4, GL, Grz में नियमों की स्वीकार्यता NEXP-पूर्ण है। यह इन लॉजिक्स में व्युत्पन्नता समस्या (नियमों या सूत्रों के लिए) के विपरीत होना चाहिए, जो पीएसपीएसीई-पूर्ण है।

प्रोजेक्टिविटी और एकता

प्रोपोज़िशनल लॉजिक्स में स्वीकार्यता मोडल बीजगणित या हेटिंग बीजगणित के समीकरण सिद्धांत में एकीकरण से निकटता से संबंधित है। कनेक्शन घिलार्डी (1999, 2000) द्वारा विकसित किया गया था। तार्किक सेटअप में, तर्क की भाषा में सूत्र ए का एक एकीकृतकर्ता एल (एक एल - लघु के लिए यूनिफायर) एक प्रतिस्थापन σ है जैसे कि σA L का एक प्रमेय है। (इस धारणा का उपयोग करते हुए, हम L में नियम A/B की स्वीकार्यता को फिर से परिभाषित कर सकते हैं क्योंकि प्रत्येक L- A का एकीकरण करने वाला एक L' है। '-बी का यूनिफायर।) एक एल-यूनीफायर σ एक एल-यूनिफायर τ से कम सामान्य है, जिसे σ ≤ लिखा जाता है τ, यदि कोई प्रतिस्थापन υ मौजूद है जैसे कि

$\vdash _{L}\sigma p\leftrightarrow \upsilon \tau p$

प्रत्येक चर के लिए p. फॉर्मूला ए का 'यूनिफ़ायर का पूरा सेट' ए के एल-यूनिफ़ायर का एक सेट एस है, जैसे कि ए का हर एल-यूनिफ़ायर एस से कुछ यूनिफ़ायर से कम सामान्य है। ए का सबसे सामान्य यूनिफ़ायर (एमजीयू) एक यूनिफ़ायर है σ ऐसा है कि {σ} ए के यूनिफायरों का एक पूरा सेट है। यह इस प्रकार है कि यदि एस ए के यूनिफायरों का एक पूरा सेट है, तो एक नियम ए / बी एल-स्वीकार्य है अगर और केवल अगर एस में प्रत्येक σ एक एल है -बी के यूनिफायर। इस प्रकार हम स्वीकार्य नियमों को चिह्नित कर सकते हैं यदि हम यूनिफायरों के अच्छे व्यवहार वाले पूर्ण सेट पा सकते हैं।

फ़ार्मुलों का एक महत्वपूर्ण वर्ग जिसमें एक सबसे सामान्य यूनिफ़ायर है, 'प्रोजेक्टिव फ़ार्मुलों' हैं: ये फ़ार्मुलों ए हैं जैसे कि ए का एक यूनिफ़ायर σ मौजूद है जैसे कि

$A\vdash _{L}B\leftrightarrow \sigma B$

प्रत्येक सूत्र B के लिए। ध्यान दें कि σ A का एक MGU है। क्रिपके सिमेंटिक्स # फाइनिट मॉडल प्रॉपर्टी के साथ सकर्मक मोडल और सुपरिंट्यूशनिस्टिक लॉजिक्स में, कोई प्रोजेक्टिव फॉर्मूलों को सिमेंटिक रूप से चित्रित कर सकता है, जिनके परिमित एल-मॉडल के सेट में 'एक्सटेंशन प्रॉपर्टी' है। : यदि एम एक रूट आर के साथ एक परिमित क्रिपके एल-मॉडल है जिसका क्लस्टर एक सिंगलटन (गणित) है, और सूत्र ए आर को छोड़कर एम के सभी बिंदुओं पर रखता है, तो हम आर में चर के मूल्यांकन को बदल सकते हैं ताकि बना सकें आर पर भी एक सच है। इसके अलावा, प्रमाण किसी दिए गए प्रोजेक्टिव फॉर्मूला ए के लिए एमजीयू का एक स्पष्ट निर्माण प्रदान करता है।

मूल सकर्मक लॉजिक्स IPC, K4, S4, GL, Grz में (और आमतौर पर परिमित मॉडल संपत्ति के साथ किसी भी सकर्मक तर्क में जिसका परिमित फ्रेम का सेट किसी अन्य प्रकार की विस्तार संपत्ति को संतुष्ट करता है), हम प्रभावी रूप से किसी भी सूत्र A के लिए इसका निर्माण कर सकते हैं ' प्रक्षेपी सन्निकटन' Π(ए): अनुमानित सूत्रों का एक सीमित सेट जैसे कि

1. $P\vdash _{L}A$ हरएक के लिए $P\in \Pi (A),$
2. A का प्रत्येक एकरूपता Π(A) के सूत्र का एकरूप है।

यह इस प्रकार है कि Π (ए) के तत्वों के एमजीयू का सेट ए के यूनिफायरों का एक पूरा सेट है। इसके अलावा, यदि पी एक अनुमानित सूत्र है, तो

$P\,|\!\!\!\sim _{L}B$ अगर और केवल अगर $P\vdash _{L}B$

किसी भी सूत्र बी के लिए। इस प्रकार हम स्वीकार्य नियमों के निम्नलिखित प्रभावी लक्षण वर्णन प्राप्त करते हैं:

$A\,|\!\!\!\sim _{L}B$ अगर और केवल अगर $\forall P\in \Pi (A)\,(P\vdash _{L}B).$

स्वीकार्य नियमों के आधार

एल को तर्क बनने दो। एल-स्वीकार्य नियमों के सेट आर को 'आधार' कहा जाता है स्वीकार्य नियमों की, यदि प्रत्येक स्वीकार्य नियम Γ/B प्रतिस्थापन, संरचना और कमजोर करने का उपयोग करके आर और एल के व्युत्पन्न नियमों से प्राप्त किया जा सकता है। दूसरे शब्दों में, R एक आधार है यदि और केवल यदि ${\phantom {.}}\!{|\!\!\!\sim _{L}}$ सबसे छोटा संरचनात्मक परिणाम संबंध है जिसमें शामिल है $\vdash _{L}$ और आर.

ध्यान दें कि एक निर्णायक तर्क के स्वीकार्य नियमों की निर्णायकता पुनरावर्ती (या पुनरावर्ती गणना योग्य) आधारों के अस्तित्व के बराबर है: एक ओर, सभी स्वीकार्य नियमों का सेट एक पुनरावर्ती आधार है यदि स्वीकार्यता निर्णायक है। दूसरी ओर, स्वीकार्य नियमों का सेट हमेशा सह-पुनरावर्ती रूप से गणना योग्य होता है, और यदि हमारे पास एक पुनरावर्ती गणना योग्य आधार है, तो स्वीकार्य नियमों का सेट भी पुनरावर्ती रूप से गणना योग्य होता है; इसलिए यह निर्णायक है। (दूसरे शब्दों में, हम निम्नलिखित कलन विधि द्वारा A/B की स्वीकार्यता तय कर सकते हैं: हम समानांतर दो संपूर्ण खोजों में शुरू करते हैं, एक प्रतिस्थापन σ के लिए जो A को एकीकृत करता है लेकिन B को नहीं, और एक R और A/B की व्युत्पत्ति के लिए $\vdash _{L}$. खोजों में से एक को अंततः एक उत्तर के साथ आना पड़ता है।) निर्णायकता के अलावा, स्वीकार्य नियमों के स्पष्ट आधार कुछ अनुप्रयोगों के लिए उपयोगी होते हैं, उदा। सबूत जटिलता में। किसी दिए गए तर्क के लिए, हम पूछ सकते हैं कि क्या इसमें स्वीकार्य नियमों का एक पुनरावर्ती या परिमित आधार है, और एक स्पष्ट आधार प्रदान करने के लिए। यदि किसी तर्क का कोई परिमित आधार नहीं है, तब भी इसका एक स्वतंत्र आधार हो सकता है: एक आधार 'आर' ऐसा कि 'आर' का कोई उचित उपसमुच्चय एक आधार नहीं है।

सामान्य तौर पर, वांछनीय गुणों वाले आधारों के अस्तित्व के बारे में बहुत कम कहा जा सकता है। उदाहरण के लिए, जबकि सारणीबद्ध लॉजिक्स आम तौर पर अच्छी तरह से व्यवहार किया जाता है, और हमेशा सूक्ष्म रूप से अभिगृहीत होता है, वहां नियमों के परिमित या स्वतंत्र आधार के बिना सारणीबद्ध मोडल लॉजिक्स मौजूद होते हैं। परिमित आधार अपेक्षाकृत दुर्लभ हैं: यहां तक ​​​​कि मूल सकर्मक लॉजिक्स IPC, K4, S4, GL, Grz के पास स्वीकार्य नियमों का परिमित आधार नहीं है, हालांकि उनके पास स्वतंत्र आधार हैं।

आधारों के उदाहरण

• खाली सेट एल-स्वीकार्य नियमों का आधार है यदि और केवल एल संरचनात्मक रूप से पूर्ण है।
• मोडल लॉजिक S4.3 के प्रत्येक विस्तार (विशेष रूप से, S5 सहित) का एक सीमित आधार है जिसमें एकल नियम शामिल है

${\frac {\Diamond p\land \Diamond \neg p}{\bot }}.$

• Visser के नियम

${\frac {\displaystyle {\Bigl (}\bigwedge _{i=1}^{n}(p_{i}\to q_{i})\to p_{n+1}\lor p_{n+2}{\Bigr )}\lor r}{\displaystyle \bigvee _{j=1}^{n+2}{\Bigl (}\bigwedge _{i=1}^{n}(p_{i}\to q_{i})\to p_{j}{\Bigr )}\lor r}},\qquad n\geq 1$

IPC या KC में स्वीकार्य नियमों का आधार हैं।

• नियम

${\frac {\displaystyle \Box {\Bigl (}\Box q\to \bigvee _{i=1}^{n}\Box p_{i}{\Bigr )}\lor \Box r}{\displaystyle \bigvee _{i=1}^{n}\Box (q\land \Box q\to p_{i})\lor r}},\qquad n\geq 0$

जीएल के स्वीकार्य नियमों का आधार हैं। (ध्यान दें कि खाली संयोजन के रूप में परिभाषित किया गया है $\bot$.)

• नियम

${\frac {\displaystyle \Box {\Bigl (}\Box (q\to \Box q)\to \bigvee _{i=1}^{n}\Box p_{i}{\Bigr )}\lor \Box r}{\displaystyle \bigvee _{i=1}^{n}\Box (\Box q\to p_{i})\lor r}},\qquad n\geq 0$

S4 या Grz के स्वीकार्य नियमों का आधार हैं।

स्वीकार्य नियमों के लिए शब्दार्थ

एक नियम Γ/B एक मोडल या इंट्यूशनिस्टिक क्रिपके फ्रेम में 'वैध' है $F=\langle W,R\rangle$, यदि निम्न प्रत्येक मूल्यांकन के लिए सत्य है $\Vdash$ एफ में:

यदि सभी के लिए $A\in \Gamma$ $\forall x\in W\,(x\Vdash A)$, तब $\forall x\in W\,(x\Vdash B)$.

(यदि आवश्यक हो तो परिभाषा सामान्य रूप से सामान्य फ्रेम के लिए सामान्यीकृत होती है।)

मान लीजिए कि X, W का एक उपसमुच्चय है, और t, W का एक बिंदु है। हम कहते हैं कि t है

• एक्स का एक 'रिफ्लेक्सिव टाइट पूर्ववर्ती', अगर डब्ल्यू में हर वाई के लिए: टी आर वाई अगर और केवल अगर टी = वाई या एक्स में कुछ एक्स के लिए: एक्स = वाई या एक्स आर वाई,
• X का एक 'अपरिवर्तक तंग पूर्ववर्ती', यदि W में प्रत्येक y के लिए: t R y यदि और केवल यदि X में कुछ x के लिए: x = y या x R y ।

हम कहते हैं कि एक फ्रेम F में रिफ्लेक्सिव (इरेफ्लेक्सिव) टाइट पूर्ववर्ती हैं, यदि W के प्रत्येक परिमित उपसमुच्चय X के लिए, W में X का रिफ्लेक्सिव (इरेफ्लेक्टिव) टाइट पूर्ववर्ती मौजूद है।

अपने पास:

• आईपीसी में एक नियम स्वीकार्य है अगर और केवल अगर यह सभी अंतर्ज्ञानवादी फ्रेम में मान्य है जिसमें रिफ्लेक्सिव टाइट पूर्ववर्ती हैं,
• K4 में एक नियम स्वीकार्य है अगर और केवल अगर यह उन सभी सकर्मक संबंध फ़्रेमों में मान्य है जिनके प्रतिवर्ती और अप्रतिबंधात्मक तंग पूर्ववर्ती हैं,
• एक नियम S4 में स्वीकार्य है अगर और केवल अगर यह सभी सकर्मक प्रतिवर्त संबंध फ्रेम में मान्य है जिसमें रिफ्लेक्सिव टाइट पूर्ववर्ती हैं,
• जीएल में एक नियम स्वीकार्य है अगर और केवल अगर यह सभी सकर्मक विपरीत अच्छी तरह से स्थापित संबंध | अच्छी तरह से स्थापित फ्रेम में मान्य है जिसमें अपरिवर्तनीय तंग पूर्ववर्ती हैं।

ध्यान दें कि कुछ तुच्छ मामलों के अलावा, तंग पूर्ववर्ती वाले फ़्रेम अनंत होने चाहिए। इसलिए बुनियादी सकर्मक लॉजिक्स में स्वीकार्य नियम परिमित मॉडल संपत्ति का आनंद नहीं लेते हैं।

संरचनात्मक पूर्णता

जबकि संरचनात्मक रूप से पूर्ण लॉजिक्स का सामान्य वर्गीकरण आसान काम नहीं है, हमें कुछ विशेष मामलों की अच्छी समझ है।

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

${\frac {(p\to q)\to p\lor r}{((p\to q)\to p)\lor ((p\to q)\to r)}}$

अंतर्ज्ञानवादी तर्क में स्वीकार्य है लेकिन व्युत्पन्न नहीं है, और इसमें केवल प्रभाव और संयोजन शामिल हैं।

हम अधिकतम संरचनात्मक रूप से अपूर्ण सकर्मक लॉजिक्स जानते हैं। एक तर्क को 'वंशानुगत रूप से संरचनात्मक रूप से पूर्ण' कहा जाता है, यदि कोई विस्तार संरचनात्मक रूप से पूर्ण हो। उदाहरण के लिए, शास्त्रीय तर्क, साथ ही ऊपर वर्णित तर्क LC और Grz.3, आनुवंशिक रूप से संरचनात्मक रूप से पूर्ण हैं। Citkin और Rybakov द्वारा क्रमशः आनुवंशिक रूप से संरचनात्मक रूप से पूर्ण सुपरिंट्यूशनिस्टिक और सकर्मक मोडल लॉजिक्स का पूरा विवरण दिया गया था। अर्थात्, एक अधीक्षणवादी तर्क आनुवंशिक रूप से संरचनात्मक रूप से पूर्ण होता है यदि और केवल अगर यह पांच कृपके फ्रेमों में से किसी में मान्य नहीं है

इसी तरह, K4 का एक विस्तार आनुवंशिक रूप से संरचनात्मक रूप से पूर्ण होता है यदि और केवल अगर यह कुछ बीस क्रिप्के फ़्रेमों में से किसी में मान्य नहीं है (उपर्युक्त पांच इंट्यूशनिस्टिक फ़्रेमों सहित)।

संरचनात्मक रूप से पूर्ण लॉजिक्स मौजूद हैं जो वंशानुगत रूप से संरचनात्मक रूप से पूर्ण नहीं हैं: उदाहरण के लिए, मध्यवर्ती तर्क | मेदवेदेव का तर्क संरचनात्मक रूप से पूर्ण है, लेकिन यह संरचनात्मक रूप से अपूर्ण तर्क KC में शामिल है।

वेरिएंट

पैरामीटर वाला नियम फॉर्म का नियम है

${\frac {A(p_{1},\dots ,p_{n},s_{1},\dots ,s_{k})}{B(p_{1},\dots ,p_{n},s_{1},\dots ,s_{k})}},$

जिनके चर नियमित चर p में विभाजित हैं_i, और पैरामीटर एस_i. नियम L-स्वीकार्य है यदि A का प्रत्येक L-एकरूप σ ऐसा है कि σs_i= एस_i प्रत्येक के लिए मैं भी बी का एक एकीकृतकर्ता है। स्वीकार्य नियमों के लिए बुनियादी निर्णायक परिणाम भी मापदंडों के साथ नियमों को ले जाते हैं। एक बहु-निष्कर्ष नियम सूत्रों के दो परिमित सेटों की एक जोड़ी (Γ, Δ) है, जिसे इस रूप में लिखा गया है

${\frac {A_{1},\dots ,A_{n}}{B_{1},\dots ,B_{m}}}\qquad {\text{or}}\qquad A_{1},\dots ,A_{n}/B_{1},\dots ,B_{m}.$

ऐसा नियम स्वीकार्य है यदि Γ का प्रत्येक एकीकरण भी Δ से कुछ सूत्र का एक एकीकृतकर्ता है। उदाहरण के लिए, एक तर्क L सुसंगत है यदि वह नियम को स्वीकार करता है

${\frac {\;\bot \;}{}},$

और एक सुपरिंट्यूशनिस्टिक लॉजिक में विच्छेदन संपत्ति है अगर यह नियम को स्वीकार करता है

${\frac {p\lor q}{p,q}}.$

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

${\frac {A_{1},\dots ,A_{n}}{\Box B_{1}\lor \dots \lor \Box B_{m}}}.$

फिर भी, तर्कों को सरल बनाने के लिए बहु-निष्कर्ष नियमों को अक्सर नियोजित किया जा सकता है।

प्रमाण सिद्धांत में, स्वीकार्यता को अक्सर अनुक्रमिक कलन के संदर्भ में माना जाता है, जहां मूल वस्तुएं सूत्र के बजाय अनुक्रम हैं। उदाहरण के लिए, कट-उन्मूलन प्रमेय को यह कहते हुए फिर से लिखा जा सकता है कि कट-फ्री सीक्वेंस कैलकुलस कट नियम को स्वीकार करता है

${\frac {\Gamma \vdash A,\Delta \qquad \Pi ,A\vdash \Lambda }{\Gamma ,\Pi \vdash \Delta ,\Lambda }}.$

(भाषा के दुरुपयोग से, यह भी कभी-कभी कहा जाता है कि (पूर्ण) अनुक्रमिक कलन कट को स्वीकार करता है, जिसका अर्थ है कि इसका कट-मुक्त संस्करण करता है।) हालांकि, अनुक्रमिक गणना में स्वीकार्यता आमतौर पर संबंधित तर्क में स्वीकार्यता के लिए केवल एक सांकेतिक रूप है: कोई भी (कहते हैं) अंतर्ज्ञानवादी तर्क के लिए पूर्ण कलन एक अनुक्रमिक नियम को स्वीकार करता है यदि और केवल अगर IPC उस सूत्र नियम को स्वीकार करता है जिसे हम प्रत्येक अनुक्रम का अनुवाद करके प्राप्त करते हैं $\Gamma \vdash \Delta$ इसके विशिष्ट सूत्र के लिए $\bigwedge \Gamma \to \bigvee \Delta$.

संदर्भ

• W. Blok, D. Pigozzi, Algebraizable logics, Memoirs of the American Mathematical Society 77 (1989), no. 396, 1989.
• A. Chagrov and M. Zakharyaschev, Modal Logic, Oxford Logic Guides vol. 35, Oxford University Press, 1997. ISBN 0-19-853779-4
• P. Cintula and G. Metcalfe, Structural completeness in fuzzy logics, Notre Dame Journal of Formal Logic 50 (2009), no. 2, pp. 153–182. doi:10.1215/00294527-2009-004
• A. I. Citkin, On structurally complete superintuitionistic logics, Soviet Mathematics - Doklady, vol. 19 (1978), pp. 816–819.
• S. Ghilardi, Unification in intuitionistic logic, Journal of Symbolic Logic 64 (1999), no. 2, pp. 859–880. Project Euclid JSTOR
• S. Ghilardi, Best solving modal equations, Annals of Pure and Applied Logic 102 (2000), no. 3, pp. 183–198. doi:10.1016/S0168-0072(99)00032-9
• R. Iemhoff, On the admissible rules of intuitionistic propositional logic, Journal of Symbolic Logic 66 (2001), no. 1, pp. 281–294. Project Euclid JSTOR
• R. Iemhoff, Intermediate logics and Visser's rules, Notre Dame Journal of Formal Logic 46 (2005), no. 1, pp. 65–81. doi:10.1305/ndjfl/1107220674
• R. Iemhoff, On the rules of intermediate logics, Archive for Mathematical Logic, 45 (2006), no. 5, pp. 581–599. doi:10.1007/s00153-006-0320-8
• E. Jeřábek, Admissible rules of modal logics, Journal of Logic and Computation 15 (2005), no. 4, pp. 411–431. doi:10.1093/logcom/exi029
• E. Jeřábek, Complexity of admissible rules, Archive for Mathematical Logic 46 (2007), no. 2, pp. 73–92. doi:10.1007/s00153-006-0028-9
• E. Jeřábek, Independent bases of admissible rules, Logic Journal of the IGPL 16 (2008), no. 3, pp. 249–267. doi:10.1093/jigpal/jzn004
• M. Kracht, Modal Consequence Relations, in: Handbook of Modal Logic (P. Blackburn, J. van Benthem, and F. Wolter, eds.), Studies of Logic and Practical Reasoning vol. 3, Elsevier, 2007, pp. 492–545. ISBN 978-0-444-51690-9
• P. Lorenzen, Einführung in die operative Logik und Mathematik, Grundlehren der mathematischen Wissenschaften vol. 78, Springer–Verlag, 1955.
• G. Mints and A. Kojevnikov, Intuitionistic Frege systems are polynomially equivalent, Zapiski Nauchnyh Seminarov POMI 316 (2004), pp. 129–146. gzipped PS
• T. Prucnal, Structural completeness of Medvedev's propositional calculus, Reports on Mathematical Logic 6 (1976), pp. 103–105.
• T. Prucnal, On two problems of Harvey Friedman, Studia Logica 38 (1979), no. 3, pp. 247–262. doi:10.1007/BF00405383
• P. Rozière, Règles admissibles en calcul propositionnel intuitionniste, Ph.D. thesis, Université de Paris VII, 1992. PDF
• V. V. Rybakov, Admissibility of Logical Inference Rules, Studies in Logic and the Foundations of Mathematics vol. 136, Elsevier, 1997. ISBN 0-444-89505-1
• F. Wolter, M. Zakharyaschev, Undecidability of the unification and admissibility problems for modal and description logics, ACM Transactions on Computational Logic 9 (2008), no. 4, article no. 25. doi:10.1145/1380572.1380574 PDF