Hilbert–Bernays provability conditions
Encyclopedia
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
.
of φ. The Hilbert–Bernays provability conditions are:
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, the Hilbert–Bernays provability conditions, named after David Hilbert
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
and Paul Bernays
Paul Bernays
Paul Isaac Bernays was a Swiss mathematician, who made significant contributions to mathematical logic, axiomatic set theory, and the philosophy of mathematics. He was an assistant to, and close collaborator of, David Hilbert.-Biography:Bernays spent his childhood in Berlin. Bernays attended the...
, 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
Kurt Gödel
Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
's second incompleteness theorem. They are also closely related to axioms of provability logic
Provability logic
Provability logic is a modal logic, in which the box operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano arithmetic....
.
The conditions
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 numberGödel number
In mathematical logic, a Gödel numbering is a function that assigns to each symbol and well-formed formula of some formal language a unique natural number, called its Gödel number. The concept was famously used by Kurt Gödel for the proof of his incompleteness theorems...
of φ. The Hilbert–Bernays provability conditions are:
- If T proves a sentence φ then T proves Prov(#(φ)).
- For every sentence φ, T proves Prov(#(φ)) → Prov(#(Prov(#(φ))))
- T proves that Prov(#(φ → ψ)) and Prov(#(φ)) imply Prov (#(ψ))