Modal logic

Mo­dal logic is a for­mal sys­tem in which we ex­pand propo­si­tional calcu­lus with two new op­er­a­tors meant to rep­re­sent ne­ces­sity ($\square$) and pos­si­bil­ity ($\di­a­mond$).noteThere are more gen­eral modal log­ics with differ­ent modal pred­i­cates out there.

Those two op­er­a­tors can be defined in terms of each other. For ex­am­ple, we have that some­thing is pos­si­ble iff it is not nec­es­sary that its op­po­site is true; ie, \(\diamond A \iff \neg \square \neg A\).

Thus in modal logic, you can ex­press sen­tences as \(\square A\) to ex­press that it is nec­es­sary that \(A\) is true. You can also go more ab­stract and say \(\neg\square \bot\) to ex­press that it is not nec­es­sary that false is true. If we read the box op­er­a­tor as “there is no math­e­mat­i­cal proof of” then the pre­vi­ous sen­tence be­comes “there is no math­e­mat­i­cal proof of false­hood”, which en­codes the con­sis­tency of ar­ith­metic.

There are many sys­tems of modal logic noteSee for ex­am­ple T,B,S5,S4,K, GLS, which differ in the sen­tences they take as ax­ioms and which rules of in­fer­ence they al­low.

Of par­tic­u­lar in­ter­est are the sys­tems called nor­mal sys­tems of modal logic, and es­pe­cially the \(Gödel-Löb\) sys­tem (called \(GL\) for short, also known as the logic of prov­abil­ity). The main in­ter­est of \(GL\) comes from be­ing a de­cid­able logic which al­lows us to rea­son about sen­tences of Peano ar­ith­metic talk­ing about prov­abil­ity via trans­la­tions, as proved by the ar­ith­meti­cal ad­e­quacy the­o­rems of Solomonov.

Another widely stud­ied sys­tem of modal logic is \(GLS\), for which Solomonov proved ad­e­quacy for truth in the stan­dard model of ar­ith­metic.

The se­man­tics of the nor­mal sys­tems of modal logic come in the form of Kripke mod­els: di­graph struc­tures com­posed of wor­lds over which a visi­bil­ity re­la­tion is defined.


Well formed sen­tences of modal logic are defined as fol­lows:

  • \(\bot\) is a well-formed sen­tence of modal logic.

  • The sen­tence let­ters \(p,q,...\) are well-formed sen­tences of modal logic.

  • If \(A\) is a well-formed sen­tence, then \(\square A\) is a well-formed sen­tence.

  • If \(A\) and \(B\) are well formed sen­tences, then \(A\to B\) is a well-formed sen­tence.

The rest of log­i­cal con­nec­tors can then be defined as ab­bre­vi­a­tions for struc­tures made from im­pli­ca­tion and \(\bot\). For ex­am­ple , \(\neg A = A\to \bot\). The pos­si­bil­ity op­er­a­tor \(\diamond\) is defined as \(\neg\square\neg\) as per the pre­vi­ous dis­cus­sion.



  • Mathematics

    Math­e­mat­ics is the study of num­bers and other ideal ob­jects that can be de­scribed by ax­ioms.