Abstract We introduce the concept of $\textit{access-based}$ intuitionistic knowledge which relies on the intuition that agent $i$ knows $\varphi$ if $i$ has found $\textit{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.

A famous result, conjectured by Gödel in 1932 and proved by McKinsey and Tarski in 1948, says that φ is a theorem of intuitionistic propositional logic IPC iff its Gödel-translation φ′ is a theorem of modal logic S4. In this article, we extend an intuitionistic version of modal logic S1 + SP, introduced in our previous paper [14], to a classical modal logic L and prove the following: a propositional formula φ is a theorem of IPC iff □φ is a theorem of L (actually, we show: Φ⊢IPCφ iff □Φ⊢L□φ⁠, for propositional Φ,φ⁠). Thus, the map φ↦□φ is an embedding of IPC into L, i.e. L contains a copy of IPC. Moreover, L is a conservative extension of classical propositional logic CPC. In this sense, L is an amalgam of CPC and IPC. We show that L is sound and complete w.r.t. a class of special Heyting algebras with a (non-normal) modal operator.

The modal systems S1–S3 were introduced by C. I. Lewis as logics for strict implication. While there are Kripke semantics for S2 and S3, there is no known natural semantics for S1. We extend S1 by a Substitution Principle (SP) which generalizes a reference rule of S1. In system S1 + SP, the relation of strict equivalence ϕ ≡ ψ satisfies the identity axioms of R. Suszko's non-Fregean logic adapted to the language of modal logic (we call these axioms the axioms of propositional identity). This enables us to develop a framework of algebraic semantics which captures S1 + SP as well as the Lewis systems S3–S5. So from the viewpoint of algebraic semantics, S1 + SP turns out to be an interesting modal logic. We show that S1 + SP is strictly contained between S1 and S3 and differs from S2. It is the weakest modal logic containing S1 such that strict equivalence is axiomatized by propositional identity.

Alfred Tarski called a language semantically closed if it contains its own truth predicate and technical means for (self-) reference. We consider the semantically closed non-Fregean logic ∈I, presented in (Lewitzka, 2009, Notre Dame Journal of Formal Logic, 50, 275–301), and introduce a predicate for validity by combining syntactical constructions with a modeltheoretic semantics. The resulting logic, called ∈I+ (Epsilon-I plus), is able to express its own finitary consequence relation. We show that every intuitionistic (or classical) abstract logic extends to a logic which has the semantic features of ∈I (of ∈I+⁠), respectively, namely a truth predicate that satisfies the Tarski biconditionals, a predicate for falsity (as intuitionistic negation), means for propositional (self-) reference, and in the case of ∈I+ also predicates for validity and logical consequence. Applications of our construction to other non-classical abstract logics remain to be further investigated.