Feasible operations on proofs: the logic of proofs for bounded arithmetic (Q929293)

The logic of proofs (LP), introduced by \textit{S. Artemov} [Technical Report MSI 95-29, Cornell University (1995)], is a constructive variant of provability logic which has explicit proof terms instead of the provability operator. It has found applications in epistemic logics, where proof terms can be reinterpreted as terms providing explicit justification for knowledge of a formula. In this paper, the author adapts Artemov's arithmetical completeness proof for LP to show completeness with respect to arithmetical interpretations in Buss's bounded arithmetical theory \(S^1_2\). In particular, LP is complete with respect to semantics where proof terms represent feasible (polynomial-time computable) functions.