Intuitionistic Epistemic Logic

TL;DR

This paper develops an intuitionistic epistemic logic that aligns with Brouwer-Heyting-Kolmogorov semantics, offering a constructive perspective on knowledge, factivity, and the knowability paradox, differing from classical logic.

Contribution

It introduces an intuitionistic framework for epistemic logic that reinterprets factivity and resolves the knowability paradox constructively.

Findings

Co-reflection $A ightarrow {f{K}} A$ is valid in this framework.

Factivity ${f{K}} A ightarrow A$ does not hold intuitionistically, but its double negation does.

The knowability paradox is resolved constructively, avoiding classical assumptions.

Abstract

We outline an intuitionistic view of knowledge which maintains the original Brou\-wer-Heyting-Kolmogorov semantics for intuitionism and is consistent with the well-known approach that intuitionistic knowledge be regarded as the result of verification. We argue that on this view co-reflection $A \rightarrow {\bf{K}} A$ is valid and the factivity of knowledge holds in the form ${\bf{K}} A \rightarrow \neg\neg A$ `known propositions cannot be false'. We show that the traditional form of factivity ${\bf{K}} A \rightarrow A$ is a distinctly classical principle which, like {\it tertium non datur} $A\vee\neg A$, does not hold intuitionistically, but, along with the whole of classical epistemic logic, is intuitionistically valid in its double negation form $\neg\neg({\bf{K}} A\rightarrow A)$. Within the intuitionistic epistemic framework the knowability paradox is resolved in a constructive manner. We argue that this paradox is the result of an unwarranted classical reading of constructive principles and as such does not have the consequences for constructive foundations traditionally attributed it.