Embedding of the modal λ-calculus into the logic of proofsстатья
Статья опубликована в журнале из перечня ВАК
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 26 августа 2016 г.
Аннотация: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 his well-known monograph [Constructive mathematical logic from the point of view of classical logic (Russian). Moskva: Nauka (1977)]. 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 λ-calculus, and the modal λ-calculus. It is shown that a small (namely, Horn) fragment of LP is sufficient for a natural embedding of the typed λ-calculus. It is also shown that LP models the modal λ-calculus.