Feasible operations on proofs: The logic of proofs for bounded arithmetic
This paper presents a semantics for the logic of proofs LP in which all the operations on proofs are realized by feasibly computable functions. More precisely, we will show that the completeness of LP for the semantics of proofs of Peano Arithmetic extends to the semantics of proofs in Buss' bounded arithmetic S-2(1). In view of applications in epistemology of LP in particular and justification logics in general this result shows that explicit knowledge in the propositional framework can be made computationally feasible.
logic of proofs bounded arithmetic