 Propositional provability logic is often called GL, after Gödel and Löb. (Alternative names found in the literature for equivalent systems are L, G, KW, K4W, and PrL). The logic GL results from adding the following axiom to the basic modal logic K: