{
localUrl: '../page/5hr.html',
arbitalUrl: 'https://arbital.com/p/5hr',
rawJsonUrl: '../raw/5hr.json',
likeableId: '0',
likeableType: 'page',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
pageId: '5hr',
edit: '5',
editSummary: '',
prevEdit: '4',
currentEdit: '5',
wasPublished: 'true',
type: 'wiki',
title: 'Löb's theorem and computer programs',
clickbait: '',
textLength: '2262',
alias: '5hr',
externalUrl: '',
sortChildrenBy: 'likes',
hasVote: 'false',
voteType: '',
votesAnonymous: 'false',
editCreatorId: 'MalcolmMcCrimmon',
editCreatedAt: '2016-07-29 23:32:55',
pageCreatorId: 'JaimeSevillaMolina',
pageCreatedAt: '2016-07-21 16:00:02',
seeDomainId: '0',
editDomainId: 'AlexeiAndreev',
submitToDomainId: '0',
isAutosave: 'false',
isSnapshot: 'false',
isLiveEdit: 'true',
isMinorEdit: 'false',
indirectTeacher: 'false',
todoCount: '5',
isEditorComment: 'false',
isApprovedComment: 'true',
isResolved: 'false',
snapshotText: '',
anchorContext: '',
anchorText: '',
anchorOffset: '0',
mergedInto: '',
isDeleted: 'false',
viewCount: '76',
text: 'The close relationship between [ logic and computability] allows us to frame Löb's theorem in terms of a computer program which is systematically looking for proofs of mathematical statements, `ProofSeeker(X)`.\n\nProofSeeker can be something like this:\n\n ProofSeeker(X):\n n=1\n while(True):\n if Prv(X,n): return True\n else n = n+1\n\nWhere `Prv(X,n)` is true if $n$ [ encodes] a proof of $X$%%note:See [-5gt] for more info on how to talk about provablity%%.\n\nNow we form a special sentence called a *reflection principle*, of the form $L(X)$= "*If `ProofSeeker(X)` halts, then X is true*". (This requires a [322 quine] to construct.)\n\nReflection principles are intuitively true, since ProofSeeker clearly halts iff it finds a proof of $X$, and if there is a proof of $X$, then $X$ must be true if we have chosen an appropriate [-5hh] to search for proofs. For example, let's say that `ProofSeeker` is looking for proofs within [3ft].\n\nThe question now becomes, what happens when we call `ProofSeeker` on $L(X)$? Is $PA$ capable of proving that the reflection principle for any given $X$ is true, and therefore `ProofSeeker` will eventually halt? Or will it run forever?\n\nSeveral possibilities appear:\n\n1. If $PA\\vdash X$, then certainly $PA\\vdash L(X)$, since if the consequent of $L(X)$ is provable, then the whole sentence is provable.\n2. If $PA\\vdash \\neg X$, then we cannot assert that $PA\\vdash L(X)$, for that would imply asserting that $PA\\vdash$"There is no proof of X". This is tantamount to $PA$ asserting the [-5km] of $PA$, which is forbidden by [ Gödel's second incompleteness theorem].\n3. If $X$ is undecidable in $PA$, then if it were the case that $PA\\vdash L(X)$ it would be inconsistent that $PA\\vdash \\neg X$ for the same reason as when $X$ is disprovable, and thus $PA\\vdash X$, contradicting that it was undecidable.\n\n**Löb's theorem** is the assertion that $PA$ proves the reflection principle for $X$ only if $PA$ proves $X$.\n\nOr conversely, Löb's theorem states that if $PA\\not\\vdash X$ then $PA\\not\\vdash \\square_{PA} X \\rightarrow X$.\n\nIt can be [ proved] in $PA$ and stronger systems. It has a very strong link with Gödel's second incompleteness theorem, and in fact [ they both are equivalent].',
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',
'PatrickLaVictoir',
'EricRogstad',
'MalcolmMcCrimmon'
],
childIds: [],
parentIds: [
'lobs_theorem'
],
commentIds: [],
questionIds: [],
tagIds: [],
relatedIds: [],
markIds: [],
explanations: [],
learnMore: [],
requirements: [],
subjects: [],
lenses: [],
lensParentId: 'lobs_theorem',
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: '17766',
pageId: '5hr',
userId: 'MalcolmMcCrimmon',
edit: '5',
type: 'newEdit',
createdAt: '2016-07-29 23:32:55',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '3218',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '17420',
pageId: '5hr',
userId: 'EricRogstad',
edit: '4',
type: 'newEdit',
createdAt: '2016-07-23 18:02:09',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: '"if it was" -> "if it were"'
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17392',
pageId: '5hr',
userId: 'JaimeSevillaMolina',
edit: '3',
type: 'newEdit',
createdAt: '2016-07-23 09:22:59',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '3150',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '17229',
pageId: '5hr',
userId: 'PatrickLaVictoir',
edit: '2',
type: 'newEdit',
createdAt: '2016-07-21 16:58:34',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17222',
pageId: '5hr',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newParent',
createdAt: '2016-07-21 16:00:04',
auxPageId: 'lobs_theorem',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17220',
pageId: '5hr',
userId: 'JaimeSevillaMolina',
edit: '1',
type: 'newEdit',
createdAt: '2016-07-21 16:00:02',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
}
],
feedSubmissions: [],
searchStrings: {},
hasChildren: 'false',
hasParents: 'true',
redAliases: {},
improvementTagIds: [],
nonMetaTagIds: [],
todos: [],
slowDownMap: 'null',
speedUpMap: 'null',
arcPageIds: 'null',
contentRequests: {}
}