The logic of proofs, semantically

A new semantics is presented for the logic of proofs (LP), (Technical Report MSI 95-29, Cornell University (1995), Bull. Symbolic Logic 7 (2001) 1) based on the intuition that it is a logic of explicit knowledge. This semantics is used to give new proofs of several basic results concerning LP. In particular, the realization of S4 into LP is established in a way that carefully examines and explicates the role of the + operator. Finally connections are made with the conventional approach, via soundness and completeness results.