A Note on Flagg and Friedman's Epistemic and Intuitionistic Formal Systems

TL;DR

This paper investigates Flagg and Friedman's translation from Epistemic to Intuitionistic logic, providing a proof of its soundness and discussing the admissibility of the necessitation rule, thereby supporting their proof method.

Contribution

It offers an explicit proof of the soundness of Flagg and Friedman's translation and examines the admissibility of the necessitation rule within this framework.

Findings

Proof of the soundness of the translation

Discussion on the admissibility of necessitation rule

Clarification of properties of the translation

Abstract

We report our findings on the properties of Flagg and Friedman's translation from Epistemic into Intuitionistic logic, which was proposed as the basis of a comprehensive proof method for the faithfulness of the Goodel translation. We focus on the propositional case and raise the issue of the admissibility of the translated necessitation rule. Then, we contribute to Flagg and Friedman's program by giving an explicit proof of the soundness of their translation.