{
localUrl: '../page/diagonal_lemma.html',
arbitalUrl: 'https://arbital.com/p/diagonal_lemma',
rawJsonUrl: '../raw/59c.json',
likeableId: '3506',
likeableType: 'page',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [
'GregorGerasev'
],
pageId: 'diagonal_lemma',
edit: '4',
editSummary: '',
prevEdit: '3',
currentEdit: '4',
wasPublished: 'true',
type: 'wiki',
title: 'Diagonal lemma',
clickbait: 'Constructing self-referential sentences',
textLength: '1939',
alias: 'diagonal_lemma',
externalUrl: '',
sortChildrenBy: 'likes',
hasVote: 'false',
voteType: '',
votesAnonymous: 'false',
editCreatorId: 'JaimeSevillaMolina',
editCreatedAt: '2016-07-22 08:11:27',
pageCreatorId: 'JaimeSevillaMolina',
pageCreatedAt: '2016-07-10 03:26:11',
seeDomainId: '0',
editDomainId: 'AlexeiAndreev',
submitToDomainId: '0',
isAutosave: 'false',
isSnapshot: 'false',
isLiveEdit: 'true',
isMinorEdit: 'false',
indirectTeacher: 'false',
todoCount: '6',
isEditorComment: 'false',
isApprovedComment: 'true',
isResolved: 'false',
snapshotText: '',
anchorContext: '',
anchorText: '',
anchorOffset: '0',
mergedInto: '',
isDeleted: 'false',
viewCount: '175',
text: '[summary: If F(x) is a one place formula of First Order Logic and $T$ is a theory extending [ minimal arithmetic] then there exists a sentence $S$ such that $T\\vdash S\\iff F(\\ulcorner S \\urcorner)$.]\n\nThe **diagonal lemma** shows how to construct self-referential sentences in the language of arithmetic from formulas $\\phi(x)$.\n\nIn its standard form it says that is $T$ is a theory extending [ minimal arithmetic] (so that it can talk about [ recursive] expressions with full generality) and $\\phi(x)$ is a formula with one free variable $x$ then there exists a sentence $S$ such that $T\\vdash S\\leftrightarrow \\phi(\\ulcorner S\\urcorner)$.\n\nThis can be further [ generalized] for cases with multiples formulas and variables.\n\nThe diagonal lemma is important because it allows the formalization of all kind of self-referential and apparently paradoxical sentences. \n\nTake for example the liar's sentence affirming that "This sentence is false". Since [ there is no truth predicate], we will have to adapt it to our language to say "This sentence is not provable". Since there is a [5gt predicate of arithmetic expressing provability] we can construct a formula $\\neg \\square_{PA} (x)$, which is true iff there is no proof in [3ft $PA$] of the sentence [31z encoded] by $x$.\n\nBy invoking the diagonal's lemma, we can see that there exists a sentence $G$ such that $PA\\vdash G\\leftrightarrow \\neg \\square_{PA} (\\ulcorner G\\urcorner)$, which reflects the spirit of our informal sentence. The [ weak form of Gödel's first incompleteness theorem] follows swiftly from there.\n\nThe equivalent in computation of the diagonal lemma is called [322 quining], and refers to computer programs which produce their own source code as part of their computation.\n\nIndeed, the key insight of the diagonal lemma and quining is that you can have subexpressions in your program that when "expanded" are identical to the original expression that contains them.',
metaText: '',
isTextLoaded: 'true',
isSubscribedToDiscussion: 'false',
isSubscribedToUser: 'false',
isSubscribedAsMaintainer: 'false',
discussionSubscriberCount: '2',
maintainerCount: '2',
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: [
'quine'
],
parentIds: [
'math'
],
commentIds: [],
questionIds: [],
tagIds: [
'needs_parent_meta_tag',
'stub_meta_tag'
],
relatedIds: [],
markIds: [],
explanations: [],
learnMore: [],
requirements: [],
subjects: [],
lenses: [
{
id: '101',
pageId: 'diagonal_lemma',
lensId: 'quine',
lensIndex: '0',
lensName: 'Quine',
lensSubtitle: '',
createdBy: '2vh',
createdAt: '2016-07-21 17:36:35',
updatedBy: '2vh',
updatedAt: '2016-07-21 17:36:46'
}
],
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: '17382',
pageId: 'diagonal_lemma',
userId: 'EricBruylant',
edit: '0',
type: 'newTag',
createdAt: '2016-07-23 05:40:07',
auxPageId: 'needs_parent_meta_tag',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17317',
pageId: 'diagonal_lemma',
userId: 'EricRogstad',
edit: '0',
type: 'newParent',
createdAt: '2016-07-22 17:01:20',
auxPageId: 'math',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17281',
pageId: 'diagonal_lemma',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newAlias',
createdAt: '2016-07-22 08:11:27',
auxPageId: '',
oldSettingsValue: '59c',
newSettingsValue: 'diagonal_lemma'
},
{
likeableId: '3163',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '2',
dislikeCount: '0',
likeScore: '2',
individualLikes: [],
id: '17282',
pageId: 'diagonal_lemma',
userId: 'JaimeSevillaMolina',
edit: '4',
type: 'newEdit',
createdAt: '2016-07-22 08:11:27',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17235',
pageId: 'diagonal_lemma',
userId: 'JaimeSevillaMolina',
edit: '3',
type: 'newEdit',
createdAt: '2016-07-21 17:45:13',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17234',
pageId: 'diagonal_lemma',
userId: 'JaimeSevillaMolina',
edit: '2',
type: 'newEdit',
createdAt: '2016-07-21 17:37:06',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17232',
pageId: 'diagonal_lemma',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newChild',
createdAt: '2016-07-21 17:36:30',
auxPageId: 'quine',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '16340',
pageId: 'diagonal_lemma',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newTag',
createdAt: '2016-07-10 03:26:13',
auxPageId: 'stub_meta_tag',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '16339',
pageId: 'diagonal_lemma',
userId: 'JaimeSevillaMolina',
edit: '1',
type: 'newEdit',
createdAt: '2016-07-10 03:26:11',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
}
],
feedSubmissions: [],
searchStrings: {},
hasChildren: 'true',
hasParents: 'true',
redAliases: {},
improvementTagIds: [],
nonMetaTagIds: [],
todos: [],
slowDownMap: 'null',
speedUpMap: 'null',
arcPageIds: 'null',
contentRequests: {}
}