अनुमेय नियम

This article is about लॉजिक सिस्टम में अनुमान के नियम. For निर्णय सिद्धांत में अवधारणा, see अनुमेय निर्णय नियम.

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

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

परिभाषाएँ

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

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

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

प्रत्येक संयोजक एफ और सूत्र a₁, ... , a_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,$

जहां Γ = {a₁, ... , a_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 से निपटने के लिए प्रथागत है।

उदाहरण

• मौलिक लॉजिक (सीपीसी) संरचनात्मक रूप से पूर्ण है। वास्तव में, मान लें कि ए/बी गैर-व्युत्पन्न नियम है, और असाइनमेंट v तय करें जैसे v(A) = 1, और v(B) = 0 प्रतिस्थापन σ परिभाषित करें जैसे कि प्रत्येक चर p के लिए, σp = $\top$ यदि v (p) = 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))$

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

• नियम

${\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 में अनुमेय (किन्तु व्युत्पन्न नहीं) है, और यह जीएल में व्युत्पन्न है। चूँकि, K4 में एलR अनुमेय नहीं है। विशेष रूप से, यह सामान्य रूप से सत्य नहीं है कि लॉजिक L में अनुमेय नियम इसके विस्तार में अनुमेय होना चाहिए।

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

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

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

फिर भी, नियमों की अनुमेयता को कई मोडल और सुपरिंट्यूशनिस्टिक लॉजिक्स में निर्णायक माना जाता है। मूलभूत सकर्मक संबंध मोडल लॉजिक्स में अनुमेय नियमों के लिए पहली निर्णय प्रक्रिया व्लादिमीर v. रयबाकोव द्वारा 'नियमों के कम रूप' का उपयोग करके बनाई गई थी। चर p₀, ... , p_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}$ या तो रिक्त है, या तार्किक निषेध है | प्रत्येक नियम 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 या आईपीसी का विस्तार) मोडल और सुपरिंट्यूशनिस्टिक लॉजिक्स के शक्तिशाली (अनंत) वर्ग पर प्रयुक्त होता है, जिसमें उदाहरण S4.1, S4.2, S4.3, केसी, T_k (साथ ही उपर्युक्त लॉजिक्स आईपीसी, K4, S4, GL, Grz) निर्णायक होने के अतिरिक्त, अनुमेयता समस्या में अपेक्षाकृत उच्च कम्प्यूटेशनल जटिलता सिद्धांत है | यहां तक ​​​​कि सरल लॉजिक्स में भी: मूलभूत सकर्मक लॉजिक्स आईपीसी, K4, S4, GL, Grz में नियमों की अनुमेयता नेक्स्प-पूर्ण है। यह इन लॉजिक्स में व्युत्पन्नता समस्या (नियमों या सूत्रों के लिए) के विपरीत होना चाहिए | जो पीएसपीएसीई-पूर्ण है।

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

प्रोपोज़िशनल लॉजिक्स में अनुमेयता मोडल बीजगणित या हेटिंग बीजगणित के समीकरण सिद्धांत में एकीकरण से निकटता से संबंधित है। सम्बन्ध घिलार्डी (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 का एमजीयू है। क्रिपके सिमेंटिक्स फाइनिट मॉडल प्रॉपर्t के साथ सकर्मक मोडल और सुपरिंट्यूशनिस्टिक लॉजिक्स में, कोई प्रोजेक्टिव सूत्रों को सिमेंटिक रूप से चित्रित कर सकता है | जिनके परिमित एल-मॉडल के समुच्चय में 'Xटेंशन प्रॉपर्t' है। यदि एम एक रूट R के साथ परिमित क्रिपके एल-मॉडल है जिसका क्लस्टर सिंगलटन (गणित) है, और सूत्र ए R को छोड़कर एम के सभी बिंदुओं पर रखता है, तो हम R में चर के मूल्यांकन को बदल सकते हैं | जिससे बना सकें R पर भी सच है। इसके अतिरिक्त, प्रमाण किसी दिए गए प्रोजेक्टिव सूत्र ए के लिए एमजीयू का स्पष्ट निर्माण प्रदान करता है।

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

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

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

$P\,|\!\!\!\sim _{L}B$ यदि और केवल यदि $P\vdash _{L}B$

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

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

अनुमेय नियमों के आधार

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

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

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

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

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

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

• विज़र के नियम

${\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$

आईपीसी या केसी में अनुमेय नियमों का आधार हैं ।

• नियम

${\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 का 'रिफ्लेक्सिव टाइट पूर्ववर्ती', यदि डब्ल्यू में प्रत्येक Y के लिए: t R Y यदि और केवल यदि t = Y या X में कुछ X के लिए: X = Y या X R Y, है |
• 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, आनुवंशिक रूप से संरचनात्मक रूप से पूर्ण हैं। सिटकिन और रयबाकोव द्वारा क्रमशः आनुवंशिक रूप से संरचनात्मक रूप से पूर्ण सुपरिंट्यूशनिस्टिक और सकर्मक मोडल लॉजिक्स का पूरा विवरण दिया गया था। अर्थात्, अधीक्षणवादी लॉजिक आनुवंशिक रूप से संरचनात्मक रूप से पूर्ण होता है यदि और केवल यदि यह पांच कृपके फ्रेमों में से किसी में मान्य नहीं है |

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

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

प्रकार

मापदंड वाला नियम फॉर्म का नियम है |

${\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, में विभाजित हैं और मापदंड s_i. नियम L-अनुमेय है | यदि A का प्रत्येक L-एकरूप σ ऐसा है कि σs_i= s_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 }}.$

(भाषा से, यह भी कभी-कभी कहा जाता है कि (पूर्ण) अनुक्रमिक कलन कट को अनुमेय करता है | जिसका अर्थ है कि इसका कट-मुक्त संस्करण करता है।) चूँकि, अनुक्रमिक गणना में अनुमेयता सामान्यतः संबंधित लॉजिक में अनुमेयता के लिए केवल सांकेतिक रूप है | कोई भी (कहते हैं) अंतर्ज्ञानवादी लॉजिक के लिए पूर्ण कलन अनुक्रमिक नियम को अनुमेय करता है | यदि और केवल यदि आईपीसी उस सूत्र नियम को अनुमेय करता है | जिसे हम प्रत्येक अनुक्रम $\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