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

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

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

Main article: मॉडल लॉजिक

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

$A$", "$A$w में संतुष्ट है", या "w बल $A$"। सम्बन्ध $\Vdash$ कहा जाता है संतुष्टि संबंध, मूल्यांकन, या बल (गणित) संबंध। संतुष्टि संबंध विशिष्ट रूप से इसके द्वारा निर्धारित होता है

प्रस्तावित वेरिएबल पर मूल्य.

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

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

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

एक मोडल लॉजिक (अर्थात , सूत्रों का एक समुच्चय) L फ्रेम C के एक वर्ग के संबंध में सही है, यदि L ⊆ Thm(C)। यदि L ⊇ Thm(C) है तो L, C के संबंध में पूर्ण है।

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

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

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

अतः क्रिपके अपूर्ण सामान्य मोडल लॉजिक्स उपस्तिथ हैं। ऐसी प्रणाली का स्वाभाविक उदाहरण जापरिडेज़ का बहुविध तर्क है।

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

स्कीम T पर विचार करें :$\Box A\to A$ T किसी भी प्रतिवर्ती संबंध फ्रेम $\langle W,R\rangle$ में मान्य है यदि $w\Vdash \Box A$ है तो $w\Vdash A$ क्योंकि w R w। दूसरी ओर, एक फ्रेम जो T को मान्य करता है उसे रिफ्लेक्सिव होना चाहिए: w ∈ w को ठीक करें, और एक प्रस्तावित वेरिएबल p की संतुष्टि को निम्नानुसार परिभाषित करें: $u\Vdash p$ यदि और केवल यदि w R u । फिर $w\Vdash \Box p$ इस प्रकार $w\Vdash p$ T, जिसका अर्थ है कि $\Vdash$ T की परिभाषा का उपयोग करते हुए w R w रिफ्लेक्सिव क्रिपके फ्रेम के वर्ग से मेल खाता है।

इसकी पूर्णता प्रमाणित करने की तुलना में L के संबंधित वर्ग को चिह्नित करना प्रायः अधिक सरल होता है, इस प्रकार पत्राचार पूर्णता प्रमाण के लिए एक मार्गदर्शक के रूप में कार्य करता है। पत्राचार का उपयोग मोडल लॉजिक्स की अपूर्णता दिखाने के लिए भी किया जाता है: मान लीजिए कि L₁ ⊆ L₂ सामान्य मोडल लॉजिक्स हैं जो फ़्रेम के समान वर्ग के अनुरूप हैं, किन्तु L₁ L₂ के सभी प्रमेयों को सिद्ध नहीं करता है। तब L₁ क्रिपके अपूर्ण है। इस प्रकार से उदाहरण के लिए, स्कीमा $\Box (A\leftrightarrow \Box A)\to \Box A$ एक अपूर्ण तर्क उत्पन्न करता है, क्योंकि यह GL (अर्थात सकर्मक और विपरीत अच्छी तरह से स्थापित फ्रेम) के फ्रेम के समान वर्ग से मेल खाता है, किन्तु GL-टॉटोलॉजी $\Box A\to \Box \Box A$ को प्रमाणित नहीं करता है

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

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

नाम	स्वयंसिद्ध	फ़्रेम की स्थिति
K	$\Box (A\to B)\to (\Box A\to \Box B)$	holds true for any frames
T	$\Box A\to A$	प्रतिवर्ती: $w\,R\,w$
-	$\Box \Box A\to \Box A$	सघन: $w\,R\,u\Rightarrow \exists v\,(w\,R\,v\land v\,R\,u)$
4	$\Box A\to \Box \Box A$	संक्रमणीय: $w\,R\,v\wedge v\,R\,u\Rightarrow w\,R\,u$
D	$\Box A\to \Diamond A$ or $\Diamond \top$ or $\neg \Box \bot$	क्रमिक: $\forall w\,\exists v\,(w\,R\,v)$
B	$A\to \Box \Diamond A$ or $\Diamond \Box A\to A$	सममितीय : $w\,R\,v\Rightarrow v\,R\,w$
5	$\Diamond A\to \Box \Diamond A$	इयूक्लिडियन: $w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v$
GL	$\Box (\Box A\to A)\to \Box A$	R संक्रमणीय, R−1 प्रतिपादित
Grz	$\Box (\Box (A\to \Box A)\to A)\to A$	R प्रतिवर्ती and संक्रमणीय, R−1−Id प्रतिपादित
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$	(एक समष्टि दूसरे क्रम की गुण)
G	$\Diamond \Box A\to \Box \Diamond A$	अभिसृत: $w\,R\,u\land w\,R\,v\Rightarrow \exists x\,(u\,R\,x\land v\,R\,x)$
-	$A\to \Box A$	विवेकपूर्ण: $w\,R\,v\Rightarrow w=v$
-	$\Diamond A\to \Box A$	आंशिक फलन: $w\,R\,u\land w\,R\,v\Rightarrow u=v$
-	$\Diamond A\leftrightarrow \Box A$	फलन: $\forall w\,\exists !u\,w\,R\,u$ ($\exists !$ विशिष्टता परिमाणीकरण है)
-	$\Box A$ or $\Box \bot$	रिक्त: $\forall w\,\forall u\,\neg (w\,R\,u)$

स्वयंसिद्ध 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

विहित मॉडल

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

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

बीजगणित में लिंडेनबाम-टार्स्की बीजगणित शब्दार्थ निर्माण के समान भूमिका निभाते है।

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

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

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

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

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

$X\Vdash A$ यदि और केवल यदि $A\in X$.

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

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

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

यह तर्क इच्छानुसार से L के लिए कार्य नहीं करता है, क्योंकि इस तथ्य का कोई प्रमाण नहीं है कि कैनोनिकल मॉडल का अंतर्निहित फ्रेम L की फ्रेम नियम को पूर्ण करता है।

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

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

सूत्रों के विहित समुच्चय का एक संघ स्वयं विहित है। पूर्व के वार्तालाप से यह पता चलता है कि सूत्रों के विहित समुच्चय द्वारा स्वयंसिद्ध कोई भी तर्क कृपके पूर्ण और संक्षिप्त है।

सूत्रों का विहित समुच्चय क्रिप्के पूर्ण है, और सघनता प्रमेय.

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

विहित, क्योंकि वे सघन नहीं हैं। स्वयंसिद्ध M अपने आप में है विहित नहीं (गोल्डब्लैट, 1991), किन्तु संयुक्त तर्क ' S4.1' (में) वास्तव में, जहाँ तक ​​कि 'K4.1') भी विहित है।

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

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

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

परिमित मॉडल गुण

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

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

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

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

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

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

See also: मल्टीमॉडल लॉजिक

इस प्रकार से क्रिपके शब्दार्थ में तर्कशास्त्र का सीधा सामान्यीकरण है

क्रिपके शब्दार्थ में एक से अधिक विधियों कों के साथ तर्क का सीधा सामान्यीकरण है। आवश्यकता ऑपरेटरों के समुच्चय के रूप में $\{\Box _{i}\mid \,i\in I\}$ वाली भाषा के लिए क्रिपके फ्रेम में एक गैर-रिक्त समुच्चय W होता है जो प्रत्येक i ∈ I के लिए द्विआधारी संबंध R_i से सुसज्जित होता है। संतुष्टि संबंध की परिभाषा को निम्नानुसार संशोधित किया गया है:

$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$है जिसमें एकल अभिगम्यता संबंध R है, और प्रत्येक विधियों के लिए उपसमुच्चय D_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 प्रथम-क्रम की भाषा है। एल का एक क्रिपके मॉडल एक ट्रिपल $\langle W,\leq ,\{M_{w}\}_{w\in W}\rangle$ है जहां $\langle W,\leq \rangle$ एक अंतर्ज्ञानवादी क्रिपके फ्रेम है, एमडब्ल्यू प्रत्येक नोड w ∈ W के लिए एक (मौलिक ) L-संरचना है, और जब भी u ≤ v होता है तो निम्नलिखित संगतता स्थितियां प्रयुक्त होती हैं:

• M_u का डोमेन M_v के डोमेन में सम्मिलित है,
• M_u और M_v में फलन प्रतीकों की प्राप्ति M_u के तत्वों पर सहमत होती है,
• प्रत्येक n-ary विधेय P और तत्वों a₁,...,a_n ∈ M_u के लिए: यदि P(a₁,...,a_n) M_u में है, तो यह M_v में है।

M_w के तत्वों द्वारा वेरिएबल का मूल्यांकन e दिया गया है, हम संतुष्टि संबंध $w\Vdash A[e]$ को परिभाषित करें :

• $w\Vdash P(t_{1},\dots ,t_{n})[e]$ यदि और केवल यदि $P(t_{1}[e],\dots ,t_{n}[e])$ M_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 के आसपास यह अनुभव किया गया कि क्रिप्के शब्दार्थ का टोपोस सिद्धांत में अस्तित्वगत परिमाणीकरण के उपचार से गहरा संबंध था। अर्थात्, समूह के वर्गों के लिए अस्तित्व का 'स्थानीय' पक्ष 'संभव' का प्रकार का तर्क था। चूंकि यह विकास अनेक लोगों का कार्य था, इस संबंध में प्रायः क्रिपके-जॉयल सिमेंटिक्स नाम का उपयोग किया जाता है।

मॉडल निर्माण

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

क्रिपके सिमेंटिक्स में प्राकृतिक समरूपता को p-मॉर्फिज्म कहा जाता है (जो छद्म-एपिमोर्फिज्म के लिए छोटा है, किन्तु इसके पूर्व वाला शब्द कदाचित् ही कभी उपयोग किया जाता है)। क्रिपके फ़्रेम $\langle W,R\rangle$ और $\langle W',R'\rangle$ का एक p-मॉर्फिज्म एक मैपिंग $f\colon W\to W'$ है जैसे कि

• f पहुंच संबंध को समान रखता है, अर्थात , u R v का तात्पर्य f(u) R’ f(v) है,
• जब भी f(u) R’ v’ होता है, तो v∈W होता है जैसे कि u R v और f(v)=v', है।

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

संतुष्ट है

$w\Vdash p$ यदि और केवल यदि $f(w)\Vdash 'p$, किसी भी प्रस्तावित वेरिएबल p के लिए है।

p-मॉर्फिज्म एक विशेष प्रकार के द्विसिमुलेशन हैं। सामान्य, फ़्रेम $\langle W,R\rangle$ और $\langle W',R'\rangle$ के मध्य एक द्विसिमुलेशन एक संबंध B ⊆ W × W' है, जो निम्नलिखित "ज़िग-ज़ैग" संपत्ति को संतुष्ट करता है:

• यदि u B u’ और u R v, तो v’ ∈ W’ का अस्तित्व इस प्रकार है कि v B v’ और u’ R’ v’,
• यदि u B u’ और u’ R’ v’, तो v ∈ W का अस्तित्व इस प्रकार है कि v B v’ और u R v।

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

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

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

इस परिभाषा से जो मुख्य गुण निकलता है वह है मॉडलों के द्विसिमुलेशन (इसलिए p-मॉर्फिज्म भी) संरक्षित करते हैंसभी सूत्रों की संतुष्टि, न कि केवल प्रस्तावात्मक वेरिएबल । हम क्रिपके मॉडल को ट्री(ग्राफ़ सिद्धांत) में परिवर्तन कर सकते हैं 'उतारना'। मॉडल दिया $\langle W,R,\Vdash \rangle$ और निश्चित नोड w₀∈ w, हम मॉडल को परिभाषित करते हैं

हम अनरेवेलिंग का उपयोग करके क्रिप्के मॉडल को एक पेड़ में बदल सकते हैं। एक मॉडल $\langle W,R,\Vdash \rangle$ और एक निश्चित नोड w₀ ∈ W, को देखते हुए, हम एक मॉडल $\langle W',R',\Vdash '\rangle$ को परिभाषित करते हैं जहां W' सभी परिमित अनुक्रमों $s=\langle w_{0},w_{1},\dots ,w_{n}\rangle$ का समुच्चय है जैसे कि सभी i < n के लिए w_i R w_i+1 और $s\Vdash p$ यदि और केवल यदि $w_{n}\Vdash p$ एक प्रस्तावित वेरिएबल 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 समुच्चय है

निस्पंदन एक उपयोगी निर्माण है जिसका उपयोग कई तर्कों के लिए एफएमपी को सिद्ध करने के लिए किया जाता है। मान लीजिए कि X उपसूत्रों के अंतर्गत बंद किए गए सूत्रों का एक समूह है। मॉडल $\langle W,R,\Vdash \rangle$ का X-फ़िल्टरेशन, W से मॉडल $\langle W',R',\Vdash '\rangle$ तक मैपिंग f है, जैसे कि

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

इससे यह निष्कर्ष निकलता है कि f सभी सूत्रों की संतुष्टि को सुरक्षित रखता है यदि X. विशिष्ट अनुप्रयोगों में, हम f को प्रक्षेपण के रूप में लेते हैं संबंध पर W के भागफल समुच्चय पर है

u ≡_X v यदि और केवल यदि सभी A ∈ X, $u\Vdash A$ के लिए यदि और केवल यदि $v\Vdash A$ जैसा कि सुलझाने के स्तिथियों में, भागफल पर पहुंच संबंध की परिभाषा भिन्न होती है।

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

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

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

Main articles: क्रिपके संरचना, राज्य संक्रमण प्रणाली, and मॉडल जाँच

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