Modality Definition Synthesis for Epistemic Intuitionistic Logic via a Theorem Prover

TL;DR

This paper presents a Prolog theorem prover for an intuitionistic epistemic logic, synthesizing modality definitions and embedding the logic into propositional intuitionistic logic, with analysis of epistemic operators and their properties.

Contribution

It introduces a method to automatically synthesize epistemic modality definitions and embed intuitionistic epistemic logic into propositional intuitionistic logic using a theorem prover.

Findings

Successfully embedded IEL into IPC with valid axioms and theorems.

Discovered that Dosen's double negation modality is inadequate as an epistemic operator.

Identified limitations of the necessitation rule in the S4 embedding.

Abstract

We derive a Prolog theorem prover for an Intuitionistic Epistemic Logic by starting from the sequent calculus {\bf G4IP} that we extend with operator definitions providing an embedding in intuitionistic propositional logic ({\bf IPC}). With help of a candidate definition formula generator, we discover epistemic operators for which axioms and theorems of Artemov and Protopopescu's {\em Intuitionistic Epistemic Logic} ({\bf IEL}) hold and formulas expected to be non-theorems fail. We compare the embedding of {\bf IEL} in {\bf IPC} with a similarly discovered successful embedding of Dosen's double negation modality, judged inadequate as an epistemic operator. Finally, we discuss the failure of the {\em necessitation rule} for an otherwise successful {\bf S4} embedding and share our thoughts about the intuitions explaining these differences between epistemic and alethic modalities in the context of the Brouwer-Heyting-Kolmogorov semantics of intuitionistic reasoning and knowledge acquisition. Keywords: epistemic intuitionistic logic, propositional intuitionistic logic, Prolog-based theorem provers, automatic synthesis of logic systems, definition formula generation algorithms, embedding of modal logics into intuitionistic logic.