Provability logic
= Provability logic
{wiki}
<Provability logic> studies modal principles valid when $\Box A$ 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>.