Logic Seminar
The intended semantics of intuitionistic logic is Brouwer-Heyting-Kolmogorov (BHK) provability semantics which spells out Brouwer's thesis that intuitionistic truth is provability. A conceptually clean way to approach BHK has been suggested by Kolmogorov and Gödel: to BHK-interpret intuitionistic logic via constructive reasoning in the usual classical mathematics.
Such exact provability reading of BHK, despite early progress made by Gödel in 1933-38, turned out to be quite elusive. A provability BHK semantics for the propositional intuitionistic logic IPC was found only in 1995 within the framework of the logic of proofs LP. The answer is given by a chain of embeddings of IPC into S4 (Gödel, MacKinsey-Tarsky), S4 into LP (realization theorem, S.A.) and LP into Peano Arithmetics PA (arithmetical completeness, S.A.).
The Logic of Proofs together with new ideas is now a fast-expanding framework, Justification Logic, with broad applications ranging from type theories with internalization to hyperintensional logics with epistemic justifications.