{
localUrl: '../page/provability_logic.html',
arbitalUrl: 'https://arbital.com/p/provability_logic',
rawJsonUrl: '../raw/5l3.json',
likeableId: '3283',
likeableType: 'page',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [
'EricBruylant'
],
pageId: 'provability_logic',
edit: '6',
editSummary: '',
prevEdit: '5',
currentEdit: '6',
wasPublished: 'true',
type: 'wiki',
title: 'Provability logic',
clickbait: 'Learn how to reason about provability!',
textLength: '7477',
alias: 'provability_logic',
externalUrl: '',
sortChildrenBy: 'likes',
hasVote: 'false',
voteType: '',
votesAnonymous: 'false',
editCreatorId: 'JaimeSevillaMolina',
editCreatedAt: '2016-07-26 10:44:04',
pageCreatorId: 'JaimeSevillaMolina',
pageCreatedAt: '2016-07-25 13:24:42',
seeDomainId: '0',
editDomainId: 'AlexeiAndreev',
submitToDomainId: '0',
isAutosave: 'false',
isSnapshot: 'false',
isLiveEdit: 'true',
isMinorEdit: 'false',
indirectTeacher: 'false',
todoCount: '10',
isEditorComment: 'false',
isApprovedComment: 'true',
isResolved: 'false',
snapshotText: '',
anchorContext: '',
anchorText: '',
anchorOffset: '0',
mergedInto: '',
isDeleted: 'false',
viewCount: '51',
text: 'The Gödel -Löb system of provability logic, or $GL$ for short, is a [-5j8] which captures important notions about [5j7 provability predicates]. It can be regarded as a formalism which allows to decide whether certain sentences in which a provability predicate appears are in fact theorems of [3ft].\n\n$GL$ has two rules of inference:\n\n* **Modus ponens** allows to infer $B$ from $A\\to B$ and $A$.\n* **Necessitation** says that if $GL\\vdash A$ then $GL\\vdash \\square A$.\n\nThe axioms of $GL$ are as follows:\n\n* $GL\\vdash \\square (A\\to B)\\to(\\square A \\to \\square B)$ (**Distibutive axioms**)\n* $GL\\vdash \\square (\\square A \\to A)\\to \\square A$ (**Gödel-Löb axioms**)\n* Propositional tautologies are axioms of $GL$.\n\n**Exercise**: Show using the rules of $GL$ that $\\square \\bot \\leftrightarrow \\square \\diamond p$. %%note:$\\diamond p$ is short for $\\neg \\square \\neg p$.%%\n\n%%hidden(Show solution):\nThose problems are best solved by working backwards.\n\nWe want to show that $GL\\vdash \\square \\bot \\leftrightarrow \\square \\diamond p$.\n\nWhat can lead us to that? Well, we know that because of [ normality], this can be deduced from $GL\\vdash \\square (\\bot \\leftrightarrow \\diamond p)$.\n\nSimilarly, that can be derived from necessitation of $GL\\vdash \\bot \\leftrightarrow \\diamond p$.\n\nThe propositional calculus shows that $GL\\vdash \\bot \\to \\diamond p$ is a tautology, so we can prove by following the steps backward that $GL\\vdash \\square \\bot \\to \\square \\diamond p$.\n\nNow we have to prove that $GL\\vdash \\square \\diamond p\\to \\square \\bot$ and we are done.\n\nFor that we are going to go forward from the tautology $GL\\vdash \\bot \\to \\neg p$. \n\nBy normality, $GL\\vdash \\square \\bot \\to \\square \\neg p$.\n\nContraposing, $Gl\\vdash \\neg \\square \\neg p\\to\\neg\\square\\bot$. By necessitation and normality, $Gl\\vdash \\square \\neg \\square \\neg p\\to\\square \\neg\\square\\bot$.\n\nBut $\\square\\neg\\square\\bot$ is equivalent to $\\square[\\square \\bot \\to \\bot]$, and it is an axiom that $GL\\vdash \\square[\\square \\bot \\to \\bot] \\to\\square \\bot$, so by modus ponens, $Gl\\vdash \\square \\neg \\square \\neg p\\to\\square \\bot$, and since $\\diamond p = \\neg \\square \\neg p$ we are done.\n%%\n\nIt is fairly easy to see that GL is consistent. If we interpret $\\square$ as the verum operator which is always true, we realize that every theorem of $GL$ is assigned a value of true according to this interpretation and the usual rules of propositional calculus %%note:[ proof] %%. However, there are well formed modal sentences such as $\\neg \\square \\bot$ such that the assigned value is false, and thus they cannot be theorems of $GL$.\n\n##Semantics\nHowever simple the deduction procedures of $GL$ are, they are bothersome to use in order to find proofs. Thankfully, an alternative interpretation in terms of [5ll Kripke models] has been developed that allows to decide far more conveniently whether a modal sentence is a theorem of $GL$.\n\n$GL$ is adequate for finite, transitive and irreflexive Kripke models. That is, a sentence $A$ is a theorem of $GL$ if and only if $A$ is valid in every finite, transitive and irreflexive model%%note: [ proof]%%. Check out the page on Kripke models if you do not know how to construct Kripke models or decide if a sentence is valid in it.\n\nAn important notion in this kind of models is that of *rank*. The rank $\\rho$ of a world $w$ from which no world is visible is $\\rho(w)=0$. The rank of any other world is defined as the maximum among the ranks of its successors, plus one. In other words, the rank of a world is the length of the greatest "chain of worlds" in the model such that $w$ can view the first slate of the chain. \n\nSince models are irreflexive and finite, the rank is a well-defined notion: no infinite chain of worlds is ever possible.\n\n**Exercise**: Show that the Gödel-Löb axioms are valid in every finite, transitive and irreflexive Kripke model.\n\n%%hidden(Show solution):\nSuppose there is a finite, transitive and irreflexive Kripke model in which an sentence of the form $\\square[\\square A\\to A]\\to \\square A$ is not valid.\n\nLet $w$ be the lowest rank world in the model such that $w\\not\\models \\square[\\square A\\to A]\\to \\square A$. Then we have that $w\\models \\square[\\square A\\to A]$ but $w\\not \\models \\square A$.\n \nTherefore, there exists $x$ such that $w R x$, also $x\\models \\neg A$ and $x\\models \\square A\\to A$. But then $x\\models \\neg\\square A$.\n\nSince $x$ has lower rank than $w$, we also have that $x\\models \\square[\\square A\\to A]\\to \\square A$. Combining those two last facts we get that $x\\not\\models \\square[\\square A\\to A]$, so there is $y$ such that $xRy$ and $y\\not\\models \\square A\\to A$.\n\nBut by transitivity $wRy$, contradicting that $w\\models \\square[\\square A\\to A]$. So the supposition was false, and the proof is done.\n%%\n\nThe Kripke model formulation specially simplifies reasoning in cases in which [constant_sentences no sentence letters appear]. A polynomial time algorithm can be written for deciding theoremhood this case.\n\nFurthermore, $GL$ is [-decidable]. However, it is [ $PSPACE$-complete] %%note:[ proof]%%.\n\n##Arithmetical adequacy\nYou can translate sentences of modal logic to sentences of arithmetic using *realizations*.\n\nA realization $*$ is a function such that \n$A\\to B*=A*\\to B*$, \n$(\\square A)* =\\square_{PA}(A*)$, \nand $p* = S_p$ for every sentence letter $p$, where each $S_p$ is an arbitrary well formed closed sentence of arithmetic.\n\n[ Solovay's adequacy theorem for GL] states that a modal sentence $A$ is a theorem of $GL$ iff $PA$ proves $A*$ for every realization $*$.\n\nThus we can use $GL$ to reason about arithmetic and viceversa.\n\nNotice that $GL$ is decidable while [ arithmetic is not]. This is explained by the fact that $GL$ only deals with a specific subset of logical sentences, in which quantification plays a restricted role. In fact, quantified provability logic is undecidable.\n\nAnother remark is that while knowing that $GL\\not\\vdash A$ implies that there is a realization such that $PA\\not\\vdash A*$, we do not know whether a specific realization of A is a theorem or not. A related result, the [ uniform completeness theorem for $GL$], proves that there exists a specific realization $\\#$ such that $PA\\not \\vdash A^{\\#}$ if $GL\\not\\vdash A$, which works for every $A$.\n\n##Fixed points\nOne of the most important results in $GL$ is the existence of fixed points of sentences of the form $p\\leftrightarrow \\phi(p)$. Concretely, the [ fixed point theorem] says that for every sentence $\\phi(p)$ modalized in $p$ %%note:that is, every $p$ occurs within the scope of a $\\square$%% there exists $H$ in which $p$ does not appear such that $GL\\vdash \\square [p\\leftrightarrow \\phi(p)] \\leftrightarrow \\square (p\\leftrightarrow h)$. Furthermore, there are constructive proofs which allow to build such an $H$.\n\nIn arithmetic, there are plenty of interesting [59c self referential sentences] such as the [godel_first_incompleteness_theorem Gödel sentence] for which the fixed point theorem is applicable and gives us insights about their meaning.\n\nFor example, the modalization of the Gödel sentence is something of the form $p\\leftrightarrow \\neg\\square p$. The procedure for finding fixed points tells us that $GL\\vdash \\square (p\\leftrightarrow \\neg\\square p)\\to \\square(p\\leftrightarrow \\neg\\square\\bot$. Thus by arithmetical adequacy, and since [ everything $PA$ proves is true] we can conclude that the Gödel sentence is equivalent to the [5km consistency of arithmetic].',
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',
'DylanHendrickson'
],
childIds: [
'fixed_point_theorem_provability_logic',
'arithmetical_adequacy_GL'
],
parentIds: [
'modal_logic'
],
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: '17717',
pageId: 'provability_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newChild',
createdAt: '2016-07-29 12:53:06',
auxPageId: 'arithmetical_adequacy_GL',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17714',
pageId: 'provability_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newAlias',
createdAt: '2016-07-29 10:59:03',
auxPageId: '',
oldSettingsValue: 'gl_provability_logic',
newSettingsValue: 'provability_logic'
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17606',
pageId: 'provability_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newChild',
createdAt: '2016-07-27 20:42:36',
auxPageId: 'fixed_point_theorem_provability_logic',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17518',
pageId: 'provability_logic',
userId: 'JaimeSevillaMolina',
edit: '6',
type: 'newEdit',
createdAt: '2016-07-26 10:44:04',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17508',
pageId: 'provability_logic',
userId: 'JaimeSevillaMolina',
edit: '5',
type: 'newEdit',
createdAt: '2016-07-25 20:43:57',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '3232',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '2',
dislikeCount: '0',
likeScore: '2',
individualLikes: [],
id: '17504',
pageId: 'provability_logic',
userId: 'DylanHendrickson',
edit: '4',
type: 'newEdit',
createdAt: '2016-07-25 19:41:15',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17492',
pageId: 'provability_logic',
userId: 'JaimeSevillaMolina',
edit: '3',
type: 'newEdit',
createdAt: '2016-07-25 17:40:11',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17489',
pageId: 'provability_logic',
userId: 'JaimeSevillaMolina',
edit: '0',
type: 'newParent',
createdAt: '2016-07-25 17:10:55',
auxPageId: 'modal_logic',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17487',
pageId: 'provability_logic',
userId: 'JaimeSevillaMolina',
edit: '2',
type: 'newEdit',
createdAt: '2016-07-25 17:10:18',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17485',
pageId: 'provability_logic',
userId: 'JaimeSevillaMolina',
edit: '1',
type: 'newEdit',
createdAt: '2016-07-25 13:24:42',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
}
],
feedSubmissions: [],
searchStrings: {},
hasChildren: 'true',
hasParents: 'true',
redAliases: {},
improvementTagIds: [],
nonMetaTagIds: [],
todos: [],
slowDownMap: 'null',
speedUpMap: 'null',
arcPageIds: 'null',
contentRequests: {}
}