Gödel Sentences of Bounded Arithmetic
Gaisi Takeuti
Abstract
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.