Talk given on Wednesday April 3, 2019 at The Graduate Center.
Abstract: BHK semantics were introduced to provide a semantics of intuitionistic logic (Int) whereby the truth of a proposition was demonstrated by exhibiting a proof of it. This semi-rigorous approach had some serious difficulties with its exact formalization. The major hurdle of formalization was completed with Artemov's Logic of Proofs (LP), which provided the desired provability semantics. Int was embedded into LP, which was then embedded into Peano Arithmetic (PA). In this talk I will discuss the second inclusion. I will show that there is a complete and sound interpretation of LP into PA, in which LP proof terms are mapped to PA provability formulas.
Slides: [ Ссылка ]
