Knowra Löb's theorem Löb's theorem Löb's theorem states that, in a sufficiently strong formal theory, proving that a sentence’s provability implies the sentence entails proving the sentence itself. It is a key result about formal provability and self-reference.
Hilbert–Bernays–Löb derivability conditions : Three formal conditions governing how a theory’s provability predicate interacts with implication and provability. They let the theory reason about its own proof predicate in the derivation.
Peano arithmetic : A formal axiomatic theory of the natural numbers, including induction principles. It is a standard example of a sufficiently strong theory for arithmetized provability.
Gödel's incompleteness theorems : Results showing limits on what sufficiently expressive, consistent formal theories can prove about arithmetic and their own consistency. Löb’s theorem uses related self-reference and provability methods but yields a distinct conditional conclusion.
Provability logic : The study of modal principles describing provability in formal arithmetic theories. Löb’s theorem motivates its characteristic axiom and helps characterize the logic GL.
Diagonal lemma : A result guaranteeing, under suitable conditions, a sentence equivalent to a formula that names that sentence. It supplies the self-referential sentence used to derive Löb’s theorem.
First-order logic : A formal logic with variables, predicates, quantifiers, and rules for deriving consequences. Löb’s theorem is formulated within formal systems whose reasoning can be represented logically.
Gödel's second incompleteness theorem : A theorem stating that a consistent, sufficiently strong theory cannot prove its own formalized consistency under standard conditions. It is a famous consequence of Löb’s theorem, rather than the same result.
Gödel–Löb provability logic : The modal logic GL, whose theorems capture principles of provability for suitable arithmetic theories. It formalizes Löb’s theorem alongside other valid principles of provability.
Provability predicate : A formula in an arithmetic theory that expresses that a sentence has a formal proof in that theory. Löb’s theorem concerns what a theory can prove about this formula.
Consistency : The property of a formal theory having no contradiction derivable from its axioms. Consistency is a central background condition in results about formal provability, though not the theorem’s conclusion.
Show all 20