Epistemic systems and Flagg and Friedman's translation
share
In 1986, Flagg and Friedman <cit.> gave an elegant alternative proof of the faithfulness of Gödel (or Rasiowa-Sikorski) translation (·)^ of Heyting arithmetic HA to Shapiro's epistemic arithmetic EA. In 2, we shall prove the faithfulness of (·)^ without using stability, by introducing another translation from an epistemic system to corresponding intuitionistic system which we shall call the modified Rasiowa-Sikorski translation. That is, this introduction of the new translation simplifies the original Flagg and Friedman's proof. In 3, we shall give some applications of the modified one for the disjunction property (𝖣𝖯) and the numerical existence property (𝖭𝖤𝖯) of Heyting arithmetic. In 4, we shall show that epistemic Markov's rule 𝖤𝖬𝖱 in EA is proved via HA. So EA ⊢𝖤𝖬𝖱 and HA ⊢𝖬𝖱 are equivalent. In 5, we shall give some relations among the translations treated in the previous sections. In 6, we shall give an alternative proof of Glivenko's theorem. In 7, we shall propose several (modal-)epistemic versions of Markov's rule for Horsten's modal-epistemic arithmetic MEA. And, as in 4, we shall study some meta-implications among those versions of Markov's rules in MEA and one in HA. Friedman and Sheard gave a modal analogue 𝖥𝖲 (i.e. Theorem in <cit.>) of Friedman's theorem 𝖥 (i.e. Theorem 1 in <cit.>): Any recursively enumerable extension of HA which has 𝖣𝖯 also has 𝖭𝖯𝖤. In 8, it is shown that 𝖥𝖲 and the modal disjunction property of EA imply that 𝖣𝖯⇔𝖭𝖤𝖯 holds in HA, i.e. the case of the trivial extension of HA in 𝖥. In 9, we shall give discussions and my philosophy.
READ FULL TEXT