{
localUrl: '../page/modal_logic.html',
arbitalUrl: 'https://arbital.com/p/modal_logic',
rawJsonUrl: '../raw/534.json',
likeableId: '3080',
likeableType: 'page',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [
'EricBruylant'
],
pageId: 'modal_logic',
edit: '10',
editSummary: '',
prevEdit: '9',
currentEdit: '10',
wasPublished: 'true',
type: 'wiki',
title: 'Modal logic',
clickbait: 'The logic of boxes and bots.',
textLength: '2574',
alias: 'modal_logic',
externalUrl: '',
sortChildrenBy: 'likes',
hasVote: 'false',
voteType: '',
votesAnonymous: 'false',
editCreatorId: 'JaimeSevillaMolina',
editCreatedAt: '2016-07-27 21:13:12',
pageCreatorId: 'JaimeSevillaMolina',
pageCreatedAt: '2016-07-05 01:08:40',
seeDomainId: '0',
editDomainId: 'AlexeiAndreev',
submitToDomainId: '0',
isAutosave: 'false',
isSnapshot: 'false',
isLiveEdit: 'true',
isMinorEdit: 'false',
indirectTeacher: 'false',
todoCount: '8',
isEditorComment: 'false',
isApprovedComment: 'true',
isResolved: 'false',
snapshotText: '',
anchorContext: '',
anchorText: '',
anchorOffset: '0',
mergedInto: '',
isDeleted: 'false',
viewCount: '88',
text: 'Modal logic is a [formal_system] in which we expand [-propositional_calculus] with two new operators meant to represent necessity ($\\square$) and possibility ($\\diamond$).%%note:There are more [ general modal logics] with different modal predicates out there.%%\n\nThose two operators can be defined in terms of each other. For example, we have that something is possible iff it is not necessary that its opposite is true; ie, $\\diamond A \\iff \\neg \\square \\neg A$.\n\nThus in modal logic, you can express sentences as $\\square A$ to express that it is necessary that $A$ is true. You can also go more abstract and say $\\neg\\square \\bot$ to express that it is not necessary that false is true. If we read the box operator as "there is no mathematical proof of" then the previous sentence becomes "there is no mathematical proof of falsehood", which encodes the [ consistency of arithmetic].\n\nThere are many systems of modal logic %note: See for example [t_modal_logic T],[b_modal_logic B],[s5_modal_logic S5],[s4_modal_logic S4],[k_modal_logic K], [gls_modal_logic GLS]%, which differ in the sentences they take as [-axioms] and which [ rules of inference] they allow.\n\nOf particular interest are the systems called [5j8 normal systems of modal logic], and especially the [5l3 $Gödel-Löb$] system (called $GL$ for short, also known as the logic of provability). The main interest of $GL$ comes from being a [ decidable] logic which allows us to reason about sentences of [3ft Peano arithmetic] talking about [5gt provability] via [ translations], as proved by the [ arithmetical adequacy theorems of Solomonov].\n\nAnother widely studied system of modal logic is $GLS$, for which Solomonov proved [ adequacy for truth] in the [-standard_model_of_arithmetic].\n\nThe [semantics_mathematical semantics] of the normal systems of modal logic come in the form of [Kripke_models]: digraph structures composed of worlds over which a visibility relation is defined.\n\n##Sentences\nWell formed sentences of modal logic are defined as follows:\n\n* $\\bot$ is a well-formed sentence of modal logic.\n* The sentence letters $p,q,...$ are well-formed sentences of modal logic.\n* If $A$ is a well-formed sentence, then $\\square A$ is a well-formed sentence.\n* If $A$ and $B$ are well formed sentences, then $A\\to B$ is a well-formed sentence.\n\nThe rest of [ logical connectors] can then be defined as abbreviations for structures made from implication and $\\bot$. For example , $\\neg A = A\\to \\bot$. The possibility operator $\\diamond$ is defined as $\\neg\\square\\neg$ as per the previous discussion.',
metaText: '',
isTextLoaded: 'true',
isSubscribedToDiscussion: 'false',
isSubscribedToUser: 'false',
isSubscribedAsMaintainer: 'false',
discussionSubscriberCount: '2',
maintainerCount: '2',
userSubscriberCount: '0',
lastVisit: '',
hasDraft: 'false',
votes: [],
voteSummary: [
'0',
'0',
'0',
'0',
'0',
'0',
'0',
'0',
'0',
'0'
],
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: {
Summary: 'Modal logic is a [formal_system] in which we expand [-propositional_calculus] with two new operators meant to represent necessity ($\\square$) and possibility ($\\diamond$).%%note:There are more [ general modal logics] with different modal predicates out there.%%'
},
creatorIds: [
'JaimeSevillaMolina',
'EricBruylant',
'PatrickLaVictoir'
],
childIds: [
'standard_provability_predicate',
'normal_system_of_provability',
'provability_logic',
'kripke_model',
'modalized_modal_sentence',
'modal_combat'
],
parentIds: [
'math'
],
commentIds: [],
questionIds: [],
tagIds: [
'start_meta_tag'
],
relatedIds: [],
markIds: [],
explanations: [
{
id: '5669',
parentId: 'modal_logic',
childId: 'modal_logic',
type: 'subject',
creatorId: 'JaimeSevillaMolina',
createdAt: '2016-07-27 21:09:41',
level: '2',
isStrong: 'true',
everPublished: 'true'
}
],
learnMore: [],
requirements: [],
subjects: [
{
id: '5669',
parentId: 'modal_logic',
childId: 'modal_logic',
type: 'subject',
creatorId: 'JaimeSevillaMolina',
createdAt: '2016-07-27 21:09:41',
level: '2',
isStrong: 'true',
everPublished: 'true'
}
],
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: '19688',
pageId: 'modal_logic',
userId: 'EricBruylant',
edit: '0',
type: 'newChild',
createdAt: '2016-09-23 14:32:01',
auxPageId: 'modal_combat',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '18443',
pageId: 'modal_logic',
userId: 'EricBruylant',
edit: '0',
type: 'deleteTag',
createdAt: '2016-08-05 17:43:11',
auxPageId: 'stub_meta_tag',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '18441',
pageId: 'modal_logic',
userId: 'EricBruylant',
edit: '0',
type: 'newTag',
createdAt: '2016-08-05 17:43:08',
auxPageId: 'start_meta_tag',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '3291',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '17622',
pageId: 'modal_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newChild',
createdAt: '2016-07-27 21:38:11',
auxPageId: 'modalized_modal_sentence',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17621',
pageId: 'modal_logic',
userId: 'JaimeSevillaMolina',
edit: '10',
type: 'newEdit',
createdAt: '2016-07-27 21:13:12',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17619',
pageId: 'modal_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newTeacher',
createdAt: '2016-07-27 21:09:41',
auxPageId: 'modal_logic',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17620',
pageId: 'modal_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newSubject',
createdAt: '2016-07-27 21:09:41',
auxPageId: 'modal_logic',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17618',
pageId: 'modal_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'deleteSubject',
createdAt: '2016-07-27 21:09:37',
auxPageId: 'modalized_modal_sentence',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17616',
pageId: 'modal_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newSubject',
createdAt: '2016-07-27 21:09:33',
auxPageId: 'modalized_modal_sentence',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17516',
pageId: 'modal_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newChild',
createdAt: '2016-07-26 10:42:25',
auxPageId: 'kripke_model',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17514',
pageId: 'modal_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newAlias',
createdAt: '2016-07-26 09:54:57',
auxPageId: '',
oldSettingsValue: 'provability_logic',
newSettingsValue: 'modal_logic'
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17491',
pageId: 'modal_logic',
userId: 'JaimeSevillaMolina',
edit: '9',
type: 'newEdit',
createdAt: '2016-07-25 17:14:21',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17490',
pageId: 'modal_logic',
userId: 'JaimeSevillaMolina',
edit: '8',
type: 'newEdit',
createdAt: '2016-07-25 17:13:44',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17488',
pageId: 'modal_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newChild',
createdAt: '2016-07-25 17:10:55',
auxPageId: 'provability_logic',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '3166',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '17291',
pageId: 'modal_logic',
userId: 'JaimeSevillaMolina',
edit: '7',
type: 'newEdit',
createdAt: '2016-07-22 10:04:00',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17287',
pageId: 'modal_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newChild',
createdAt: '2016-07-22 09:55:22',
auxPageId: 'normal_system_of_provability',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17238',
pageId: 'modal_logic',
userId: 'JaimeSevillaMolina',
edit: '6',
type: 'newEdit',
createdAt: '2016-07-21 17:56:16',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17237',
pageId: 'modal_logic',
userId: 'JaimeSevillaMolina',
edit: '5',
type: 'newEdit',
createdAt: '2016-07-21 17:54:39',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: 'Typo'
},
{
likeableId: '3152',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '2',
dislikeCount: '0',
likeScore: '2',
individualLikes: [],
id: '17230',
pageId: 'modal_logic',
userId: 'PatrickLaVictoir',
edit: '4',
type: 'newEdit',
createdAt: '2016-07-21 16:59:24',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17164',
pageId: 'modal_logic',
userId: 'EricBruylant',
edit: '0',
type: 'newChild',
createdAt: '2016-07-19 19:01:21',
auxPageId: 'standard_provability_predicate',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '16830',
pageId: 'modal_logic',
userId: 'EricBruylant',
edit: '3',
type: 'newEdit',
createdAt: '2016-07-16 01:02:58',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: 'alias add'
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '16829',
pageId: 'modal_logic',
userId: 'EricBruylant',
edit: '0',
type: 'newAlias',
createdAt: '2016-07-16 01:02:57',
auxPageId: '',
oldSettingsValue: '534',
newSettingsValue: 'provability_logic'
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '15383',
pageId: 'modal_logic',
userId: 'EricBruylant',
edit: '0',
type: 'newParent',
createdAt: '2016-07-05 06:44:37',
auxPageId: 'math',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '15381',
pageId: 'modal_logic',
userId: 'EricBruylant',
edit: '2',
type: 'newEdit',
createdAt: '2016-07-05 06:44:21',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '15372',
pageId: 'modal_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newTag',
createdAt: '2016-07-05 01:08:42',
auxPageId: 'stub_meta_tag',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '15371',
pageId: 'modal_logic',
userId: 'JaimeSevillaMolina',
edit: '1',
type: 'newEdit',
createdAt: '2016-07-05 01:08:40',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
}
],
feedSubmissions: [],
searchStrings: {},
hasChildren: 'true',
hasParents: 'true',
redAliases: {},
improvementTagIds: [],
nonMetaTagIds: [],
todos: [],
slowDownMap: 'null',
speedUpMap: 'null',
arcPageIds: 'null',
contentRequests: {}
}