Provability logic studies modal principles valid when is interpreted by an arithmetical provability predicate. The distribution axiom corresponds to formalized modus ponens rule, necessitation corresponds to verification of actual proofs, and the Löb axiom is the Internal form of Löb's theorem. The standard system capturing these principles is Gödel-Löb logic.
Provability logic is a branch of mathematical logic that studies formal systems of provability. Specifically, it deals with the properties and behaviors of provability predicates, which are statements or operators that express the idea that a certain statement is provable within a given formal system. One of the most prominent systems within provability logic is known as Gödel's provability logic, often represented by the modal system \( GL \) (Gödel-Löb logic).
New to topics? Read the docs here!