{
localUrl: '../page/kripke_model.html',
arbitalUrl: 'https://arbital.com/p/kripke_model',
rawJsonUrl: '../raw/5ll.json',
likeableId: '3244',
likeableType: 'page',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [
'EricBruylant'
],
pageId: 'kripke_model',
edit: '6',
editSummary: '',
prevEdit: '5',
currentEdit: '6',
wasPublished: 'true',
type: 'wiki',
title: 'Kripke model',
clickbait: 'The semantics of modal logic',
textLength: '4625',
alias: 'kripke_model',
externalUrl: '',
sortChildrenBy: 'likes',
hasVote: 'false',
voteType: '',
votesAnonymous: 'false',
editCreatorId: 'JaimeSevillaMolina',
editCreatedAt: '2016-07-26 16:42:16',
pageCreatorId: 'JaimeSevillaMolina',
pageCreatedAt: '2016-07-26 10:42:23',
seeDomainId: '0',
editDomainId: 'AlexeiAndreev',
submitToDomainId: '0',
isAutosave: 'false',
isSnapshot: 'false',
isLiveEdit: 'true',
isMinorEdit: 'false',
indirectTeacher: 'false',
todoCount: '17',
isEditorComment: 'false',
isApprovedComment: 'true',
isResolved: 'false',
snapshotText: '',
anchorContext: '',
anchorText: '',
anchorOffset: '0',
mergedInto: '',
isDeleted: 'false',
viewCount: '61',
text: '**Kripke models** are [ interpretations] of [-534] which turn out to be adequate under some basic constraints for a wide array of systems of modal logic.\n\n#Definition \nA Kripke model $M$ is formed by three elements:\n\n* A set of **worlds** $W$\n* A **visibility relationship** between worlds $R$. If $wRx$, we will say that $w$ sees $x$ or that $x$ is a successor of $w$.\n* A **valuation function** $V$ that associates pairs of worlds and sentence letters to truth values.\n\nYou can visualize Kripke worlds as a [-digraph] in which each node is a world, and the edges represent visibility.\n\n[todo: images of Kripke worlds]\n\nThe valuation function can be extended to assign truth values to whole modal sentences. We will say that a world $w\\in W$ makes a modal sentence $A$ true (*notation*: $M,w\\models A$) if it is assigned a truth value of true according to the following rules:\n\n* If $A$ is a sentence letter $p$, then $M,w\\models p$ if $V(w,p)=\\top$.\n* If $A$ is a truth functional compound of sentences, then its value comes from the propositional calculus and the values of its components. For example, if $A=B\\to C$, then $M,w\\models A$ [-46m] $M,w\\not\\models B$ or $M,w\\models C$.\n* If $A$ is of the form $\\square B$, then $M,w\\models \\square B$ if $M,x\\models B$ for every successor $x$ of $w$.\n\nGiven this way of assigning truth values to sentences, we will say the following:\n\n* $A$ is valid in a model $M$ (*notation*: $M\\models A$) if $M,w\\models A$ for every $w$ in $W$. \n* $A$ is valid in a class of models if it is valid in every model of the class.\n* $A$ is satisfiable in a model $M$ if there exists $w\\in W$ such that $M,w\\models A$.\n* $A$ is satisfiable in a class of models if it is satisfiable in some model of the class.\n\nNotice that a sentence $A$ is valid in a class of models iff its negation is not satisfiable.\n\n#Kripke models as semantics of modal logic\nKripke models are tightly connected to the interpretations of certain modal logics.\n\nFor example, they model well the rules of [5j8 normal provability systems].\n\n**Exercise**: show that Kripke models satisfy the necessitation rule of modal logic. That is, if $A$ is valid in $M$, then $\\square A$ is valid in $M$.\n\n%%hidden(Show solution):\nLet $w\\inW$ be a world of $M$. Let $x$ be an arbitrary successor of $w$. Then, as $M\\models A$, then $M,x\\models A$. Since $x$ was arbitrary, every successor of $w$ models $A$, so $w\\models \\square A$. As $w$ was arbitrary, then every world in $M$ models $\\square A$, and thus $M\\models \\square A$.\n%%\n\n**Exercise**: Show that the distributive axioms are always valid in Kripke models. Distributive axioms are modal sentences of the form $\\square[A\\to B]\\to(\\square A \\to \\square B)$.\n\n%%hidden(Show solution):\nSuppose that $w\\in W$ is such that $w\\models \\square[A\\to B]$ and $w\\models \\square A$.\n\nLet $x$ be a successor of $w$. Then $x\\models A\\to B$ and $x\\models A$. We conclude by the propositional calculus that $x\\models B$, so as $x$ was an arbitrary successor we have that $w\\models \\square B$, and thus $w\\models\\square[A\\to B]\\to(\\square A \\to \\square B)$.\n\nWe conclude that $M\\models\\square[A\\to B]\\to(\\square A \\to \\square B)$, no matter what $M$ is.\n%%\n\nThose two last exercises prove that the [ K system] of modal logic is [soundness sound] for the class of all Kripke models. This is because we have proved that its axioms and rules of inference hold in all Kripke models (propositional tautologies and modus ponens trivially hold).\n\n##Some adequacy theorems\nNow we present a relation of modal logics and the class of Kripke models in which they are [adequacy adequate]. You can check the proofs of adequacy in their respective pages.\n\n* The class of *all* Kripke models is adequate to the [ K system]\n* The class of [573 transitive] Kripke models is adequate to [ K4]\n* The class of [ reflexive] Kripke models is adequate to [ T]\n* The class of [ reflexive] and [573 transitive] Kripke models is adequate to [ S4]\n* The class of [ reflexive] and [ symmetric] Kripke models is adequate to [ B]\n* The class of [ reflexive] and [ euclidean] Kripke models is adequate to [ S5]\n* The class of [ finite], [ irreflexive] and [573 transitive] Kripke models is adequate to [5l3 GL]\n\nNotice that as the constraint on the models becomes stronger, the set of valid sentences increases, and thus the correspondent adequate system is stronger.\n\nA note about notation may be in order. We say that a Kripke model is, e.g, [573 transitive] if its visibility relation is transitive %%note:Same for reflexive, symmetric and euclidean %%. Similarly, a Kripke model is finite if its set of worlds is finite.\n',
metaText: '',
isTextLoaded: 'true',
isSubscribedToDiscussion: 'false',
isSubscribedToUser: 'false',
isSubscribedAsMaintainer: 'false',
discussionSubscriberCount: '1',
maintainerCount: '1',
userSubscriberCount: '0',
lastVisit: '',
hasDraft: 'false',
votes: [],
voteSummary: 'null',
muVoteSummary: '0',
voteScaling: '0',
currentUserVote: '-2',
voteCount: '0',
lockedVoteType: '',
maxEditEver: '0',
redLinkCount: '0',
lockedBy: '',
lockedUntil: '',
nextPageId: '',
prevPageId: '',
usedAsMastery: 'false',
proposalEditNum: '0',
permissions: {
edit: {
has: 'false',
reason: 'You don't have domain permission to edit this page'
},
proposeEdit: {
has: 'true',
reason: ''
},
delete: {
has: 'false',
reason: 'You don't have domain permission to delete this page'
},
comment: {
has: 'false',
reason: 'You can't comment in this domain because you are not a member'
},
proposeComment: {
has: 'true',
reason: ''
}
},
summaries: {},
creatorIds: [
'JaimeSevillaMolina',
'DylanHendrickson'
],
childIds: [],
parentIds: [
'modal_logic'
],
commentIds: [],
questionIds: [],
tagIds: [],
relatedIds: [],
markIds: [],
explanations: [],
learnMore: [],
requirements: [],
subjects: [],
lenses: [],
lensParentId: '',
pathPages: [],
learnMoreTaughtMap: {},
learnMoreCoveredMap: {},
learnMoreRequiredMap: {},
editHistory: {},
domainSubmissions: {},
answers: [],
answerCount: '0',
commentCount: '0',
newCommentCount: '0',
linkedMarkCount: '0',
changeLogs: [
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17530',
pageId: 'kripke_model',
userId: 'JaimeSevillaMolina',
edit: '6',
type: 'newEdit',
createdAt: '2016-07-26 16:42:16',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17529',
pageId: 'kripke_model',
userId: 'JaimeSevillaMolina',
edit: '5',
type: 'newEdit',
createdAt: '2016-07-26 16:38:34',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17528',
pageId: 'kripke_model',
userId: 'JaimeSevillaMolina',
edit: '4',
type: 'newEdit',
createdAt: '2016-07-26 16:37:33',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17520',
pageId: 'kripke_model',
userId: 'DylanHendrickson',
edit: '3',
type: 'newEdit',
createdAt: '2016-07-26 13:56:12',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '3235',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '17519',
pageId: 'kripke_model',
userId: 'DylanHendrickson',
edit: '2',
type: 'newEdit',
createdAt: '2016-07-26 13:51:11',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: 'typo'
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17517',
pageId: 'kripke_model',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newParent',
createdAt: '2016-07-26 10:42:25',
auxPageId: 'modal_logic',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17515',
pageId: 'kripke_model',
userId: 'JaimeSevillaMolina',
edit: '1',
type: 'newEdit',
createdAt: '2016-07-26 10:42:23',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
}
],
feedSubmissions: [],
searchStrings: {},
hasChildren: 'false',
hasParents: 'true',
redAliases: {},
improvementTagIds: [],
nonMetaTagIds: [],
todos: [],
slowDownMap: 'null',
speedUpMap: 'null',
arcPageIds: 'null',
contentRequests: {}
}