provability

Provability is the relation between a statement and a formal system: a statement φ is provable in a theory T if there exists a finite derivation of φ from the axioms of T using its inference rules. The set of provable statements, theorems of T, depends on the chosen axioms and rules; in any given system, there are true statements that are unprovable within it. In mathematics and logic, attention is often given to formal theories that can express arithmetic, such as Peano Arithmetic (PA).

To study provability, logicians formalize a provability predicate Pr_T(x) expressing that x is the Gödel number of a theorem of T. With Gödel numbering one can prove metatheorems about provability, including Löb's theorem: if T proves that 'if φ is provable, then φ', then T proves φ, for φ in the language of T.

Gödel's incompleteness theorems show fundamental limits: if T is consistent and strong enough to formalize arithmetic, there exist true arithmetical statements that T does not prove; and T cannot prove its own consistency (second incompleteness theorem). These results imply that no sufficiently powerful formal system can capture all mathematical truth, nor certify its own reliability from within.

Provability logic, or GL, is a modal logic that formalizes the behavior of the provability operator □. In GL, □φ is interpreted as 'φ is provable in T'. The axioms include Löb's axiom and rules reflecting that provability is closed under logical consequence. Semantics use Kripke frames capturing the relative strength of theories, enabling analysis of reflection principles and other metatheoretical questions about provability.

The notion of provability informs automated theorem proving, formal verification, and the study of proof systems such as Hilbert-style, natural deduction, or sequent calculus. It remains central to investigations of mathematical foundations and the limits of formal reasoning.