Modal logic is a \(\square\)) and possibility (\(\diamond\)).noteThere are more with different modal predicates out there.in which we expand with two new operators meant to represent necessity (
Those two operators can be defined in terms of each other. For example, we have that something is possible iff it is not necessary that its opposite is true; ie, \(\diamond A \iff \neg \square \neg A\).
Thus in modal logic, you can express sentences as \(\square A\) to express that it is necessary that \(A\) is true. You can also go more abstract and say \(\neg\square \bot\) to express that it is not necessary that false is true. If we read the box operator as “there is no mathematical proof of” then the previous sentence becomes “there is no mathematical proof of falsehood”, which encodes the .
There are many systems of modal logic noteSee for example , , , , , , which differ in the sentences they take as and which they allow.
Of particular interest are the systems called normal systems of modal logic, and especially the \(Gödel-Löb\) system (called \(GL\) for short, also known as the logic of provability). The main interest of \(GL\) comes from being a logic which allows us to reason about sentences of Peano arithmetic talking about provability via , as proved by the .
Another widely studied system of modal logic is \(GLS\), for which Solomonov proved in the .
Theof the normal systems of modal logic come in the form of : digraph structures composed of worlds over which a visibility relation is defined.
Well formed sentences of modal logic are defined as follows:
\(\bot\) is a well-formed sentence of modal logic.
The sentence letters \(p,q,...\) are well-formed sentences of modal logic.
If \(A\) is a well-formed sentence, then \(\square A\) is a well-formed sentence.
If \(A\) and \(B\) are well formed sentences, then \(A\to B\) is a well-formed sentence.
The rest of \(\bot\). For example , \(\neg A = A\to \bot\). The possibility operator \(\diamond\) is defined as \(\neg\square\neg\) as per the previous discussion.can then be defined as abbreviations for structures made from implication and
- Standard provability predicate
Encoding provability as a statement of arithmetic
- Normal system of provability logic
- Provability logic
Learn how to reason about provability!
- Kripke model
The semantics of modal logic
- Modalized modal sentence
- Modal combat
Mathematics is the study of numbers and other ideal objects that can be described by axioms.