{ localUrl: '../page/godel_codes.html', arbitalUrl: 'https://arbital.com/p/godel_codes', rawJsonUrl: '../raw/31z.json', likeableId: '1983', likeableType: 'page', myLikeValue: '0', likeCount: '2', dislikeCount: '0', likeScore: '2', individualLikes: [ 'EricBruylant', 'JaimeSevillaMolina' ], pageId: 'godel_codes', edit: '5', editSummary: '', prevEdit: '4', currentEdit: '5', wasPublished: 'true', type: 'wiki', title: 'Gödel encoding and self-reference', clickbait: 'The formalism that mathematicians use to talk about arithmetic turns out to be able to talk about itself.', textLength: '1801', alias: 'godel_codes', externalUrl: '', sortChildrenBy: 'likes', hasVote: 'false', voteType: '', votesAnonymous: 'false', editCreatorId: 'PatrickLaVictoir', editCreatedAt: '2016-05-06 17:58:15', pageCreatorId: 'PatrickLaVictoir', pageCreatedAt: '2016-04-03 21:53:44', seeDomainId: '0', editDomainId: 'AlexeiAndreev', submitToDomainId: '0', isAutosave: 'false', isSnapshot: 'false', isLiveEdit: 'true', isMinorEdit: 'false', indirectTeacher: 'false', todoCount: '0', isEditorComment: 'false', isApprovedComment: 'true', isResolved: 'false', snapshotText: '', anchorContext: '', anchorText: '', anchorOffset: '0', mergedInto: '', isDeleted: 'false', viewCount: '104', text: 'A Gödel encoding is a way of using the formal machinery of proving theorems in arithmetic to discuss that very machinery. [Kurt Gödel](https://en.wikipedia.org/wiki/Kurt_G%C3%B6del) rocked the world of mathematics in 1931 by showing that this was possible, and that it had surprising consequences for the sort of things that could ever be formally proven in a given system.\n\nThe original formulation of this self-referential framework was really messy (involving prime factorizations of huge numbers), but we can think about it more easily now by thinking about computer programs. In order to get mathematical statements that refer to themselves, we can first show that we can talk interchangeably about mathematical proofs and computer programs, and then show how to write computer programs that refer to themselves.\n\nTo be specific about the machinery of proving theorems, we'll use the formal system of [3ft Peano Arithmetic].\n\nWhat kind of self-reference do we want for our computer program? We would like to be able to write a program that takes its own source code and performs computations on it. But it doesn't count for the program to access its own location in memory; we'd like something we could write directly into an interpreter, with no other framework, and get the same result.\n\nThis kind of program is known as a [322 quine].\n\nGödel encoding is equivalent to an encoding of a computer program as a binary string.\n\nIf we think about any conjecture in mathematics that can be stated in terms of arithmetic, you can write a program that loops over all possible strings, checks whether any of them is a valid proof of the conjecture, and halts if and only if it finds one. In the other direction, we can imagine proving a theorem about whether a particular computer program ever halts.', 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: [ 'PatrickLaVictoir' ], childIds: [ 'quine' ], parentIds: [ 'math' ], commentIds: [], questionIds: [], tagIds: [], 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: '9630', pageId: 'godel_codes', userId: 'PatrickLaVictoir', edit: '5', type: 'newEdit', createdAt: '2016-05-06 17:58:15', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '9628', pageId: 'godel_codes', userId: 'PatrickLaVictoir', edit: '4', type: 'newEdit', createdAt: '2016-05-06 17:54:31', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '9210', pageId: 'godel_codes', userId: 'PatrickLaVictoir', edit: '3', type: 'newEdit', createdAt: '2016-04-03 22:14:44', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '9208', pageId: 'godel_codes', userId: 'PatrickLaVictoir', edit: '2', type: 'newEdit', createdAt: '2016-04-03 22:03:46', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '9206', pageId: 'godel_codes', userId: 'PatrickLaVictoir', edit: '1', type: 'newEdit', createdAt: '2016-04-03 21:53:44', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' } ], feedSubmissions: [], searchStrings: {}, hasChildren: 'true', hasParents: 'true', redAliases: {}, improvementTagIds: [], nonMetaTagIds: [], todos: [], slowDownMap: 'null', speedUpMap: 'null', arcPageIds: 'null', contentRequests: {} }