क्रिपके शब्दार्थ

क्रिपके अर्थ विज्ञान (रिलेशनल सेमेन्टिक्स या फ्रेम सेमेन्टिक्स के रूप में भी जाना जाता है, और अक्सर संभावित विश्व सेमेन्टिक्स के साथ भ्रमित होता है) 1950 के दशक के अंत और 1960 के दशक की शुरुआत में शाऊल क्रिपके और आंद्रे जोयाल द्वारा बनाई गई गैर-शास्त्रीय तर्क प्रणालियों के लिए औपचारिक शब्दार्थ है। इसकी कल्पना सबसे पहले मोडल तर्क के लिए की गई थी, और बाद में इसे अंतर्ज्ञानवादी तर्क और अन्य गैर-शास्त्रीय प्रणालियों के लिए अनुकूलित किया गया। क्रिप्के शब्दार्थ का विकास गैर-शास्त्रीय तर्कशास्त्र के सिद्धांत में सफलता थी, क्योंकि ऐसे तर्कशास्त्र का मॉडल सिद्धांत क्रिपके से पहले लगभग अस्तित्वहीन था (बीजगणितीय शब्दार्थ अस्तित्व में थे, लेकिन उन्हें 'छिपे हुए वाक्यविन्यास' माना जाता था)।

मोडल लॉजिक का शब्दार्थ

Main article: Modal logic

प्रस्तावात्मक मोडल लॉजिक की भाषा में प्रस्तावात्मक चरों का गणनीय सेट, सत्य-कार्यात्मक तार्किक संयोजक का सेट होता है (इस लेख में) $\to$ और $\neg$), और मोडल ऑपरेटर $\Box$ ( अनिवार्य रूप से )। मोडल ऑपरेटर $\Diamond$ (संभवतः) (शास्त्रीय रूप से) द्वैत (गणित)#तर्क और समुच्चय सिद्धांत में द्वैत है $\Box$ और आवश्यकता के संदर्भ में शास्त्रीय मोडल तर्क इस प्रकार है: $\Diamond A:=\neg \Box \neg A$ (संभवतः ए को ए के समकक्ष परिभाषित किया गया है, जरूरी नहीं कि ए नहीं)।

बुनियादी परिभाषाएँ

क्रिपके फ्रेम या मोडल फ्रेम जोड़ी है $\langle W,R\rangle$, जहां W (संभवतः खाली) सेट है, और R, W तत्वों पर द्विआधारी संबंध है

W को नोड्स या वर्ल्ड कहा जाता है, और R को अभिगम्यता संबंध के रूप में जाना जाता है।

क्रिपके मॉडल ट्रिपल है $\langle W,R,\Vdash \rangle$, कहाँ

$\langle W,R\rangle$ क्रिपके फ्रेम है, और $\Vdash$ W के नोड्स और मोडल फ़ार्मुलों के बीच संबंध है, जैसे कि सभी w ∈W और मोडल फ़ार्मुलों A और B के लिए:

• $w\Vdash \neg A$ अगर और केवल अगर $w\nVdash A$,
• $w\Vdash A\to B$ अगर और केवल अगर $w\nVdash A$ या $w\Vdash B$,
• $w\Vdash \Box A$ अगर और केवल अगर $u\Vdash A$ सभी के लिए $u$ ऐसा है कि $w\;R\;u$.

हम पढ़ते है $w\Vdash A$ जैसे “डब्ल्यू संतुष्ट करता है।” ए", "ए डब्ल्यू में संतुष्ट है", या "डब्ल्यू बल ए"। रिश्ता $\Vdash$ कहा जाता है

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

सूत्र ए 'मान्य' है:

• प्रतिमा $\langle W,R,\Vdash \rangle$, अगर $w\Vdash A$ सभी w∈W के लिए,
• चौखटा $\langle W,R\rangle$, यदि यह वैध है $\langle W,R,\Vdash \rangle$ के सभी संभावित विकल्पों के लिए $\Vdash$,
• फ़्रेम या मॉडल का वर्ग सी, यदि यह सी के प्रत्येक सदस्य में मान्य है।

हम Thm(C) को उन सभी सूत्रों के समुच्चय के रूप में परिभाषित करते हैं जो मान्य हैं

C. इसके विपरीत, यदि X सूत्रों का सेट है, तो Mod(X) को होने दें सभी फ़्रेमों का वर्ग जो X से प्रत्येक सूत्र को मान्य करता है।

मोडल लॉजिक (यानी, सूत्रों का सेट) एल ' दृढ़ता ' के साथ है फ़्रेम C के वर्ग के संबंध में, यदि L ⊆ Thm(C)। एल है 'पूर्णता (तर्क)' wrt C यदि L ⊇ Thm(C)।

पत्राचार और पूर्णता

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

क्रिपके फ्रेम के किसी भी वर्ग सी के लिए, Thm(C) सामान्य मोडल लॉजिक है (विशेष रूप से, न्यूनतम सामान्य मोडल लॉजिक, K के प्रमेय, प्रत्येक क्रिपके मॉडल में मान्य हैं)। हालाँकि, इसका विपरीत सामान्य रूप से लागू नहीं होता है: जबकि अध्ययन किए गए अधिकांश मोडल सिस्टम सरल स्थितियों द्वारा वर्णित फ़्रेमों के वर्गों से पूर्ण हैं, क्रिपके अपूर्ण सामान्य मोडल लॉजिक्स मौजूद हैं। ऐसी प्रणाली का स्वाभाविक उदाहरण जापरिडेज़ का बहुविध तर्क है।

सामान्य मोडल लॉजिक L, फ़्रेम C के वर्ग से 'संगत' होता है, यदि C = Mod(L)। दूसरे शब्दों में, C फ़्रेमों का सबसे बड़ा वर्ग है, जैसे कि L ध्वनि wrt C है। इसका अर्थ यह है कि L क्रिप्के पूर्ण है यदि और केवल यदि यह अपने संबंधित वर्ग का पूर्ण है।

स्कीम 'टी' पर विचार करें: $\Box A\to A$.

टी किसी भी प्रतिवर्ती संबंध फ्रेम में मान्य है $\langle W,R\rangle$: अगर $w\Vdash \Box A$, तब $w\Vdash A$ चूंकि डब्ल्यू आर डब्ल्यू। दूसरी ओर, फ्रेम जो

मान्य 'टी' को रिफ्लेक्सिव होना चाहिए: डब्ल्यू ∈ डब्ल्यू को ठीक करें, और प्रस्तावित चर p की संतुष्टि को इस प्रकार परिभाषित करें:

$u\Vdash p$ यदि और केवल यदि आप। तब $w\Vdash \Box p$, इस प्रकार $w\Vdash p$ T द्वारा, जिसका अर्थ है w R w की परिभाषा का उपयोग करना $\Vdash$. टी रिफ्लेक्सिव के वर्ग से मेल खाता है क्रिपके फ्रेम।

संबंधित वर्ग को चिह्नित करना अक्सर बहुत आसान होता है

एल की तुलना में इसकी पूर्णता साबित करने के लिए, इस प्रकार पत्राचार के रूप में कार्य करता है

पूर्णता प्रमाण के लिए मार्गदर्शिका. पत्राचार का प्रयोग दिखाने के लिए भी किया जाता है

मोडल लॉजिक्स की अपूर्णता: मान लीजिए

एल₁⊆एल₂ ये सामान्य मोडल लॉजिक हैं फ़्रेम के समान वर्ग के अनुरूप, लेकिन L₁ नहीं करता

एल के सभी प्रमेय सिद्ध करें₂. फिर एल₁ है

क्रिपके अधूरा. उदाहरण के लिए, स्कीमा $\Box (A\leftrightarrow \Box A)\to \Box A$ यह अधूरा तर्क उत्पन्न करता है

जीएल के समान फ्रेम के वर्ग से मेल खाता है (अर्थात् सकर्मक और

बातचीत अच्छी तरह से स्थापित फ्रेम), लेकिन जीएल-टॉटोलॉजी को साबित नहीं करती है $\Box A\to \Box \Box A$.

सामान्य मोडल अभिगृहीत स्कीमाटा

निम्न तालिका सामान्य मोडल स्वयंसिद्धों को उनके संबंधित वर्गों के साथ सूचीबद्ध करती है। स्वयंसिद्धों का नामकरण अक्सर भिन्न होता है; यहाँ, स्वयंसिद्ध K का नाम शाऊल क्रिपके के नाम पर रखा गया है; ्सिओम टी का नाम एपिस्टेमिक मोडल लॉजिक#ज्ञानमीमांसीय तर्क में ज्ञान या सत्य ्सिओम के नाम पर रखा गया है; ्सिओम डी का नाम डोंटिक तर्क के नाम पर रखा गया है; ्सिओम बी का नाम एल. ई. जे. ब्रौवर के नाम पर रखा गया है; और अभिगृहीत 4 और 5 का नाम सी. आई. लुईस की प्रतीकात्मक तर्क संख्या के आधार पर रखा गया है।

Name	Axiom	Frame condition
K	$\Box (A\to B)\to (\Box A\to \Box B)$	holds true for any frames
T	$\Box A\to A$	reflexive: $w\,R\,w$
-	$\Box \Box A\to \Box A$	dense: $w\,R\,u\Rightarrow \exists v\,(w\,R\,v\land v\,R\,u)$
4	$\Box A\to \Box \Box A$	transitive: $w\,R\,v\wedge v\,R\,u\Rightarrow w\,R\,u$
D	$\Box A\to \Diamond A$ or $\Diamond \top$ or $\neg \Box \bot$	serial: $\forall w\,\exists v\,(w\,R\,v)$
B	$A\to \Box \Diamond A$ or $\Diamond \Box A\to A$	symmetric : $w\,R\,v\Rightarrow v\,R\,w$
5	$\Diamond A\to \Box \Diamond A$	Euclidean: $w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v$
GL	$\Box (\Box A\to A)\to \Box A$	R transitive, R−1 well-founded
Grz	$\Box (\Box (A\to \Box A)\to A)\to A$	R reflexive and transitive, R−1−Id well-founded
H	$\Box (\Box A\to B)\lor \Box (\Box B\to A)$	$w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v\lor v\,R\,u$
M	$\Box \Diamond A\to \Diamond \Box A$	(a complicated second-order property)
G	$\Diamond \Box A\to \Box \Diamond A$	convergent: $w\,R\,u\land w\,R\,v\Rightarrow \exists x\,(u\,R\,x\land v\,R\,x)$
-	$A\to \Box A$	discrete: $w\,R\,v\Rightarrow w=v$
-	$\Diamond A\to \Box A$	partial function: $w\,R\,u\land w\,R\,v\Rightarrow u=v$
-	$\Diamond A\leftrightarrow \Box A$	function: $\forall w\,\exists !u\,w\,R\,u$ ($\exists !$ is the uniqueness quantification)
-	$\Box A$ or $\Box \bot$	empty: $\forall w\,\forall u\,\neg (w\,R\,u)$

Axiom K के रूप में भी पुनर्लेखन किया जा सकता है $\Box [(A\to B)\land A]\to \Box B$, जो तार्किक रूप से हर संभव दुनिया में अनुमान के नियम के रूप में मूड सेट करना को स्थापित करता है।

ध्यान दें कि अभिगृहीत D के लिए, $\Diamond A$ निहितार्थ का तात्पर्य है $\Diamond \top$, जिसका अर्थ है कि मॉडल में प्रत्येक संभावित दुनिया के लिए, उसमें से हमेशा कम से कम संभावित दुनिया पहुंच योग्य होती है (जो स्वयं हो सकती है)। यह निहितार्थ $\Diamond A\rightarrow \Diamond \top$ क्वांटिफ़ायर (तर्क)#मात्रा निर्धारण की सीमा द्वारा अंतर्निहित निहितार्थ के समान है।

सामान्य मोडल सिस्टम

The following table lists several common normal modal systems. Frame conditions for some of the systems were simplified: the logics are sound and complete with respect to the frame classes given in the table, but they may correspond to a larger class of frames.

Name	Axioms	Frame condition
K	—	all frames
T	T	reflexive
K4	4	transitive
S4	T, 4	preorder
S5	T, 5 or D, B, 4	equivalence relation
S4.3	T, 4, H	total preorder
S4.1	T, 4, M	preorder, $\forall w\,\exists u\,(w\,R\,u\land \forall v\,(u\,R\,v\Rightarrow u=v))$
S4.2	T, 4, G	directed preorder
GL, K4W	GL or 4, GL	finite strict partial order
Grz, S4Grz	Grz or T, 4, Grz	finite partial order
D	D	serial
D45	D, 4, 5	transitive, serial, and Euclidean

विहित मॉडल

किसी भी सामान्य मोडल लॉजिक के लिए, एल, क्रिप्के मॉडल (जिसे 'कैनोनिकल मॉडल' कहा जाता है) का निर्माण किया जा सकता है जो सटीक रूप से गैर-प्रमेयों का खंडन करता है

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

बीजगणित में लिंडेनबाम-टार्स्की बीजगणित निर्माण के समान भूमिका

शब्दार्थ।

सूत्रों का सेट एल-संगत है यदि एल और मोडस पोनेंस के प्रमेयों का उपयोग करके इसमें कोई विरोधाभास नहीं निकाला जा सकता है। अधिकतम एल-संगत सेट ( एल-एमसीएस

संक्षेप में) एल-संगत सेट है जिसमें कोई उचित एल-संगत सुपरसेट नहीं है।

एल का 'कैनोनिकल मॉडल' क्रिपके मॉडल है

$\langle W,R,\Vdash \rangle$, जहां W सभी L-MCS का समुच्चय है,

और संबंध आर और $\Vdash$ निम्नानुसार हैं:

$X\;R\;Y$ प्रत्येक सूत्र के लिए यदि और केवल यदि $A$, अगर $\Box A\in X$ तब $A\in Y$,

$X\Vdash A$ अगर और केवल अगर $A\in X$.

कैनोनिकल मॉडल एल का मॉडल है, जैसा कि प्रत्येक एल-एमसीएस में होता है

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

विहित मॉडलों का मुख्य अनुप्रयोग पूर्णता प्रमाण हैं। 'K' के विहित मॉडल के गुण तुरंत सभी क्रिपके फ़्रेमों के वर्ग के संबंध में 'K' की पूर्णता दर्शाते हैं।

यह तर्क मनमाने ढंग से एल के लिए काम नहीं करता है, क्योंकि इस बात की कोई गारंटी नहीं है कि कैनोनिकल मॉडल का अंतर्निहित फ्रेम एल की फ्रेम शर्तों को पूरा करता है।

हम कहते हैं कि सूत्र या सूत्रों का सेट ्स 'विहित' है क्रिपके फ्रेम की संपत्ति पी के संबंध में, यदि

• X हर उस फ़्रेम में मान्य है जो P को संतुष्ट करता है,
• किसी भी सामान्य मोडल लॉजिक एल के लिए जिसमें ्स शामिल है, एल के कैनोनिकल मॉडल का अंतर्निहित फ्रेम पी को संतुष्ट करता है।

सूत्रों के विहित सेटों का संघ स्वयं विहित है।

पिछली चर्चा से यह पता चलता है कि कोई भी तर्क स्वयंसिद्ध है सूत्रों का विहित सेट क्रिप्के पूर्ण है, और

सघनता प्रमेय.

अभिगृहीत T, 4, D, B, 5, H, G (और इस प्रकार उनमें से कोई भी संयोजन) विहित है। GL और Grz नहीं हैं

विहित, क्योंकि वे सघन नहीं हैं। स्वयंसिद्ध M अपने आप में है

विहित नहीं (गोल्डब्लैट, 1991), लेकिन संयुक्त तर्क 'एस4.1' (में) वास्तव में, यहां तक ​​कि 'K4.1') भी विहित है।

सामान्य तौर पर, यह निर्णय की समस्या है कि कोई दिया गया स्वयंसिद्ध है या नहीं विहित. हम अच्छी पर्याप्त स्थिति जानते हैं: हेनरिक साहल्कविस्ट ने सूत्रों के व्यापक वर्ग की पहचान की (जिसे अब कहा जाता है)। साहलक्विस्ट सूत्र) जैसे कि

• सहलक्विस्ट सूत्र विहित है,
• सहलक्विस्ट सूत्र के अनुरूप फ़्रेमों का वर्ग प्रथम-क्रम तर्क है|प्रथम-क्रम निश्चित है,
• एल्गोरिदम है जो किसी दिए गए साहलक्विस्ट सूत्र के अनुरूप फ्रेम स्थिति की गणना करता है।

यह शक्तिशाली मानदंड है: उदाहरण के लिए, सभी स्वयंसिद्ध विहित के रूप में ऊपर सूचीबद्ध सहलक्विस्ट सूत्र (समकक्ष) हैं।

परिमित मॉडल संपत्ति

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

धारणा निर्णयात्मकता (तर्क) प्रश्न है: यह से अनुसरण करता है पोस्ट का प्रमेय कि पुनरावर्ती स्वयंसिद्ध मोडल लॉजिक एल

जिसमें एफएमपी है वह निर्णय लेने योग्य है, बशर्ते यह निर्णय लेने योग्य हो कि क्या दिया गया है

परिमित फ़्रेम L का मॉडल है। विशेष रूप से, प्रत्येक परिमित रूप से

एफएमपी के साथ स्वयंसिद्ध तर्क निर्णय लेने योग्य है।

किसी दिए गए तर्क के लिए एफएमपी स्थापित करने की विभिन्न विधियाँ हैं।

विहित मॉडल निर्माण का परिशोधन और विस्तार अक्सर

1. मॉडल निर्माण या जैसे उपकरणों का उपयोग करके काम करें
2. मॉडल निर्माण. और संभावना के रूप में,

कट-उन्मूलन|कट-मुक्त पर आधारित पूर्णता प्रमाण अनुक्रमिक कलन आमतौर पर परिमित मॉडल उत्पन्न करते हैं सीधे.

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

ऊपर) एफएमपी है।

कुछ मामलों में, हम क्रिपके तर्क की पूर्णता साबित करने के लिए एफएमपी का उपयोग कर सकते हैं:

प्रत्येक सामान्य मोडल लॉजिक वर्ग के संबंध में पूर्ण है

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

S4.3 के प्रत्येक सामान्य ्सटेंशन में FMP है, और क्रिपके है पूरा।

मल्टीमॉडल लॉजिक्स

See also: Multimodal logic

क्रिपके शब्दार्थ में तर्कशास्त्र का सीधा सामान्यीकरण है से अधिक तौर-तरीके. भाषा के लिए क्रिपके फ्रेम

$\{\Box _{i}\mid \,i\in I\}$ इसके आवश्यकता ऑपरेटरों के सेट के रूप में

इसमें द्विआधारी संबंधों से सुसज्जित गैर-रिक्त सेट डब्ल्यू शामिल है आर_iप्रत्येक i∈I के लिए। a की परिभाषा संतुष्टि संबंध को इस प्रकार संशोधित किया गया है:

$w\Vdash \Box _{i}A$ अगर और केवल अगर $\forall u\,(w\;R_{i}\;u\Rightarrow u\Vdash A).$

टिम कार्लसन द्वारा खोजे गए सरलीकृत शब्दार्थ का उपयोग अक्सर किया जाता है

पॉलीमॉडल प्रयोज्यता तर्क । कार्लसन मॉडल संरचना है

$\langle W,R,\{D_{i}\}_{i\in I},\Vdash \rangle$

ल अभिगम्यता संबंध आर और उपसमुच्चय के साथ डी_i⊆ प्रत्येक तौर-तरीके के लिए डब्ल्यू। संतुष्टि है

के रूप में परिभाषित

$w\Vdash \Box _{i}A$ अगर और केवल अगर $\forall u\in D_{i}\,(w\;R\;u\Rightarrow u\Vdash A).$

कार्लसन मॉडल को कल्पना करना और उसके साथ काम करना सामान्य से अधिक आसान है

पॉलीमॉडल क्रिपके मॉडल; हालाँकि, क्रिप्के पूर्ण बहुरूपी हैं

कार्लसन के तर्क अधूरे हैं।

अंतर्ज्ञानवादी तर्क का शब्दार्थ

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

संतुष्टि की परिभाषा.

अंतर्ज्ञानवादी क्रिपके मॉडल ट्रिपल है

$\langle W,\leq ,\Vdash \rangle$, कहाँ $\langle W,\leq \rangle$ पूर्व-आदेशित क्रिपके फ्रेम है, और $\Vdash$ निम्नलिखित शर्तों को पूरा करता है:

• यदि p प्रस्तावात्मक चर है, $w\leq u$, और $w\Vdash p$, तब $u\Vdash p$ (स्थिरता की स्थिति (cf. रसता)),
• $w\Vdash A\land B$ अगर और केवल अगर $w\Vdash A$ और $w\Vdash B$,
• $w\Vdash A\lor B$ अगर और केवल अगर $w\Vdash A$ या $w\Vdash B$,
• $w\Vdash A\to B$ यदि और केवल यदि सभी के लिए $u\geq w$, $u\Vdash A$ तात्पर्य $u\Vdash B$,
• नहीं $w\Vdash \bot$.

A, ¬A के निषेध को A → ⊥ के संक्षिप्त रूप के रूप में परिभाषित किया जा सकता है। यदि आप सभी के लिए ऐसा है कि w ≤ u, नहीं u ⊩ A, तो w ⊩ A → ⊥ शून्य सत्य है, इसलिए w ⊩ ¬ ।

अंतर्ज्ञानवादी तर्क अपने क्रिपके के संबंध में ध्वनि और पूर्ण है

शब्दार्थ, और इसमें परिमित मॉडल गुण है।

अंतर्ज्ञानवादी प्रथम-क्रम तर्क

मान लीजिए L प्रथम-क्रम तर्क|प्रथम-क्रम भाषा है। ए क्रिपके L का मॉडल त्रिगुण है $\langle W,\leq ,\{M_{w}\}_{w\in W}\rangle$, कहाँ $\langle W,\leq \rangle$ अंतर्ज्ञानवादी क्रिपके फ्रेम है, एम_w है

(शास्त्रीय) प्रत्येक नोड w∈W, और के लिए एल-संरचना जब भी u ≤ v होता है तो निम्नलिखित संगतता स्थितियाँ लागू होती हैं:

• एम का डोमेन_uएम के डोमेन में शामिल है_v,
• एम में फ़ंक्शन प्रतीकों की प्राप्ति_uऔर एम_vएम के तत्वों पर सहमति_u,
• प्रत्येक n-ary विधेय P और तत्वों a के लिए₁,...,ए_n∈एम_u: यदि पी(ए₁,...,ए_n) एम में रखता है_u, तो यह एम में रहता है_v.

एम के तत्वों द्वारा चरों का मूल्यांकन ई दिया गया है_w, हम

संतुष्टि संबंध को परिभाषित करें $w\Vdash A[e]$:

• $w\Vdash P(t_{1},\dots ,t_{n})[e]$ अगर और केवल अगर $P(t_{1}[e],\dots ,t_{n}[e])$ एम में रखता है_w,
• $w\Vdash (A\land B)[e]$ अगर और केवल अगर $w\Vdash A[e]$ और $w\Vdash B[e]$,
• $w\Vdash (A\lor B)[e]$ अगर और केवल अगर $w\Vdash A[e]$ या $w\Vdash B[e]$,
• $w\Vdash (A\to B)[e]$ यदि और केवल यदि सभी के लिए $u\geq w$, $u\Vdash A[e]$ तात्पर्य $u\Vdash B[e]$,
• नहीं $w\Vdash \bot [e]$,
• $w\Vdash (\exists x\,A)[e]$ यदि और केवल यदि कोई मौजूद है $a\in M_{w}$ ऐसा है कि $w\Vdash A[e(x\to a)]$,
• $w\Vdash (\forall x\,A)[e]$ यदि और केवल यदि प्रत्येक के लिए $u\geq w$ और हर $a\in M_{u}$ , $u\Vdash A[e(x\to a)]$.

यहां e(x→a) वह मूल्यांकन है जो x देता है मान a, और अन्यथा e से सहमत है।

इसमें थोड़ी अलग औपचारिकता देखें।

क्रिपके-जॉयल शब्दार्थ

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

मॉडल निर्माण

जैसा कि शास्त्रीय मॉडल सिद्धांत में होता है, इसके लिए विधियाँ हैं अन्य मॉडलों से नया क्रिपके मॉडल बनाना।

क्रिपके शब्दार्थ में प्राकृतिक समरूपता कहलाती है

पी-मॉर्फिज्म (जो छद्म-एपिमोर्फिज्म का संक्षिप्त रूप है, लेकिन बाद वाले शब्द का प्रयोग शायद ही कभी किया जाता है)। क्रिपके फ्रेम का पी-रूपवाद

$\langle W,R\rangle$ और $\langle W',R'\rangle$ मैपिंग है $f\colon W\to W'$ ऐसा है कि

• एफ पहुंच संबंध को बरकरार रखता है, यानी, यू आर वी का तात्पर्य एफ (यू) आर 'एफ (वी) है,
• जब भी f(u) R' v' होता है, तो v∈W होता है जैसे कि uRv और f(v)=v'।

क्रिपके मॉडल का पी-रूपवाद $\langle W,R,\Vdash \rangle$ और $\langle W',R',\Vdash '\rangle$ उनका पी-रूपवाद है अंतर्निहित फ़्रेम $f\colon W\to W'$, कौन

संतुष्ट

$w\Vdash p$ अगर और केवल अगर $f(w)\Vdash 'p$, किसी भी प्रस्तावित चर पी के लिए।

पी-मॉर्फिज्म विशेष प्रकार के द्विसिमुलेशन हैं। सामान्य तौर पर, ए

फ़्रेमों के बीच 'द्विसिमुलेशन' $\langle W,R\rangle$ और $\langle W',R'\rangle$ रिश्ता है B ⊆ W × W', जो संतुष्ट करता है

निम्नलिखित "ज़िग-ज़ैग" संपत्ति:

• यदि u ‍B u' और u ‍R ‍v', तो ‍‍‍‍‍ ∈ ‍W' का ‍अस्तित्व ‍है जैसे ‍‍‍‍‍‍‍‍‍‍‍‍‍‍‍‍‍‍‍‍‍‍‍‍‍
• यदि u B u' और u'R'v', तो v∈W का अस्तित्व इस प्रकार है कि vBv' और uRv।

फोर्सिंग को संरक्षित करने के लिए मॉडलों का द्विसिमुलेशन अतिरिक्त रूप से आवश्यक है

परमाणु सूत्रों की:

यदि w B w', तो $w\Vdash p$ अगर और केवल अगर $w'\Vdash 'p$, किसी भी प्रस्तावित चर पी के लिए।

इस परिभाषा से जो मुख्य गुण निकलता है वह है मॉडलों के द्विसिमुलेशन (इसलिए पी-मॉर्फिज्म भी) संरक्षित करते हैं

सभी सूत्रों की संतुष्टि, न कि केवल प्रस्तावात्मक चर।

हम क्रिपके मॉडल को पेड़ (ग्राफ़ सिद्धांत) में बदल सकते हैं

'उतारना'। मॉडल दिया $\langle W,R,\Vdash \rangle$ और निश्चित

नोड डब्ल्यू₀∈ डब्ल्यू, हम मॉडल को परिभाषित करते हैं

$\langle W',R',\Vdash '\rangle$, जहां W' है सभी परिमित अनुक्रमों का सेट

$s=\langle w_{0},w_{1},\dots ,w_{n}\rangle$ ऐसा

वह डब्ल्यू_iआर डब्ल्यू_i+1सभी के लिए

मैं < n, और $s\Vdash p$ अगर और केवल अगर $w_{n}\Vdash p$ प्रस्तावात्मक चर के लिए

पी। अभिगम्यता संबंध R' की परिभाषा बदलता रहता है; सबसे सरल मामले में हम डालते हैं

$\langle w_{0},w_{1},\dots ,w_{n}\rangle \;R'\;\langle w_{0},w_{1},\dots ,w_{n},w_{n+1}\rangle$,

लेकिन कई अनुप्रयोगों को रिफ्लेक्सिव और/या ट्रांजिटिव क्लोजर की आवश्यकता होती है

यह संबंध, या इसी तरह के संशोधन।

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

उपसूत्र लेने के अंतर्गत सूत्र बंद हो गए। ए का ्स-निस्पंदन नमूना $\langle W,R,\Vdash \rangle$ डब्ल्यू से मॉडल तक मैपिंग एफ है $\langle W',R',\Vdash '\rangle$ ऐसा है कि

• एफ अनुमान है,
• एफ पहुंच संबंध को बरकरार रखता है, और (दोनों दिशाओं में) चर पी ∈ ्स की संतुष्टि,
• यदि f(u) R'f(v) और $u\Vdash \Box A$, कहाँ $\Box A\in X$, तब $v\Vdash A$.

इससे यह निष्कर्ष निकलता है कि f सभी सूत्रों की संतुष्टि को सुरक्षित रखता है

X. विशिष्ट अनुप्रयोगों में, हम f को प्रक्षेपण के रूप में लेते हैं

संबंध पर W के भागफल सेट पर

यू ≡_Xv यदि और केवल यदि सभी A∈X के लिए, $u\Vdash A$ अगर और केवल अगर $v\Vdash A$.

जैसे कि सुलझने के मामले में, पहुंच की परिभाषा

भागफल पर संबंध भिन्न होता है।

सामान्य फ़्रेम शब्दार्थ

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

कंप्यूटर विज्ञान अनुप्रयोग

Main articles: Kripke structure, state transition system, and model checking

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

इतिहास और शब्दावली

इसी तरह का कार्य जो क्रिपके की क्रांतिकारी अर्थ संबंधी सफलताओं से पहले का था:

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

यह भी देखें

• अलेक्जेंडर टोपोलॉजी
• सामान्य मोडल लॉजिक
• द्वि-आयामीवाद
• प्रेरण_पहेलियाँ#मैला_बच्चे_पहेली

टिप्पणियाँ

a^ After Andrzej Grzegorczyk.

संदर्भ

• Blackburn, P.; de Rijke, M.; Venema, Yde (2002). Modal Logic. Cambridge University Press. ISBN 978-1-316-10195-7.
• Bull, Robert A.; Segerberg, K. (2012) [1984]. "Basic Modal Logic". In Gabbay, D.M.; Guenthner, F. (eds.). Extensions of Classical Logic. Handbook of Philosophical Logic. Vol. 2. Springer. pp. 1–88. ISBN 978-94-009-6259-0.
• Chagrov, A.; Zakharyaschev, M. (1997). Modal Logic. Clarendon Press. ISBN 978-0-19-853779-3.
• Dummett, Michael A. E. (2000). Elements of Intuitionism (2nd ed.). Clarendon Press. ISBN 978-0-19-850524-2.
• Fitting, Melvin (1969). Intuitionistic Logic, Model Theory and Forcing. North-Holland. ISBN 978-0-444-53418-7.
• Goldblatt, Robert (2006). "Mathematical Modal Logic: a View of its Evolution" (PDF). In Gabbay, Dov M.; Woods, John (eds.). Logic and the Modalities in the Twentieth Century (PDF). Handbook of the History of Logic. Vol. 7. Elsevier. pp. 1–98. ISBN 978-0-08-046303-2.
• Cresswell, M.J.; Hughes, G.E. (2012) [1996]. A New Introduction to Modal Logic. Routledge. ISBN 978-1-134-80028-5.
• Mac Lane, Saunders; Moerdijk, Ieke (2012) [1991]. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer. ISBN 978-1-4612-0927-0.
• van Dalen, Dirk (2013) [1986]. "Intuitionistic Logic". In Gabbay, Dov M.; Guenthner, Franz (eds.). Alternatives to Classical Logic. Handbook of Philosophical Logic. Vol. 3. Springer. pp. 225–339. ISBN 978-94-009-5203-4.

बाहरी संबंध

• Garson, James. "Modal Logic". The Stanford Encyclopedia of Philosophy.
• Moschovakis, Joan (2018). "Intuitionistic Logic". Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University.
• Detlovs, V.; Podnieks, K. "4.4 Constructive Propositional Logic — Kripke Semantics". Introduction to Mathematical Logic. University of Latvia. N.B: Constructive = intuitionistic.
• Burgess, John P. "Kripke Models". Archived from the original on 2004-10-20.
• "Kripke models", Encyclopedia of Mathematics, EMS Press, 2001 [1994]