Logic of Proofs for Bounded Arithmetic

The logic of proofs is known to be complete for the semantics of proofs in 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 S1 2.

• Type: Conference
• Year: 2006
• Where: CSR
• Authors: Evan Goris
• Keywords: CSR 2006, Logic, Paper, Semantics, Theoretical Computer Science