zbMATH — the first resource for mathematics

Access-based intuitionistic knowledge. (English) Zbl 07332115
Summary: We introduce the concept of access-based intuitionistic knowledge which relies on the intuition that agent \(i\) knows \(\varphi\) if \(i\) has found access to a proof of \(\varphi\). Basic principles are distribution and factivity of knowledge as well as \(\square\varphi\rightarrow K_i\varphi\) and \(K_i(\varphi\vee\psi)\rightarrow (K_i\varphi\vee K_i\psi)\), where \(\square\varphi\) reads “\(\varphi\) 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 \(\mathit{IPC}\) and \(\mathit{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.
03-XX Mathematical logic and foundations
68-XX Computer science
PDF BibTeX Cite
Full Text: DOI