{
localUrl: '../page/fixed_point_theorem_provability_logic.html',
arbitalUrl: 'https://arbital.com/p/fixed_point_theorem_provability_logic',
rawJsonUrl: '../raw/5lx.json',
likeableId: '3287',
likeableType: 'page',
myLikeValue: '0',
likeCount: '3',
dislikeCount: '0',
likeScore: '3',
individualLikes: [
'PatrickLaVictoir',
'EricBruylant',
'JaimeSevillaMolina'
],
pageId: 'fixed_point_theorem_provability_logic',
edit: '8',
editSummary: '',
prevEdit: '7',
currentEdit: '8',
wasPublished: 'true',
type: 'wiki',
title: 'Fixed point theorem of provability logic',
clickbait: 'Deal with those pesky self-referential sentences!',
textLength: '13863',
alias: 'fixed_point_theorem_provability_logic',
externalUrl: '',
sortChildrenBy: 'likes',
hasVote: 'false',
voteType: '',
votesAnonymous: 'false',
editCreatorId: 'JaimeSevillaMolina',
editCreatedAt: '2017-03-02 16:00:20',
pageCreatorId: 'JaimeSevillaMolina',
pageCreatedAt: '2016-07-27 20:41:53',
seeDomainId: '0',
editDomainId: 'AlexeiAndreev',
submitToDomainId: '0',
isAutosave: 'false',
isSnapshot: 'false',
isLiveEdit: 'true',
isMinorEdit: 'false',
indirectTeacher: 'false',
todoCount: '14',
isEditorComment: 'false',
isApprovedComment: 'true',
isResolved: 'false',
snapshotText: '',
anchorContext: '',
anchorText: '',
anchorOffset: '0',
mergedInto: '',
isDeleted: 'false',
viewCount: '111',
text: '[summary:\n>Let $\\phi(p, q_1,...,q_n)$ be a modal sentence [5m4 modalized] in $p$. \n>Then there exists a sentence $H(q_1,..,q_n)$ such that $GL\\vdash \\boxdot[p\\leftrightarrow \\phi(p,q_1,...,q_n)] \\leftrightarrow \\boxdot[p\\leftrightarrow H(q_1,..,q_n)]$.\n\nThis result can be used to give us insight about [59c self-referent] sentences of arithmetic.\n]\n\nThe fixed point theorem of provability logic is a key result that gives a explicit procedure to find equivalences for sentences such as the ones produced by the [-59c].\n\nIn its most simple formulation, it states that:\n\n>Let $\\phi(p)$ be a modal sentence [5m4 modalized] in $p$. Then there exists a letterless $H$ such that $GL\\vdash \\boxdot[p\\leftrightarrow \\phi(p)] \\leftrightarrow \\boxdot[p\\leftrightarrow H]$ %%note: Notation: $\\boxdot A = A\\wedge \\square A$%%.\n\nThis result can be generalized for cases in which letter sentences other than $p$ appear in the original formula, and the case where multiple formulas are present.\n\n#Fixed points\nThe $H$ that appears in the statement of the theorem is called a **fixed point** of $\\phi(p)$ on $p$.\n\nIn general, a fixed point of a formula $\\psi(p, q_1...,q_n)$ on $p$ will be a modal formula $H(q_1,...,q_n)$ in which $p$ does not appear such that $GL\\vdash \\boxdot[p\\leftrightarrow\\psi(p, q_1,...,q_n)] \\leftrightarrow \\boxdot[p_i\\leftrightarrow H(q_1,...,q_n)]$.\n\nThe fixed point theorem gives a sufficient condition for the existence of fixed points, namely that $\\psi$ is modalized in $\\psi$. It is an open problem to determine a necessary condition for the existence of fixed points.\n\nFixed points satisfy some important properties:\n\nIf $H$ is a fixed point of $\\phi$ on $p$, then $GL\\vdash H(q_1,...,q_n)\\leftrightarrow \\phi(H(q_1,...,q_n),q_1,...,q_n)$. This coincides with our intuition of what a fixed point is, since this can be seen as an argument that when fed to $\\phi$ it returns something equivalent to itself.\n\n%%hidden(Proof):\nSince $H$ is a fixed point, $GL\\vdash \\boxdot[p\\leftrightarrow\\psi(p, q_1,...,q_n)] \\leftrightarrow \\boxdot[p_i\\leftrightarrow H(q_1,...,q_n)]$. Since $GL$ is [ normal], it is closed under substitution. By substituing $p$ for $H$, we find that $GL\\vdash \\boxdot[H(q_1,...,q_n)\\leftrightarrow\\psi(H(q_1,...,q_n), q_1,...,q_n)] \\leftrightarrow \\boxdot[H(q_1,...,q_n)\\leftrightarrow H(q_1,...,q_n)]$.\n\nBut trivially $GL\\vdash \\boxdot[H(q_1,...,q_n)\\leftrightarrow H(q_1,...,q_n)$, so $GL\\vdash \\boxdot[H(q_1,...,q_n)\\leftrightarrow\\psi(H(q_1,...,q_n), q_1,...,q_n)]$.\n%%\n\n$H$ and $I$ are fixed points of $\\phi$ if and only if $GL\\vdash H\\leftrightarrow I$. This is knows as the \n**uniqueness of fixed points**.\n\n%%hidden(Proof):\nLet $H$ be a fixed point on $p$ of $\\phi(p)$; that is, $GL\\vdash \\boxdot(p\\leftrightarrow \\phi(p))\\leftrightarrow (p\\leftrightarrow H)$.\n\nSuppose $I$ is such that $GL\\vdash H\\leftrightarrow I$. Then by the first substitution theorem, $GL\\vdash F(I)\\leftrightarrow F(H)$ for every formula $F(q)$. If $F(q)=\\boxdot(p\\leftrightarrow q)$, then $GL\\vdash \\boxdot(p\\leftrightarrow H)\\leftrightarrow \\boxdot(p\\leftrightarrow I)$, from which it follows that $GL\\vdash \\boxdot(p\\leftrightarrow \\phi(p))\\leftrightarrow (p\\leftrightarrow I)$.\n\nConversely, if $H$ and $I$ are fixed points, then $GL\\vdash \\boxdot (p\\leftrightarrow H)\\leftrightarrow \\boxdot (p\\leftrightarrow I)$, so since $GL$ is closed under substitution, $GL\\vdash\\boxdot (H\\leftrightarrow H)\\leftrightarrow \\boxdot (H\\leftrightarrow I)$. Since $GL\\vdash \\boxdot (H\\leftrightarrow H)$, it follows that $GL\\vdash (H\\leftrightarrow I)$.\n%%\n\n#Special case fixed point theorem\n\nThe special case of the fixed point theorem is what we stated at the beginning of the page. Namely:\n\n>Let $\\phi(p)$ be a modal sentence [5m4 modalized] in p. \n>Then there exists a letterless $H$ such that $GL\\vdash \\boxdot[p\\leftrightarrow \\phi(p)] \\leftrightarrow \\boxdot[p\\leftrightarrow H]$.\n\nThere is a nice semantical procedure based on [5ll Kripke models] that allows to compute $H$ as a truth functional compound of sentences $\\square^n \\bot$ %%note:$\\square^n A = \\underbrace{\\square,\\square,\\ldots,\\square}_{n\\text{-times}} A$ %%. (ie, $H$ is in [ normal form]).\n\n\n##$A$-traces\nLet $A$ be a modal sentence modalized in $p$ in which no other sentence letter appears (we call such a sentence a $p$-sentence). We want to calculate $A$'s fixed point on $p$. This procedure bears a resemblance to the [ trace] method for evaluating letterless modal sentences.\n\nWe are going to introduce the notion of the $A$-trace of a $p$-sentence $B$, notated by $[[B]]_A$. The $A$-trace maps modal sentences to sets of [45h natural numbers], and is defined recursively as follows:\n\n* $[[\\bot]]_A = \\emptyset$\n* $[[B\\to C]]_A = (\\mathbb{N} \\setminus [[B]]_A)\\cup [[C]]_A$\n* $[[\\square D]]_A=\\{m:\\forall i < m i\\in [[D]]_A\\}$\n* $[[p]]_A=[[A]]_A$\n\n*Lemma*: Let $M$ be a finite, transitive and irreflexive Kripke model in which $(p\\leftrightarrow A) is valid, and $B$ a $p$-sentence. Then $M,w\\models B$ iff $\\rho(w)\\in [[B]]_A$.\n\n%%hidden(Proof):\nComing soon [todo: proof]\n%%\n\n*Lemma*: The $A$-trace of a $p$-sentence $B$ is either finite or cofinite, and furthermore either it has less than $n$ elements or lacks less than $n$ elements, where $n$ is the number of $\\square$s in $A$.\n\n%%hidden(Proof):\nComing soon [todo: proof]\n%%\n\nThose two lemmas allow us to express the truth value of $A$ in terms of world ranks for models in which $p\\leftrightarrow A$ is valid. Then the fixed point $H$ will be either the union or the negation of the union of a finite number of sentences $\\square^{n+1}\\bot\\wedge \\square^n \\bot$ %%note:Such a sentence is only true in worlds of rank $n$%%\n\nIn the following section we work through an example, and demonstrate how can we easily compute those fixed points using a [ Kripke chain].\n\n##Applications\n\nFor an example, we will compute the fixed point for the modal [ Gödel sentence] $p\\leftrightarrow \\neg\\square p$ and analyze its significance.\n\nWe start by examining the truth value of $\\neg\\square p$ in the $0$th rank worlds. Since the only letter is $p$ and it is modalized, this can be done without problem (remember that $\\square B$ is always true in the rank $0$ worlds, no mater what $B$ is). Now we apply to $p$ the constraint of having the same truth value as $\\neg\\square p$.\n\nWe iterate the procedure for the next world ranks.\n\n$$\n\\begin{array}{cccc}\n \\text{world= } & p & \\square (p) & \\neg \\square (p) \\\\\n 0 & \\bot & \\top & \\bot \\\\\n 1 & \\top & \\bot & \\top \\\\\n 2 & \\top & \\bot & \\top \\\\\n\\end{array}\n$$\n\nSince there is only one $\\square$ in the formula, the chain is guaranteed to stabilize in the first world and there is no need for going further. We have shown the truth values in world $2$ to show that this is indeed the case.\n\nFrom the table we have just constructed it becomes evident that $[[p]]_{\\neg\\square p} = \\mathbb{N}\\setminus \\{0\\}$. Thus $H = \\square^{0+1}\\bot \\wedge \\square^0\\bot = \\neg\\square\\bot$.\n\nTherefore, $GL\\vdash \\square [p\\leftrightarrow \\neg\\square p]\\leftrightarrow \\square[p\\leftrightarrow \\neg\\square \\bot]$. Thus, the fixed point for the modal Gödel sentence is the [-5km] of arithmetic!\n\nBy employing the [ arithmetical soundness of GL], we can translate this result to $PA$ and show that $PA\\vdash \\square_{PA} [G\\leftrightarrow \\neg\\square_{PA} G]\\leftrightarrow \\square_{PA}[G\\leftrightarrow \\neg\\square_{PA} \\bot]$ for every sentence $G$ of arithmetic.\n\nSince in $PA$ we can construct $G$ by the [-59c] such that $PA\\vdash G\\leftrightarrow \\neg\\square_{PA} G$, by necessitation we have that for such a $G$ then $PA\\vdash \\square_PA[ G\\leftrightarrow \\neg\\square_{PA} G]$. By the theorem we just proved using the fixed point, then $PA\\vdash \\square_{PA}[G\\leftrightarrow \\neg\\square_{PA} \\bot]$. SInce [ everything $PA$ proves is true] then $PA\\vdash G\\leftrightarrow \\neg\\square_{PA} \\bot$.\n\nSurprisingly enough, the Gödel sentence is equivalent to the consistency of arithmetic! This makes more evident that $G$ is not provable [godel_second_incompleteness_theorm unless $PA$ is inconsistent], and that it is not disprovable unless it is [omega_inconsistency $\\omega$-inconsistent].\n\n**Exercise:** Find the fixed point for the [ Henkin sentence] $H\\leftrightarrow\\square H$.\n\n%%hidden(Show solution):\n$$\n\\begin{array}{ccc}\n \\text{world= } & p & \\square (p) \\\\\n 0 & \\top & \\top \\\\\n 1 & \\top & \\top \\\\\n\\end{array}\n$$\nThus the fixed point is simply $\\top$.\n%%\n\n\n#General case\nThe first generalization we make to the theorem is allowing the appearance of sentence letters other than the one we are fixing. The concrete statement is as follows:\n\n>Let $\\phi(p, q_1,...,q_n)$ be a modal sentence [5m4 modalized] in p. Then $\\phi$ has a fixed point on $p$.%%.\n\nThere are several constructive procedures for finding the fixed point in the general case.\n\nOne particularly simple procedure is based on **k-decomposition**.\n\n##K-decomposition\nLet $\\phi$ be as in the hypothesis of the fixed point theorem. Then we can express $\\phi$ as $B(\\square D_1(p), ..., \\square D_{k}(p))$, since every $p$ occurs within the scope of a $\\square$ (The $q_i$s are omitted for simplicity, but they may appear scattered between $B$ and the $D_i$s). This is called a $k$-decomposition of $\\phi$.\n\nIf $\\phi$ is $0$-decomposable, then it is already a fixed point, since $p$ does not appear. \n\nOtherwise, consider $B_i = B(\\square D_1(p), ..., \\square D_{i-1}(p),\\top, \\square D_{i+1}(p),...,\\square D_k(p))$, which is $k-1$-decomposable.\n\nAssuming that the procedure works for $k-1$ decomposable formulas, we can use it to compute a fixed point $H_i$ for each $B_i$. Now, $H=B(\\square D_1(H_1),...,\\square D_k(H_k))$ is the desired fixed point for $\\phi$.\n\n%%hidden(Proof):\n[todo: proof]\nThere is a nice semantic proof in *Computability and Logic*, by Boolos *et al*.\n%%\n\nThis procedure constructs fixed points with structural similarity to the original sentence.\n\n###Example\nLet's compute the fixed point of $p\\leftrightarrow \\neg\\square(q\\to p)$.\n\nWe can 1-decompose the formula in $B(d)=\\neg d$, $D_1(p)=q\\to p$. \n\nThen $B_1(p)=\\neg \\top = \\bot$, which is its own fixed point. Thus the desired fixed point is $H=B(\\square D_1(\\bot))=\\neg\\square \\neg q$.\n\n**Exercise:** Compute the fixed point of $p\\leftrightarrow \\square [\\square(p\\wedge q)\\wedge \\square(p\\wedge r)]$.\n\n%%hidden(Show solution):\nOne possible decomposition of the the formula at hand is $B(a)=a$, $D_1(p)=\\square(p\\wedge q)\\wedge \\square(p\\wedge r)$.\n\nNow we compute the fixed point of $B(\\top)$, which is simply $\\top$.\n\nTherefore the fixed point of the whole expression is $B(\\square D_1(p=\\top))=\\square[\\square(\\top\\wedge q)\\wedge \\square(\\top\\wedge r)]=\\square[\\square(q)\\wedge \\square(r)]$\n%%\n\n#Generalized fixed point theorem\n\n>Suppose that $A_i(p_1,...,p_n)$ are $n$ modal sentences such that $A_i$ is modalized in $p_n$ (possibly containing sentence letters other than $p_js$).\n\n>Then there exists $H_1, ...,H_n$ in which no $p_j$ appears such that $GL\\vdash \\wedge_{i\\le n} \\{\\boxdot (p_i\\leftrightarrow A_i(p_1,...,p_n)\\}\\leftrightarrow \\wedge_{i\\le n} \\{\\boxdot(p_i\\leftrightarrow H_i)\\}$.\n\n%%hidden(Proof):\nWe will prove it by induction. \n\nFor the base step, we know by the fixed point theorem that there is $H$ such that $GL\\vdash \\boxdot(p_1\\leftrightarrow A_i(p_1,...,p_n)) \\leftrightarrow \\boxdot(p_1\\leftrightarrow H(p_2,...,p_n))$\n\nNow suppose that for $j$ we have $H_1,...,H_j$ such that $GL\\vdash \\wedge_{i\\le j} \\{\\boxdot(p_i\\leftrightarrow A_i(p_1,...,p_n)\\}\\leftrightarrow \\wedge_{i\\le j} \\{\\boxdot(p_i\\leftrightarrow H_i(p_{j+1},...,p_n))\\}$.\n\nBy the [ second substitution theorem], $GL\\vdash \\boxdot(A\\leftrightarrow B)\\rightarrow [F(A)\\leftrightarrow F(B)]$. Therefore we have that $GL\\vdash \\boxdot(p_i\\leftrightarrow H_i(p_{j+1},...,p_n)\\rightarrow [\\boxdot(p_{j+1}\\leftrightarrow A_{j+1}(p_{1},...,p_n))\\leftrightarrow \\boxdot(p_{j+1}\\leftrightarrow A_{j+1}(p_{1},...,p_{i-1},H_i(p_{j+1},...,p_n),p_{i+1},...,p_n))]$.\n\nIf we iterate the replacements, we finally end up with $GL\\vdash \\wedge_{i\\le j} \\{\\boxdot(p_i\\leftrightarrow A_i(p_1,...,p_n)\\}\\rightarrow \\boxdot(p_{j+1}\\leftrightarrow A_{j+1}(H_1,...,H_j,p_{j+1},...,p_n))$.\n\nAgain by the fixed point theorem, there is $H_{j+1}'$ such that $GL\\vdash \\boxdot(p_{j+1}\\leftrightarrow A_{j+1}(H_1,...,H_j,p_{j+1},...,p_n)) \\leftrightarrow \\boxdot[p_{j+1}\\leftrightarrow H_{j+1}'(p_{j+2},...,p_n)]$.\n\nBut as before, by the second substitution theorem, $GL\\vdash \\boxdot[p_{j+1}\\leftrightarrow H_{j+1}'(p_{j+2},...,p_n)]\\rightarrow [\\boxdot(p_i\\leftrightarrow H_i(p_{j+1},...,p_n)) \\leftrightarrow \\boxdot(p_i\\leftrightarrow H_i(H_{j+1}',...,p_n))$.\n\nLet $H_{i}'$ stand for $H_i(H_{j+1}',...,p_n)$, and by combining the previous lines we find that $GL\\vdash \\wedge_{i\\le j+1} \\{\\boxdot(p_i\\leftrightarrow A_i(p_1,...,p_n)\\}\\rightarrow \\wedge_{i\\le j+1} \\{\\boxdot(p_i\\leftrightarrow H_i'(p_{j+2},...,p_n))\\}$.\n\nBy [ Goldfarb's lemma], we do not need to check the other direction, so $GL\\vdash \\wedge_{i\\le j+1} \\{\\boxdot(p_i\\leftrightarrow A_i(p_1,...,p_n)\\}\\leftrightarrow \\wedge_{i\\le j+1} \\{\\boxdot(p_i\\leftrightarrow H_i'(p_{j+2},...,p_n))\\}$ and the proof is finished $\\square$\n\n----\n\nOne remark: the proof is wholly constructive. You can iterate the construction of fixed point following the procedure implied by the construction of the $H_i'$ to compute fixed points.\n\n%%\n\nAn immediate consequence of the theorem is that for those fixed points $H_i$ and every $A_i$, $GL\\vdash H_i\\leftrightarrow A_i(H_1,...,H_n)$.\n\nIndeed, since $GL$ is closed under substitution, we can make the change $p_i$ for $H_i$ in the theorem to get that $GL\\vdash \\wedge_{i\\le n} \\{\\boxdot (H_i\\leftrightarrow A_i(H_1,...,H_n)\\}\\leftrightarrow \\wedge_{i\\le n} \\{\\boxdot(H_i\\leftrightarrow H_i)\\}$.\n\nSince the righthand side is trivially a theorem of $GL$, we get the desired result.\n',
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: 'true',
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: {
Summary: '>Let $\\phi(p, q_1,...,q_n)$ be a modal sentence [5m4 modalized] in $p$. \n>Then there exists a sentence $H(q_1,..,q_n)$ such that $GL\\vdash \\boxdot[p\\leftrightarrow \\phi(p,q_1,...,q_n)] \\leftrightarrow \\boxdot[p\\leftrightarrow H(q_1,..,q_n)]$.\n\nThis result can be used to give us insight about [59c self-referent] sentences of arithmetic.'
},
creatorIds: [
'JaimeSevillaMolina'
],
childIds: [],
parentIds: [
'provability_logic'
],
commentIds: [],
questionIds: [],
tagIds: [
'work_in_progress_meta_tag'
],
relatedIds: [],
markIds: [],
explanations: [
{
id: '5665',
parentId: 'fixed_point_theorem_provability_logic',
childId: 'fixed_point_theorem_provability_logic',
type: 'subject',
creatorId: 'JaimeSevillaMolina',
createdAt: '2016-07-27 20:42:41',
level: '3',
isStrong: 'true',
everPublished: 'true'
}
],
learnMore: [],
requirements: [],
subjects: [
{
id: '5665',
parentId: 'fixed_point_theorem_provability_logic',
childId: 'fixed_point_theorem_provability_logic',
type: 'subject',
creatorId: 'JaimeSevillaMolina',
createdAt: '2016-07-27 20:42:41',
level: '3',
isStrong: 'true',
everPublished: 'true'
}
],
lenses: [],
lensParentId: '',
pathPages: [],
learnMoreTaughtMap: {},
learnMoreCoveredMap: {},
learnMoreRequiredMap: {
'5lx': [
'655'
]
},
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: '22226',
pageId: 'fixed_point_theorem_provability_logic',
userId: 'JaimeSevillaMolina',
edit: '8',
type: 'newEdit',
createdAt: '2017-03-02 16:00:20',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '19721',
pageId: 'fixed_point_theorem_provability_logic',
userId: 'JaimeSevillaMolina',
edit: '7',
type: 'newEdit',
createdAt: '2016-09-25 09:57:14',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17689',
pageId: 'fixed_point_theorem_provability_logic',
userId: 'JaimeSevillaMolina',
edit: '6',
type: 'newEdit',
createdAt: '2016-07-28 19:26:16',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17632',
pageId: 'fixed_point_theorem_provability_logic',
userId: 'JaimeSevillaMolina',
edit: '6',
type: 'newEdit',
createdAt: '2016-07-28 08:33:12',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17631',
pageId: 'fixed_point_theorem_provability_logic',
userId: 'JaimeSevillaMolina',
edit: '5',
type: 'newEdit',
createdAt: '2016-07-28 08:23:48',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: 'A-traces'
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17614',
pageId: 'fixed_point_theorem_provability_logic',
userId: 'JaimeSevillaMolina',
edit: '4',
type: 'newEdit',
createdAt: '2016-07-27 21:03:57',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17613',
pageId: 'fixed_point_theorem_provability_logic',
userId: 'JaimeSevillaMolina',
edit: '3',
type: 'newEdit',
createdAt: '2016-07-27 20:51:18',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17610',
pageId: 'fixed_point_theorem_provability_logic',
userId: 'JaimeSevillaMolina',
edit: '2',
type: 'newEdit',
createdAt: '2016-07-27 20:43:34',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17608',
pageId: 'fixed_point_theorem_provability_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newTeacher',
createdAt: '2016-07-27 20:42:41',
auxPageId: 'fixed_point_theorem_provability_logic',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17609',
pageId: 'fixed_point_theorem_provability_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newSubject',
createdAt: '2016-07-27 20:42:41',
auxPageId: 'fixed_point_theorem_provability_logic',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17607',
pageId: 'fixed_point_theorem_provability_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newParent',
createdAt: '2016-07-27 20:42:36',
auxPageId: 'provability_logic',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17605',
pageId: 'fixed_point_theorem_provability_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newTag',
createdAt: '2016-07-27 20:42:24',
auxPageId: 'work_in_progress_meta_tag',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17604',
pageId: 'fixed_point_theorem_provability_logic',
userId: 'JaimeSevillaMolina',
edit: '1',
type: 'newEdit',
createdAt: '2016-07-27 20:41:53',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
}
],
feedSubmissions: [],
searchStrings: {},
hasChildren: 'false',
hasParents: 'true',
redAliases: {},
improvementTagIds: [],
nonMetaTagIds: [],
todos: [],
slowDownMap: 'null',
speedUpMap: 'null',
arcPageIds: 'null',
contentRequests: {}
}