# Martin Löb

**Martin Hugo Löb** (31 March 1921 – August 2006) was a German-born mathematical logician who spent his career in Britain and the Netherlands, best known for [Löb's theorem](https://www.edgepedia.org/lobs-theorem) of 1955 and for developing the Leeds logic group into one of the leading centers in the UK and helping to establish logic at Amsterdam.<sup>[1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries)</sup><sup> • </sup><sup>[2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html)</sup> The Association for Symbolic Logic called him "a central figure in the early development of Mathematical Logic in the United Kingdom."<sup>[3](https://aslonline.org/files/newsletters/pdfs/april2007newsletter.pdf)</sup>

| Key fact | Detail |
|---|---|
| Born / died | 31 March 1921; died August 2006 in the Netherlands, aged 85 (21 August per the Guardian and ASL, 28 August per the Amsterdam memorial) <sup>[1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries)</sup><sup> • </sup><sup>[3](https://aslonline.org/files/newsletters/pdfs/april2007newsletter.pdf)</sup><sup> • </sup><sup>[2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html)</sup> |
| Signature result | Löb's theorem (1955): for a sufficiently strong theory, proving Prov(⌜A⌝) → A entails that it already proves A <sup>[4](https://plato.stanford.edu/entries/goedel-incompleteness/)</sup> |
| Doctorate | Ph.D., University of London, 1953, thesis *A Methodological Characterization of Constructive Mathematics*, advised by R. L. Goodstein <sup>[5](https://www.mathgenealogy.org/id.php?id=42265)</sup> |
| Leeds | Assistant Lecturer 1951, then Reader and Professor of Mathematical Logic, twenty years <sup>[1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries)</sup> |
| Amsterdam | Chair of Mathematical Logic, 1971–1985, in the line of Evert Beth <sup>[2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html)</sup><sup> • </sup><sup>[1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries)</sup> |
| Named after him | The Gödel–Löb provability logic GL, whose axiom is □(□A → A) → □A <sup>[6](https://plato.stanford.edu/entries/logic-provability/)</sup> |

## Life and career

Löb was brought up in Berlin; the Nazis came to power in 1933, when he was twelve. In 1939, just before the Second World War began, he escaped to England.<sup>[7](https://mathshistory.st-andrews.ac.uk/Biographies/Lob/)</sup> As a German national he was classed an "enemy alien", and in 1940 he was deported on the transport ship *Dunera* to an internment camp at Hay, on the Murrumbidgee River in the Australian outback.<sup>[7](https://mathshistory.st-andrews.ac.uk/Biographies/Lob/)</sup><sup> • </sup><sup>[2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html)</sup> There, at age 19, he began learning advanced mathematics and logic at the "camp university" set up by the older academic refugees interned alongside him.<sup>[3](https://aslonline.org/files/newsletters/pdfs/april2007newsletter.pdf)</sup>

The British government acknowledged its mistake in enforcing the internments, and it was three years before Löb could return to the UK.<sup>[1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries)</sup><sup> • </sup><sup>[7](https://mathshistory.st-andrews.ac.uk/Biographies/Lob/)</sup> In 1945 he began a part-time degree at the [University of London](https://www.edgepedia.org/university-of-london) while teaching at a boarding school.<sup>[7](https://mathshistory.st-andrews.ac.uk/Biographies/Lob/)</sup> A research studentship was advertised to work under R. L. Goodstein at [Leicester](https://www.edgepedia.org/leicester); Löb got it, and his Ph.D. followed, awarded by the University of London in 1953 for the thesis *A Methodological Characterization of Constructive Mathematics*.<sup>[1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries)</sup><sup> • </sup><sup>[5](https://www.mathgenealogy.org/id.php?id=42265)</sup>

**Leeds and Amsterdam.** By 1951, at age 30, Löb was an Assistant Lecturer at the [University of Leeds](https://www.edgepedia.org/university-of-leeds), where he stayed twenty years, becoming Reader and then Professor of Mathematical Logic.<sup>[1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries)</sup> In the early 1970s he accepted the chair of Mathematical Logic at the [University of Amsterdam](https://www.edgepedia.org/university-of-amsterdam), previously held by Evert Beth, and held it from 1971 to 1985, retiring at 65.<sup>[2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html)</sup><sup> • </sup><sup>[1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries)</sup> In Amsterdam he and Anne Troelstra occupied the two central logic chairs, succeeding Beth and Heyting; Löb helped create the interdisciplinary *vakgroep* that was the predecessor of today's Institute for Logic, Language and [Computation](https://www.edgepedia.org/computation) (ILLC).<sup>[2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html)</sup> He died in Annen, in the Dutch province of Drente, after a lengthy illness.<sup>[2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html)</sup><sup> • </sup><sup>[3](https://aslonline.org/files/newsletters/pdfs/april2007newsletter.pdf)</sup>

## Löb's theorem

Leon Henkin had asked about sentences that "express their own provability": if a sentence says "this statement is provable in T", is it provable in T? Löb answered the question in his 1955 paper, showing that, for a sufficiently strong theory T satisfying the relevant derivability conditions (technical axioms a theory must satisfy for provability theorems to apply), such a sentence is indeed provable in T.<sup>[7](https://mathshistory.st-andrews.ac.uk/Biographies/Lob/)</sup><sup> • </sup><sup>[4](https://plato.stanford.edu/entries/goedel-incompleteness/)</sup> The paper's general result, now called Löb's theorem, states that for any sentence A of the language of a sufficiently strong theory F satisfying the relevant derivability conditions:

\[ F \vdash \mathrm{Prov}_{F}(\ulcorner A \urcorner) \rightarrow A \quad \text{if and only if} \quad F \vdash A. \]

In plain terms, a sufficiently strong theory satisfying the relevant derivability conditions can prove "if A is provable then A" only in the trivial case that the theory already proves A itself.<sup>[4](https://plato.stanford.edu/entries/goedel-incompleteness/)</sup><sup> • </sup><sup>[6](https://plato.stanford.edu/entries/logic-provability/)</sup> The theorem is associated with Löb's Paradox, illustrated by the sentence "if this sentence is true then the moon is made of green cheese".<sup>[2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html)</sup>

**Attribution and derivability conditions.** The 1955 paper brought three advances: it introduced the now-standard Löb derivability conditions, a useful simplification of the complicated conditions Hilbert and Bernays had introduced in 1939; it solved Henkin's problem; and it contained the generalization now called Löb's Theorem, which Löb himself credited to the anonymous referee of the paper, who happened to be Henkin.<sup>[4](https://plato.stanford.edu/entries/goedel-incompleteness/)</sup> Substituting the falsum symbol ⊥ for A in the theorem yields that PA ⊢ ¬Prov(⌜⊥⌝) implies PA ⊢ ⊥, which is exactly the contraposition of Gödel's second incompleteness theorem: the theorem is, in this sense, a strengthening of Gödel's result.<sup>[6](https://plato.stanford.edu/entries/logic-provability/)</sup>

## Provability logic and its aftermath

The modal face of Löb's theorem is the axiom □(□A → A) → □A. Adding it to the minimal modal logic K yields the propositional provability logic called **GL**, after Gödel and Löb (alternative names in the literature are L, G, KW, K4W, and PrL).<sup>[6](https://plato.stanford.edu/entries/logic-provability/)</sup> Ironically, the first statement of the formalized Löb theorem as a modal principle appeared not in arithmetic but in a 1963 paper by T. Smiley on the logical basis of ethics; serious investigation of provability logic began only in the early 1970s.<sup>[6](https://plato.stanford.edu/entries/logic-provability/)</sup>

The main modal result about GL is the fixed point theorem, proved independently by Dick de Jongh and Giovanni Sambin in 1975: for any p-modalized formula A(p) there is a fixed point B, unique up to GL-provable equivalence, with GL ⊢ B ↔ A(B), and the fixed point can be found by an effective procedure.<sup>[6](https://plato.stanford.edu/entries/logic-provability/)</sup><sup> • </sup><sup>[8](https://eprints.illc.uva.nl/id/eprint/1774/7/2021.FPT.jb.pdf)</sup> The field was consolidated in George Boolos's *The Logic of Provability* ([Cambridge University Press](https://www.edgepedia.org/cambridge-university-press), 1995), a fully rewritten successor to his *The Unprovability of Consistency* (1979), which shows how modal concepts and techniques illuminate [Gödel's incompleteness theorems](https://www.edgepedia.org/godels-incompleteness-theorems) by reinterpreting necessity and possibility as provability and consistency.<sup>[9](https://www.cambridge.org/core/books/logic-of-provability/F1549530F91505462083CE2FEB6444AA)</sup>

## Wider contributions, students and lineage

At Leeds, joined briefly by Robin Gandy, Löb established the BA in [Mathematics](https://www.edgepedia.org/mathematics) and [Philosophy](https://www.edgepedia.org/philosophy) and ran the early international conferences that brought distinguished senior logicians such as [Alonzo Church](https://www.edgepedia.org/alonzo-church) and Alfred Tarski to Britain; he developed the Leeds logic group into one of the leading centers in the UK, working on proof theory, modal logic, and computability theory.<sup>[1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries)</sup><sup> • </sup><sup>[7](https://mathshistory.st-andrews.ac.uk/Biographies/Lob/)</sup> His published work beyond the 1955 theorem includes "Extensional interpretations of modal logics" in the *Journal of Symbolic Logic*, volume 31 (1966), pages 23–45.<sup>[10](https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/m-h-lob-extensional-interpretations-of-modal-logics-the-journal-of-symbolic-logic-vol-31-1966-pp-2345/EFAB8663DD6652C4875BFB8E09CCEF0A)</sup> His best-known Amsterdam result is the undecidability of intuitionistic second-order propositional logic, even when the language contains only implication and the universal quantifier.<sup>[2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html)</sup>

The Mathematics Genealogy Project records 3 students and 431 mathematical descendants.

## By the numbers

- 431 mathematical descendants from 3 students.<sup>[5](https://www.mathgenealogy.org/id.php?id=42265)</sup>
- 20 years at Leeds (1951 to the early 1970s) and a 14-year Amsterdam chair (1971–1985).<sup>[1](https://www.theguardian.com/science/2006/oct/03/uk.obituaries)</sup><sup> • </sup><sup>[2](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html)</sup>
- The theorem is dated 1955 by most sources, though the Stanford Encyclopedia's provability logic entry dates it to 1953.<sup>[4](https://plato.stanford.edu/entries/goedel-incompleteness/)</sup><sup> • </sup><sup>[6](https://plato.stanford.edu/entries/logic-provability/)</sup>
- Gödel's second incompleteness theorem has been mechanized in a proof assistant only once, by Lawrence Paulson in 2015 in Isabelle; Löb's theorem itself has since been mechanized in Rocq.<sup>[11](https://msp-strath.github.io/MSPweb/types2025/slides/TYPES2025-slides17.pdf)</sup>

## Recent developments

The theorem has remained a working tool. A 2023 *Journal of Automated Reasoning* paper implemented the metatheory of GL in the HOL Light proof assistant, covering soundness and completeness for possible-world semantics with a prototype theorem prover, adapting the completeness proof from Boolos's 1995 monograph and overcoming the technical difficulty of GL's non-compactness.<sup>[12](https://link.springer.com/article/10.1007/s10817-023-09677-z)</sup> A TYPES 2025 presentation reported a mechanized proof of Löb's theorem for first-order arithmetic in the Rocq proof assistant, assuming the HBL derivability conditions and the consistency of the theory.<sup>[11](https://msp-strath.github.io/MSPweb/types2025/slides/TYPES2025-slides17.pdf)</sup>

**Type theory and AI.** Via the Curry–Howard isomorphism, which identifies formal proofs with abstract syntax trees of programs, Löb's theorem implies that for total programming languages which validate it, self-interpreters are impossible; a research paper formalizes variations of the theorem in Agda.<sup>[13](https://jasongross.github.io/lob-paper/nightly/lob.pdf)</sup> In AI foundations, a 2024 arXiv paper traces the "Löbian Obstacle", the problem named by Yudkowsky and Hereshoff (2013) concerning agents being confident in their own conclusions, to Löb (1955) and to Smullyan's doxastic-logic presentation (1986), and defines "Löb Safe" logics for reflective agents.<sup>[14](https://arxiv.org/html/2408.09590v2)</sup> MIRI's research program cites the 1955 theorem because it illustrates the self-reference involved when an algorithm considers its own output, making it germane to self-modifying agents and formal verification.<sup>[15](https://intelligence.org/files/lob-notes-IAFF.pdf)</sup>

## References

1. [Martin Löb, obituary by Stan Wainer, The Guardian (3 October 2006)](https://www.theguardian.com/science/2006/oct/03/uk.obituaries)
2. [Martin Löb (1921–2006), memorial notice, OZSL/ILLC Amsterdam](https://web.archive.org/web/20061223222900/http:/www.ozsl.uu.nl/MartinLob.html)
3. [In Memoriam: Martin Löb, Association for Symbolic Logic Newsletter, April 2007](https://aslonline.org/files/newsletters/pdfs/april2007newsletter.pdf)
4. [Gödel's Incompleteness Theorems, Stanford Encyclopedia of Philosophy](https://plato.stanford.edu/entries/goedel-incompleteness/)
5. [Martin Löb, The Mathematics Genealogy Project](https://www.mathgenealogy.org/id.php?id=42265)
6. [Provability Logic, Stanford Encyclopedia of Philosophy](https://plato.stanford.edu/entries/logic-provability/)
7. [Martin Löb, MacTutor History of Mathematics](https://mathshistory.st-andrews.ac.uk/Biographies/Lob/)
8. [An Abstract Look at the Fixed-Point Theorem for Provability Logic, ILLC preprint](https://eprints.illc.uva.nl/id/eprint/1774/7/2021.FPT.jb.pdf)
9. [George Boolos, The Logic of Provability, Cambridge University Press](https://www.cambridge.org/core/books/logic-of-provability/F1549530F91505462083CE2FEB6444AA)
10. [M. H. Löb, Extensional interpretations of modal logics, Journal of Symbolic Logic 31 (1966)](https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/m-h-lob-extensional-interpretations-of-modal-logics-the-journal-of-symbolic-logic-vol-31-1966-pp-2345/EFAB8663DD6652C4875BFB8E09CCEF0A)
11. [Löb's Theorem and Provability Predicates in Rocq, TYPES 2025 slides](https://msp-strath.github.io/MSPweb/types2025/slides/TYPES2025-slides17.pdf)
12. [Mechanising Gödel–Löb Provability Logic in HOL Light, Journal of Automated Reasoning (2023)](https://link.springer.com/article/10.1007/s10817-023-09677-z)
13. [Löb's Theorem (formalized in Agda), Gross et al.](https://jasongross.github.io/lob-paper/nightly/lob.pdf)
14. [Löb-Safe Logics for Reflective Agents, arXiv (2024)](https://arxiv.org/html/2408.09590v2)
15. [An Introduction to Löb's Theorem in MIRI Research](https://intelligence.org/files/lob-notes-IAFF.pdf)

---
*Topic: Encyclopedia › Physical world and mathematics › Physical and mathematical scientists › Mathematicians and statisticians › Logicians, set theorists, and combinatorialists › Proof theorists and foundational logicians*

*Initially written Oct 10, 2026 · Edited: Oct 11, 2026; Oct 15, 2026*

*Copyright 2026 EdgeChat AI, a subsidiary of Biostate AI.*

License: Edgepedia Community License 1.0, https://www.edgepedia.org/edgepedia/license