Hilbert–Bernays provability conditions

From Wikipedia, the free encyclopedia
Jump to navigation Jump to search

In mathematical logic, the Hilbert–Bernays provability conditions, named after David Hilbert and Paul Bernays, are a set of requirements for formalized provability predicates in formal theories of arithmetic (Smith 2007:224).

These conditions are used in many proofs of Kurt Gödel's second incompleteness theorem. They are also closely related to axioms of provability logic.

The conditions[edit]

Let T be a formal theory of arithmetic with a formalized provability predicate Prov(n), which is expressed as a formula of T with one free number variable. For each formula φ in the theory, let #(φ) be the Gödel number of φ. The Hilbert–Bernays provability conditions are:

  1. If T proves a sentence φ then T proves Prov(#(φ)).
  2. For every sentence φ, T proves Prov(#(φ)) → Prov(#(Prov(#(φ))))
  3. T proves that Prov(#(φ → ψ)) and Prov(#(φ)) imply Prov (#(ψ))


  • Smith, Peter (2007). An introduction to Gödel's incompleteness theorems. Cambridge University Press. ISBN 978-0-521-67453-9