In 1986, Flagg and Friedman \cite{ff} gave an elegant alternative proof of the faithfulness of G\"{o}del 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 . 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, it is shown that $\mathsf{FS}$ and the modal $\mathsf{DP}$ of $\bf EA$ imply that $\mathsf{DP} \Leftrightarrow \mathsf{NEP}$ holds in $\bf HA$, i.e. the case of the trivial extension of $\bf HA$ in $\mathsf{F}$. This is a partial result for our conjecture. $ In {\S}9, we shall give some discussions.
翻译:1986年,Flagg与Friedman \cite{ff} 给出了Gödel翻译 $(\cdot)^\Box$ 从Heyting算术 $\bf HA$ 到Shapiro知识论算术 $\bf EA$ 忠实性的一个优雅替代证明。在第2节中,我们将通过引入另一种从知识论系统到相应直觉主义系统的翻译(称为**修正的Rasiowa-Sikorski翻译**),在不使用稳定性条件的情况下证明 $(\cdot)^\Box$ 的忠实性。这一新翻译的引入简化了Flagg与Friedman的原始证明。在第3节中,我们将给出修正翻译在Heyting算术的析取性质($\mathsf{DP}$)和数值存在性质($\mathsf{NEP}$)上的若干应用。在第4节中,我们将证明 $\bf EA$ 中的知识论Markov规则 $\mathsf{EMR}$ 可通过 $\bf HA$ 导出,从而 $\bf EA$ $\vdash \mathsf{EMR}$ 与 $\bf HA$ $\vdash \mathsf{MR}$ 等价。在第5节中,我们将给出前文所讨论翻译之间的若干关系。在第6节中,我们将提供Glivenko定理的另一个证明。在第7节中,我们将为Horsten的模态-知识论算术 $\bf MEA$ 提出Markov规则的若干(模态)知识论版本。与第4节类似,我们将研究 $\bf MEA$ 中这些Markov规则版本与 $\bf HA$ 中对应规则之间的元蕴含关系。Friedman与Sheard曾给出Friedman定理 $\mathsf{F}$(即文献\cite{friedman}中的定理1)的模态类比 $\mathsf{FS}$(即文献\cite{fs}中的定理):**任何具有 $\mathsf{DP}$ 性质的 $\bf HA$ 递归可枚举扩张同时具有 $\mathsf{NPE}$ 性质**。在第8节中,我们将证明 $\mathsf{FS}$ 与 $\bf EA$ 的模态 $\mathsf{DP}$ 蕴含 $\bf HA$ 中 $\mathsf{DP} \Leftrightarrow \mathsf{NEP}$ 成立,即 $\mathsf{F}$ 中 $\bf HA$ 平凡扩张的情形。这是对我们猜想的部分结果。第9节将给出若干讨论。