Access-based intuitionistic knowledge

摘要

We introduce the concept of access-based intuitionistic knowledge which relies on the intuition that agent i knows phi if i has found access to a proof of phi. Basic principles are distribution and factivity of knowledge as well as square(phi) -> K-i phi and K-i(phi boolean OR psi) -> (K-i phi boolean OR K-i psi), where (sic)(phi) reads 'phi is proved'. The formalization extends a family of classical modal logics (Lewitzka, 2017, Journal of Logic and Computation, 27, 201-212) designed as combinations of IPC and CPC and as systems for the reasoning about proof, i.e. intuitionistic truth. We adopt a formalization of common knowledge from (Lewitzka, 2011, Studia Logica, 97, 233-264) and interpret it here as access-based common knowledge. We compare our proposal with recent approaches to intuitionistic knowledge (Artemov and Protopopescu, 2016, The Review of Symbolic Logic, 9, 266-298; Lewitzka, 2019, Annals of Pure and Applied Logic, 170, 218-250) and bring together these different concepts in a unifying semantic framework based on Heyting algebra expansions.