John Connor --- Intuitionistic Epistemic Logic and Propositional Truncation in the Type Theory.

Talk given on Wednesday November 14, 2018 at The Graduate Center, CUNY. Abstract: Intuitionistic Epistemic Logic (IEL) is an extension of Intuitionistic Propositional Logic introduced by Artemov and Protopopescu. IEL introduces a co-reflexive modal axiom P ⇒ (K P), where the intended interpretation of (K P) is that P is known, but a proof of P is not necessarily at hand. In this talk I introduce an extension of the simply typed λ-calculus which is equivalent to IEL via an extension of the Curry-Howard cor