Logic of proofs for bounded arithmetic

Abstract

The logic of proofs is known to be complete for the semantics of proofs in Peano Arithmetic PA. In this paper we present a refinement of this theorem, we will show that we can assure that all the operations on proofs can be realized by feasible, that is PTIME-computable, functions. In particular we will show that the logic of proofs is complete for the semantics of proofs in Buss' bounded arithmetic S 2 1. In view of recent applications of the Logic of Proofs in epistemology this result shows that explicit knowledge in the propositional framework can be made computationally feasible. © Springer-Verlag Berlin Heidelberg 2006.