Logic Seminar

Serge Artemov Graduate School, CUNY
From BHK Semantics to Justification Logic.

Wednesday, October 3, 2018 - 4:00pm
Malott 206

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.