Embedding of the Modal $\lambda$-Calculus into the Logic of Proofs

The Logic of Proofs LP introduced by the author may be regarded as a basic formal system for reasoning about propositions and proofs. LP comes from Gödel's calculus of provability, also known as modal logic S4 to which P. S. Novikov devoted the well-known monograph Constructive Mathematical Logic from the Point of View of the Classical One. LP gives an exact mathematical answer to the question of the provability semantics of S4 raised by Gödel. This paper gives a comparison of the expressive powers of LP, the typed $\lambda$-calculus, and the modal $\lambda$-calculus. It is shown that a small (namely, Horn) fragment of LP is sufficient for a natural embedding of the typed $\lambda$-calculus. It is also shown that LP models the modal $\lambda$-calculus.