In 1986, Flagg and Friedman \cite{ff} gave an elegant alternative proof of the faithfulness of G\"{o}del (or Rasiowa-Sikorski) translation $(\cdot)^\Box$ of Heyting arithmetic $\bf HA$ to Shapiro's epistemic arithmetic $\bf EA$. In \S 2, we shall prove the faithfulness of $(\cdot)^\Box$ without using stability, by introducing another translation from an epistemic system to corresponding intuitionistic system which we shall call \it the modified Rasiowa-Sikorski translation\rm . That is, this introduction of the new translation simplifies the original Flagg and Friedman's proof. In \S 3, we shall give some applications of the modified one for the disjunction property ($\mathsf{DP}$) and the numerical existence property ($\mathsf{NEP}$) of Heyting arithmetic. In \S 4, we shall show that epistemic Markov's rule $\mathsf{EMR}$ in $\bf EA$ is proved via $\bf HA$. So $\bf EA$ $\vdash \mathsf{EMR}$ and $\bf HA$ $\vdash \mathsf{MR}$ are equivalent. In \S 5, we shall give some relations among the translations treated in the previous sections. In \S 6, we shall give an alternative proof of Glivenko's theorem. In \S 7, we shall propose several(modal-)epistemic versions of Markov's rule for Horsten's modal-epistemic arithmetic $\bf MEA$. And, as in \S 4, we shall study some meta-implications among those versions of Markov's rules in $\bf MEA$ and one in $\bf HA$. Friedman and Sheard gave a modal analogue $\mathsf{FS}$ (i.e. Theorem in \cite{fs}) of Friedman's theorem $\mathsf{F}$ (i.e. Theorem 1 in \cite {friedman}): \it Any recursively enumerable extension of $\bf HA$ which has $\mathsf{DP}$ also has $\mathsf{NPE}$\rm . In \S 8, we shall give a proof of our \it Fundamental Conjecture \rm $\mathsf{FC}$ proposed in Inou\'{e} \cite{ino90a} as follows: $\mathsf{FC}: \enspace \mathsf{FS} \enspace \Longrightarrow \enspace \mathsf{F}.$ This is a new type of proofs. In \S 9, I shall give discussions.
翻译:1986年,Flagg和Friedman \cite{ff} 为Heyting算术$\bf HA$到Shapiro认知算术$\bf EA$的Gödel(或Rasiowa-Sikorski)翻译$(\cdot)^\Box$的忠实性给出了一个优雅的替代证明。在§2中,我们将通过引入另一种从认知系统到相应直觉主义系统的翻译(称为修正Rasiowa-Sikorski翻译),在不使用稳定性的情况下证明$(\cdot)^\Box$的忠实性。这一新翻译的引入简化了Flagg和Friedman的原始证明。在§3中,我们将给出修正翻译在Heyting算术的析取性质($\mathsf{DP}$)和数值存在性质($\mathsf{NEP}$)方面的一些应用。在§4中,我们将证明$\bf EA$中的认知马尔可夫规则$\mathsf{EMR}$可通过$\bf HA$进行证明,因此$\bf EA$ $\vdash \mathsf{EMR}$与$\bf HA$ $\vdash \mathsf{MR}$是等价的。在§5中,我们将给出前几节处理的各种翻译之间的关系。在§6中,我们将给出Glivenko定理的另一种证明。在§7中,我们将针对Horsten的模态认知算术$\bf MEA$提出马尔可夫规则的若干(模态)认知版本。与§4类似,我们将研究$\bf MEA$中这些马尔可夫规则版本与$\bf HA$中规则之间的元蕴含关系。Friedman和Sheard给出了Friedman定理$\mathsf{F}$(即\cite{friedman}中的定理1)的模态类比$\mathsf{FS}$(即\cite{fs}中的定理):\it 任何具有$\mathsf{DP}$的$\bf HA$递归可枚举扩展也具有$\mathsf{NPE}$\rm 。在§8中,我们将给出Inoué \cite{ino90a}中提出的基本猜想$\mathsf{FC}$的证明:$\mathsf{FC}: \enspace \mathsf{FS} \enspace \Longrightarrow \enspace \mathsf{F}.$ 这是一种新型证明。在§9中,我将进行讨论。