{
localUrl: '../page/arithmetical_adequacy_GL.html',
arbitalUrl: 'https://arbital.com/p/arithmetical_adequacy_GL',
rawJsonUrl: '../raw/5n5.json',
likeableId: '3266',
likeableType: 'page',
myLikeValue: '0',
likeCount: '2',
dislikeCount: '0',
likeScore: '2',
individualLikes: [
'EricBruylant',
'PatrickStevens'
],
pageId: 'arithmetical_adequacy_GL',
edit: '1',
editSummary: '',
prevEdit: '0',
currentEdit: '1',
wasPublished: 'true',
type: 'wiki',
title: 'Solovay's theorems of arithmetical adequacy for GL',
clickbait: 'Using GL to reason about PA, and viceversa',
textLength: '2590',
alias: 'arithmetical_adequacy_GL',
externalUrl: '',
sortChildrenBy: 'likes',
hasVote: 'false',
voteType: '',
votesAnonymous: 'false',
editCreatorId: 'JaimeSevillaMolina',
editCreatedAt: '2016-07-29 12:53:04',
pageCreatorId: 'JaimeSevillaMolina',
pageCreatedAt: '2016-07-29 12:53:04',
seeDomainId: '0',
editDomainId: 'AlexeiAndreev',
submitToDomainId: '0',
isAutosave: 'false',
isSnapshot: 'false',
isLiveEdit: 'true',
isMinorEdit: 'false',
indirectTeacher: 'false',
todoCount: '3',
isEditorComment: 'false',
isApprovedComment: 'true',
isResolved: 'false',
snapshotText: '',
anchorContext: '',
anchorText: '',
anchorOffset: '0',
mergedInto: '',
isDeleted: 'false',
viewCount: '25',
text: '[summary:\n$GL\\vdash A$ iff $PA\\vdash A^*$ for every realization $*$.\n\nRealizations are translations from modal sentences to sentences of arithmetic.\n]\n\nOne of the things that makes [-5l3] such an interesting formal system is the direct relation between its theorems and a restricted albeit rich class of theorems regarding [5j7 provability predicates] in [3ft].\n\nAs usual, the adequacy result comes in the form of a pair of theorems, proving respectively [-soundness] and [-completeness] for this class. Before stating the results, we describe the way to [translation translate] modal sentences to sentences of arithmetic, thus describing the class of sentences of arithmetic the result alludes to.\n\n##Realizations\nA realization $*$ is a function from the set of well-formed sentences of modal logic to the set of sentences of arithmetic. Intuitively, we are trying to preserve the structure of the sentence while mapping the expressions proper of modal logic to related predicates in the language of $PA$.\n\nConcretely,\n\n* $p^* = S_p$: sentence letters are mapped to arbitrary closed sentences of arithmetic.\n* $(\\square A)^*=P(A^*)$: the box operator is mapped to a [-5j7] $P$, usually the [-5gt].\n* $(A\\to B)^* = A^* \\to B^*$: truth functional compounds are mapped as expected.\n* $\\bot ^* = \\neg X$, where $X$ is any theorem of $PA$, for example, $0\\ne 1$.\n\nThe class of sentences of $PA$ such that there exists a modal sentence of which they are a realization is the set for which we will prove the soundness and completeness.\n\n##Arithmetical soundness\n> If $GL\\vdash A$, then $PA\\vdash A^*$ for every realization $*$.\n\nThe applications to this result are endless. For example, this theorem allows us to take advantage of the procedures to calculate [5lx fixed points] in $GL$ to get results about $PA$.\n\nTo better get an intuition of how this correspondence works, try figuring out how the properties of the [-5j7] relate to the axioms and rules of inference of $GL$.\n\n[ Proof]\n\n##Arithmetical completeness\n> If $GL\\not\\vdash A$, then there exists a realization $*$ such that $PA\\not\\vdash A^*$.\n\nThe proof of arithmetical completeness is a beautiful and intricate construction that exploits the semantical relationship between $GL$ and the finite, transitive and irreflexive [5ll Kripke models]. Check [ its page] for the details.\n\n##Uniform arithmetical completeness\n> There exists a realization $*$ such that for every modal sentence $A$ we have that $GL\\not\\vdash A$ only if $PA\\not\\vdash A$.\n\nThis result generalizes the arithmetical completeness theorem to a new level.\n\n[ Proof]',
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: [
'provability_logic'
],
commentIds: [],
questionIds: [],
tagIds: [
'work_in_progress_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: '17798',
pageId: 'arithmetical_adequacy_GL',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newAlias',
createdAt: '2016-07-30 21:12:51',
auxPageId: '',
oldSettingsValue: 'arithmetical_adecuacy',
newSettingsValue: 'arithmetical_adequacy_GL'
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17718',
pageId: 'arithmetical_adequacy_GL',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newParent',
createdAt: '2016-07-29 12:53:06',
auxPageId: 'provability_logic',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17719',
pageId: 'arithmetical_adequacy_GL',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newTag',
createdAt: '2016-07-29 12:53:06',
auxPageId: 'work_in_progress_meta_tag',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17716',
pageId: 'arithmetical_adequacy_GL',
userId: 'JaimeSevillaMolina',
edit: '1',
type: 'newEdit',
createdAt: '2016-07-29 12:53:04',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
}
],
feedSubmissions: [],
searchStrings: {},
hasChildren: 'false',
hasParents: 'true',
redAliases: {},
improvementTagIds: [],
nonMetaTagIds: [],
todos: [],
slowDownMap: 'null',
speedUpMap: 'null',
arcPageIds: 'null',
contentRequests: {}
}