{
  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: '98',
  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: {}
}