Geodesic
Embedding of the Modal $\lambda$-Calculus into the Logic of Proofs
Trudy Matematicheskogo Instituta imeni V.A. Steklova, Mathematical logic and algebra, Tome 242 (2003), pp. 44-58

Voir la notice de l'article provenant de la source Math-Net.Ru

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. 
@article{TM_2003_242_a3,
     author = {S. N. Artemov},
     title = {Embedding of the {Modal} $\lambda${-Calculus} into the {Logic} of {Proofs}},
     journal = {Trudy Matematicheskogo Instituta imeni V.A. Steklova},
     pages = {44--58},
     publisher = {mathdoc},
     volume = {242},
     year = {2003},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/TM_2003_242_a3/}
}
TY  - JOUR
AU  - S. N. Artemov
TI  - Embedding of the Modal $\lambda$-Calculus into the Logic of Proofs
JO  - Trudy Matematicheskogo Instituta imeni V.A. Steklova
PY  - 2003
SP  - 44
EP  - 58
VL  - 242
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/TM_2003_242_a3/
LA  - ru
ID  - TM_2003_242_a3
ER  - 
%0 Journal Article
%A S. N. Artemov
%T Embedding of the Modal $\lambda$-Calculus into the Logic of Proofs
%J Trudy Matematicheskogo Instituta imeni V.A. Steklova
%D 2003
%P 44-58
%V 242
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TM_2003_242_a3/
%G ru
%F TM_2003_242_a3
S. N. Artemov. Embedding of the Modal $\lambda$-Calculus into the Logic of Proofs. Trudy Matematicheskogo Instituta imeni V.A. Steklova, Mathematical logic and algebra, Tome 242 (2003), pp. 44-58. http://geodesic.mathdoc.fr/item/TM_2003_242_a3/