Knowing how to understand intuitionistic logic (and its relatives)

In this talk, we provide an intuitive understanding of intuitionistic logic by interpreting it as a logic of knowing how (to prove). The approach is inspired by scattered but related ideas hidden in the vast literature of math, philosophy, CS, and linguistics about intuitionistic logic, which also echoes Heyting's largely forgotten conception of intuitionistic logic as "a logic of knowing". The key technique is to combine the bundled modality we developed in the past decade with the BHK-style interpretation. If time permits, I will demonstrate the use of this epistemic interpretation with applications in inquisitive logic, dependence logic, and deontic logic.