= Gödel-Löb logic
{c}
{title2=$\mathrm{GL}$}
= GL
{c}
{synonym}
The <Gödel-Löb logic> has propositional tautologies, $\Box(A\to B)\to(\Box A\to\Box B)$ and $\Box(\Box A\to A)\to\Box A$ as axiom schemes. Its rules are <modus ponens rule> and the <necessitation rule>; uniform <propositional substitution> is built into the schemes. Under an arithmetic realization, each axiom and each rule preserves provability in a theory with the <Hilbert-Bernays-Löb derivability conditions> and diagonalization. This proves arithmetic soundness by induction on derivations; it is distinct from claiming that every true arithmetic sentence is provable.
Back to article page
