{
localUrl: '../page/normal_system_of_provability.html',
arbitalUrl: 'https://arbital.com/p/normal_system_of_provability',
rawJsonUrl: '../raw/5j8.json',
likeableId: '0',
likeableType: 'page',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
pageId: 'normal_system_of_provability',
edit: '5',
editSummary: '',
prevEdit: '3',
currentEdit: '5',
wasPublished: 'true',
type: 'wiki',
title: 'Normal system of provability logic',
clickbait: '',
textLength: '1895',
alias: 'normal_system_of_provability',
externalUrl: '',
sortChildrenBy: 'likes',
hasVote: 'false',
voteType: '',
votesAnonymous: 'false',
editCreatorId: 'JaimeSevillaMolina',
editCreatedAt: '2017-04-22 16:13:21',
pageCreatorId: 'JaimeSevillaMolina',
pageCreatedAt: '2016-07-22 09:54:59',
seeDomainId: '0',
editDomainId: 'AlexeiAndreev',
submitToDomainId: '0',
isAutosave: 'false',
isSnapshot: 'false',
isLiveEdit: 'true',
isMinorEdit: 'false',
indirectTeacher: 'false',
todoCount: '1',
isEditorComment: 'false',
isApprovedComment: 'true',
isResolved: 'false',
snapshotText: '',
anchorContext: '',
anchorText: '',
anchorOffset: '0',
mergedInto: '',
isDeleted: 'false',
viewCount: '22',
text: 'Between the modal systems of provability, the normal systems distinguish themselves by exhibiting nice properties that make them useful to reason.\n\nA normal system of provability is defined as satisfying the following conditions:\n\n1. Has **necessitation** as a rule of inference. That is, if $L\\vdash A$ then $L\\vdash \\square A$.\n2. Has **modus ponens** as a rule of inference: if $L\\vdash A\\rightarrow B$ and $L\\vdash A$ then $L\\vdash B$.\n3. Proves all **tautologies** of propositional logic.\n4. Proves all the **distributive axioms** of the form $\\square(A\\rightarrow B)\\rightarrow (\\square A \\rightarrow \\square B)$.\n5. It is **closed under substitution**. That is, if $L\\vdash F(p)$ then $L\\vdash F(H)$ for every modal sentence $H$.\n\nThe simplest normal system, which only has as axioms the tautologies of propositional logic and the distributive axioms, it is known as the [ K system].\n\n##Normality\nThe good properties of normal systems are collectively called **normality**.\n\nSome theorems of normality are:\n\n* $L\\vdash \\square(A_1\\wedge ... \\wedge A_n)\\leftrightarrow (\\square A_1 \\wedge ... \\wedge \\square A_n)$\n* Suppose $L\\vdash A\\rightarrow B$. Then $L\\vdash \\square A \\rightarrow \\square B$ and $L\\vdash \\diamond A \\rightarrow \\diamond B$.\n* $L\\vdash \\diamond A \\wedge \\square B \\rightarrow \\diamond (A\\wedge B)$\n\n##First substitution theorem\nNormal systems also satisfy the first substitution theorem.\n>(**First substitution theorem**) Suppose $L\\vdash A\\leftrightarrow B$, and $F(p)$ is a formula in which the sentence letter $p$ appears. Then $L\\vdash F(A)\\leftrightarrow F(B)$.\n\n##The hierarchy of normal systems\nThe most studied normal systems can be ordered by extensionality:\n\n\n\nThose systems are:\n\n* The system K\n* The system K4\n* The system [5l3 GL]\n* The system T\n* The system S4\n* The system B\n* The system S5\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'
],
childIds: [],
parentIds: [
'modal_logic'
],
commentIds: [],
questionIds: [],
tagIds: [
'needs_summary_meta_tag'
],
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: '22484',
pageId: 'normal_system_of_provability',
userId: 'JaimeSevillaMolina',
edit: '5',
type: 'newEdit',
createdAt: '2017-04-22 16:13:21',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17486',
pageId: 'normal_system_of_provability',
userId: 'JaimeSevillaMolina',
edit: '3',
type: 'newEdit',
createdAt: '2016-07-25 14:21:17',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17384',
pageId: 'normal_system_of_provability',
userId: 'EricBruylant',
edit: '0',
type: 'newTag',
createdAt: '2016-07-23 05:43:19',
auxPageId: 'needs_summary_meta_tag',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17289',
pageId: 'normal_system_of_provability',
userId: 'JaimeSevillaMolina',
edit: '2',
type: 'newEdit',
createdAt: '2016-07-22 09:56:25',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '3195',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '17288',
pageId: 'normal_system_of_provability',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newParent',
createdAt: '2016-07-22 09:55:22',
auxPageId: 'modal_logic',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '3181',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '17286',
pageId: 'normal_system_of_provability',
userId: 'JaimeSevillaMolina',
edit: '1',
type: 'newEdit',
createdAt: '2016-07-22 09:54:59',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
}
],
feedSubmissions: [],
searchStrings: {},
hasChildren: 'false',
hasParents: 'true',
redAliases: {},
improvementTagIds: [],
nonMetaTagIds: [],
todos: [],
slowDownMap: 'null',
speedUpMap: 'null',
arcPageIds: 'null',
contentRequests: {}
}