Gödel Sentences of Bounded Arithmetic

Gaisi Takeuti


In his early work, Feferman emphasized that the arithmetization of metamathematics must be carried out intensionally. Bounded Arithmetic is a very interesting case in this sense. We present two formalizations of proof predicate of Bounded Arithmetic. One of them is the usual proof predicate and another one gives a detailed information on bounds of free variables used in the proof. Now Bounded Arithmetic has the following special feature of Gödel sentences. Even if we fix one formalization of proof predicate, it has infinitely many Gödel sentences and their properties and their mutual relations are closely related to the P=/=NP problem. Therefore the study of Gödel sentences of Bounded Arithmetic is an excellent approach to the P=/=NP problem. In our two formalizations of proof predicate of Bounded Arithmetic we show that the properties of their Gödel sentences form a good contrast to each other and discuss how P=/=NP problem is related to their properties.