{
localUrl: '../page/proof_lobs_thorem.html',
arbitalUrl: 'https://arbital.com/p/proof_lobs_thorem',
rawJsonUrl: '../raw/59b.json',
likeableId: '3038',
likeableType: 'page',
myLikeValue: '0',
likeCount: '6',
dislikeCount: '0',
likeScore: '6',
individualLikes: [
'PatrickLaVictoir',
'EricBruylant',
'JaimeSevillaMolina',
'MalcolmMcCrimmon',
'PatrickStaples',
'StephanieZolayvar'
],
pageId: 'proof_lobs_thorem',
edit: '12',
editSummary: 'fixed some links',
prevEdit: '11',
currentEdit: '12',
wasPublished: 'true',
type: 'wiki',
title: 'Proof of Löb's theorem',
clickbait: 'Proving that I am Santa Claus',
textLength: '3792',
alias: 'proof_lobs_thorem',
externalUrl: '',
sortChildrenBy: 'likes',
hasVote: 'false',
voteType: '',
votesAnonymous: 'false',
editCreatorId: 'MYass',
editCreatedAt: '2016-10-14 10:10:23',
pageCreatorId: 'JaimeSevillaMolina',
pageCreatedAt: '2016-07-10 03:03:54',
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: '334',
text: '[summary:\nYou can prove [55w] by assuming $\\square A\\to A$ and constructing a sentence $S$ such that $PA\\vdash S\\leftrightarrow (\\square S \\to A)$\n]\n\nThe intuition behind the proof of Löb's theorem invokes the formalization of the following argument:\n\nLet $S$ stand for the sentence "If $S$ is provable, then I am Santa Claus".\n\nAs it is standard, when trying to prove a If...then theorem we can start by supposing the antecedent and checking that the consequent follows. But if $S$ is provable, then we can chain its proof to an application of modus ponens of $S$ to itself in order to get a proof of the consequent "I am Santa Claus". If we suppose that showing the existence of a proof of a sentence implies that the sentence is true, then "I am Santa Claus" is true.\n\nThus we have supposed that $S$ is provably true then it follows that "I am Santa Claus", which is a proof of what $S$ states! Therefore, $S$ is provably true, and we can apply the same reasoning again (this time without supposing a counterfactual) to get that it is true that "I am Santa Claus".\n\nHoly Gödel! Have we broken logic? If this argument worked, then we could prove any nonsensical thing we wanted. So where does it fail?\n\nOne suspicious point is our implicit assumption that $S$ can be constructed in the first place as a first order sentence. But we know that there exists a [5j7 provability predicate] encoding the meaning we need, and then we can apply the [59c diagonal lemma] to the formula $Prv(x)\\implies$ "I am Santa Claus" to get our desired $S$.\n\n(We will ignore the fact that expressing "I am Santa Claus" in the language of first order logic is rather difficult, since we could easily replace it with something simple like $0=1$.)\n\nIt turns out that the culprit of this paradox is the apparently innocent supposition that when "I am Santa Claus" is provable, then it is true.\n\nHow can this be false?, you may ask. Well, the standard provability predicate $Prv$ is something of the form $\\exists y Proof(x,y)$, where $Proof(x,y)$ is true iff $y$ encodes a valid proof of $x$. But $y$ might be a [ nonstandard number] encoding a [ nonstandard proof] of infinitely many steps. If the only proofs of $x$ are nonstandard then certainly you will never be able to prove $x$ from the axioms of the system using standard methods.\n\nWe can restate this result as Löb's theorem: If $Prv(A)\\implies A$ is provable, then $A$ is provable.\n\n-----\nNow we go for the formal proof.\n\nLet $T$ be an [ axiomatizable] extension of [ minimal arithmetic], and $P$ a one-place predicate satisfying the [5j7 Bernais-Hilbert derivability conditions], which are:\n\n1. If $T\\vdash A$, then $T\\vdash P(A)$.\n2. $T\\vdash P(A\\implies B) \\implies (P(A)\\implies P(B))$\n3. $T\\vdash P(A)\\implies P(P(A))$.\n\nFor example, $PA$ and the standard provability predicate [ satisfy those conditions].\n\nLet us suppose that $A$ is such that $T\\vdash P(A)\\implies A$.\n\nAs $T$ extends [ minimal arithmetic], the [-59c] is applicable, and thus there exists $S$ such that $T\\vdash S \\iff (P(S)\\implies A)$.\n\nBy condition 1, $T\\vdash P(S \\implies (P(S)\\implies A))$.\n\nBy condition 2, $T\\vdash P(S) \\implies P(P(S) \\implies A)$.\n\nAlso by condition 2, $T\\vdash P(P(S) \\implies A) \\implies (P(P(S)) \\implies P(A))$.\n\nCombining these, $T\\vdash P(S) \\implies (P(P(S)) \\implies P(A))$.\n\nBy condition 3, $T\\vdash P(S)\\implies P(P(S))$ and thus $T\\vdash P(S)\\implies P(A)$.\n\nBy our initial assumption, this means that $T\\vdash P(S)\\implies A$.\n\nBut by the construction of $S$, then $T\\vdash S$!\n\nBy condition 1 again, then $T\\vdash P(S)$, and since we already had shown that $T\\vdash P(S)\\implies A$, we have that $T\\vdash A$, which completes the proof.\n\nWe remark that $P$ can be any predicate satisfying the conditions, such as the verum predicate $x=x$.',
metaText: '',
isTextLoaded: 'true',
isSubscribedToDiscussion: 'false',
isSubscribedToUser: 'false',
isSubscribedAsMaintainer: 'false',
discussionSubscriberCount: '1',
maintainerCount: '1',
userSubscriberCount: '0',
lastVisit: '',
hasDraft: 'false',
votes: [],
voteSummary: [
'0',
'0',
'0',
'0',
'0',
'0',
'0',
'0',
'0',
'0'
],
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',
'DylanHendrickson',
'MalcolmMcCrimmon',
'MYass'
],
childIds: [],
parentIds: [
'lobs_theorem'
],
commentIds: [
'59w',
'5ht'
],
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: '3611',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '2',
dislikeCount: '0',
likeScore: '2',
individualLikes: [],
id: '20142',
pageId: 'proof_lobs_thorem',
userId: 'MYass',
edit: '12',
type: 'newEdit',
createdAt: '2016-10-14 10:10:23',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: 'fixed some links'
},
{
likeableId: '3415',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '18830',
pageId: 'proof_lobs_thorem',
userId: 'JaimeSevillaMolina',
edit: '11',
type: 'newEdit',
createdAt: '2016-08-19 11:10:44',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '3254',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '17765',
pageId: 'proof_lobs_thorem',
userId: 'MalcolmMcCrimmon',
edit: '10',
type: 'newEdit',
createdAt: '2016-07-29 23:29:51',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17680',
pageId: 'proof_lobs_thorem',
userId: 'JaimeSevillaMolina',
edit: '9',
type: 'newEdit',
createdAt: '2016-07-28 17:24:55',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17676',
pageId: 'proof_lobs_thorem',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'deleteTag',
createdAt: '2016-07-28 17:21:28',
auxPageId: 'needs_clickbait_meta_tag',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '3211',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '17391',
pageId: 'proof_lobs_thorem',
userId: 'JaimeSevillaMolina',
edit: '8',
type: 'newEdit',
createdAt: '2016-07-23 08:40:45',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17390',
pageId: 'proof_lobs_thorem',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newAlias',
createdAt: '2016-07-23 08:40:44',
auxPageId: '',
oldSettingsValue: '59b',
newSettingsValue: 'proof_lobs_thorem'
},
{
likeableId: '3167',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '17290',
pageId: 'proof_lobs_thorem',
userId: 'JaimeSevillaMolina',
edit: '7',
type: 'newEdit',
createdAt: '2016-07-22 10:01:54',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17280',
pageId: 'proof_lobs_thorem',
userId: 'JaimeSevillaMolina',
edit: '6',
type: 'newEdit',
createdAt: '2016-07-22 08:10:02',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17156',
pageId: 'proof_lobs_thorem',
userId: 'EricBruylant',
edit: '0',
type: 'newTag',
createdAt: '2016-07-19 02:40:03',
auxPageId: 'needs_clickbait_meta_tag',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '16564',
pageId: 'proof_lobs_thorem',
userId: 'JaimeSevillaMolina',
edit: '5',
type: 'newEdit',
createdAt: '2016-07-11 18:10:28',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '16372',
pageId: 'proof_lobs_thorem',
userId: 'DylanHendrickson',
edit: '4',
type: 'newEdit',
createdAt: '2016-07-10 15:01:39',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '16338',
pageId: 'proof_lobs_thorem',
userId: 'JaimeSevillaMolina',
edit: '3',
type: 'newEdit',
createdAt: '2016-07-10 03:11:26',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '16337',
pageId: 'proof_lobs_thorem',
userId: 'JaimeSevillaMolina',
edit: '2',
type: 'newEdit',
createdAt: '2016-07-10 03:10:46',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '16335',
pageId: 'proof_lobs_thorem',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newParent',
createdAt: '2016-07-10 03:03:56',
auxPageId: 'lobs_theorem',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '16333',
pageId: 'proof_lobs_thorem',
userId: 'JaimeSevillaMolina',
edit: '1',
type: 'newEdit',
createdAt: '2016-07-10 03:03:54',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
}
],
feedSubmissions: [],
searchStrings: {},
hasChildren: 'false',
hasParents: 'true',
redAliases: {},
improvementTagIds: [],
nonMetaTagIds: [],
todos: [],
slowDownMap: 'null',
speedUpMap: 'null',
arcPageIds: 'null',
contentRequests: {
improveStub: {
likeableId: '3709',
likeableType: 'contentRequest',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '156',
pageId: 'proof_lobs_thorem',
requestType: 'improveStub',
createdAt: '2016-11-13 21:08:41'
},
lessTechnical: {
likeableId: '3342',
likeableType: 'contentRequest',
myLikeValue: '0',
likeCount: '8',
dislikeCount: '0',
likeScore: '8',
individualLikes: [],
id: '35',
pageId: 'proof_lobs_thorem',
requestType: 'lessTechnical',
createdAt: '2016-08-06 05:23:20'
},
slowDown: {
likeableId: '3359',
likeableType: 'contentRequest',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [],
id: '39',
pageId: 'proof_lobs_thorem',
requestType: 'slowDown',
createdAt: '2016-08-07 00:13:54'
}
}
}